		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Constraint-vars

Set of variables in a constraint.

Signature
(constraint-vars constr) → vars
Arguments: constr — Guard (constraintp constr).
Returns: vars — Type (string-setp vars).

Definitions and Theorems

Function: constraint-vars

(defun constraint-vars (constr)
  (declare (xargs :guard (constraintp constr)))
  (let ((__function__ 'constraint-vars))
    (declare (ignorable __function__))
    (constraint-case constr
                     :equal (union (expression-vars constr.left)
                                   (expression-vars constr.right))
                     :relation (expression-list-vars constr.args))))

Theorem: string-setp-of-constraint-vars

(defthm string-setp-of-constraint-vars
  (b* ((vars (constraint-vars constr)))
    (string-setp vars))
  :rule-classes :rewrite)