		Search-engine friendly clone of the ACL2 documentation.

Constraint-tuple

Make-constraint-tuple

Basic constructor macro for constraint-tuple structures.

Syntax

(make-constraint-tuple [:rule <rule>] 
                       [:existing-lits <existing-lits>] 
                       [:matching-lit <matching-lit>] 
                       [:common-vars <common-vars>] 
                       [:existing-vars <existing-vars>] 
                       [:sig-table <sig-table>])

This is the usual way to construct constraint-tuple structures. It simply conses together a structure with the specified fields.

This macro generates a new constraint-tuple structure from scratch. See also change-constraint-tuple, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-constraint-tuple

(defmacro make-constraint-tuple (&rest args)
  (std::make-aggregate 'constraint-tuple
                       args
                       '((:rule)
                         (:existing-lits)
                         (:matching-lit)
                         (:common-vars)
                         (:existing-vars)
                         (:sig-table))
                       'make-constraint-tuple
                       nil))

Function: constraint-tuple

(defun constraint-tuple (rule existing-lits matching-lit
                              common-vars existing-vars sig-table)
 (declare (xargs :guard (and (constraint-rule-p rule)
                             (pseudo-var-set-p existing-lits)
                             (pseudo-var-p matching-lit)
                             (pseudo-var-set-p common-vars)
                             (pseudo-var-set-p existing-vars)
                             (sig-table-p sig-table))))
 (declare (xargs :guard t))
 (let ((__function__ 'constraint-tuple))
  (declare (ignorable __function__))
  (b* ((rule (mbe :logic (constraint-rule-fix rule)
                  :exec rule))
       (existing-lits (mbe :logic (pseudo-var-set-fix existing-lits)
                           :exec existing-lits))
       (matching-lit (mbe :logic (pseudo-var-fix matching-lit)
                          :exec matching-lit))
       (common-vars (mbe :logic (pseudo-var-set-fix common-vars)
                         :exec common-vars))
       (existing-vars (mbe :logic (pseudo-var-set-fix existing-vars)
                           :exec existing-vars))
       (sig-table (mbe :logic (sig-table-fix sig-table)
                       :exec sig-table)))
    (cons (cons rule (cons existing-lits matching-lit))
          (cons common-vars
                (cons existing-vars sig-table))))))