		Search-engine friendly clone of the ACL2 documentation.

Semantics-shallowly-embedded

Sesem-constraint

Shallowly embedded semantics of a constraint.

Signature
(sesem-constraint constr prime state) → term
Arguments: constr — Guard (constraintp constr).; prime — Guard (symbolp prime).

We turn an equality constraint into an ACL2 equality of the terms denoted by the left and right expressions. We turn a relation constraint into an ACL2 call of the relation on the terms denoted by the argument expressions. Note that we include the variable for the prime.

Definitions and Theorems

Function: sesem-constraint

(defun sesem-constraint (constr prime state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (constraintp constr)
                             (symbolp prime))))
 (let ((__function__ 'sesem-constraint))
  (declare (ignorable __function__))
  (constraint-case
       constr
       :equal
       (cons 'equal
             (cons (sesem-expression constr.left prime state)
                   (cons (sesem-expression constr.right prime state)
                         'nil)))
       :relation
       (cons (name-to-symbol constr.name state)
             (append (sesem-expression-list constr.args prime state)
                     (cons prime 'nil))))))