		Search-engine friendly clone of the ACL2 documentation.

Semantics-deeply-embedded

Definition-satp

Check if a sequence of prime field elements satisfies a named PFCS definition.

Signature
(definition-satp name defs vals p) → yes/no
Arguments: name — Guard (stringp name).; defs — Guard (definition-listp defs).; vals — Guard (fe-listp vals p).; p — Guard (primep p).
Returns: yes/no — Type (booleanp yes/no).

We find the definition with the given name, to obtain its parameters. We form an assignment of the prime field elements to the parameters, in order, and we check if this assignment satisfies the constraint consisting of a call of the definition on its parameters.

This is a convenient abbreviation for expressing the satisfiability of a definition.

Definitions and Theorems

Function: definition-satp

(defun definition-satp (name defs vals p)
 (declare (xargs :guard (and (stringp name)
                             (definition-listp defs)
                             (primep p)
                             (fe-listp vals p))))
 (let ((__function__ 'definition-satp))
  (declare (ignorable __function__))
  (b*
   ((def (lookup-definition name defs))
    ((unless def) nil)
    (para (definition->para def))
    ((unless (= (len vals) (len para))) nil)
    (asg (omap::from-lists para vals))
    (constr
       (make-constraint-relation :name name
                                 :args (expression-var-list para))))
   (constraint-satp constr defs asg p))))

Theorem: booleanp-of-definition-satp

(defthm booleanp-of-definition-satp
  (b* ((yes/no (definition-satp name defs vals p)))
    (booleanp yes/no))
  :rule-classes :rewrite)