constraint-db - ACL2 Book

other

(in-package "GL")

other

(include-book "clause-processors/unify-subst" :dir :system)

other

(include-book "glcp-unify-defs")

other

(include-book "clause-processors/magic-ev" :dir :system)

gl-bool-fixfunction

(defun gl-bool-fix (x) (and x t))

other

(defaggregate constraint-rule
  (thmname lit-alist syntaxp))

other

(defaggregate constraint-tuple
  (rule existing-lits
    matching-lit
    common-vars
    existing-vars
    sig-table))

gbc-rule-lit-add-catalog-entryfunction

(defun gbc-rule-lit-add-catalog-entry
  (var pat rule ccat)
  (b* ((fnsym (car pat)) (tuples (cdr (hons-assoc-equal fnsym ccat)))
      (new-tuple (constraint-tuple rule
          nil
          var
          nil
          nil
          (hons-acons nil (list nil) nil))))
    (cons (cons fnsym (cons new-tuple tuples))
      ccat)))

gbc-rule-add-catalog-entriesfunction

(defun gbc-rule-add-catalog-entries
  (lit-alist rule ccat)
  (b* (((when (atom lit-alist)) ccat) ((cons var pat) (car lit-alist))
      (ccat (gbc-rule-lit-add-catalog-entry var
          pat
          rule
          ccat)))
    (gbc-rule-add-catalog-entries (cdr lit-alist)
      rule
      ccat)))

gbc-alist-has-symmetricfunction

(defun gbc-alist-has-symmetric
  (term alist)
  (b* (((when (atom alist)) nil) (term2 (cdar alist))
      ((mv ok1 &) (simple-one-way-unify term term2 nil))
      ((mv ok2 &) (simple-one-way-unify term2 term nil)))
    (or (and ok1 ok2)
      (gbc-alist-has-symmetric term (cdr alist)))))

gbc-alist-remove-symmetricfunction

(defun gbc-alist-remove-symmetric
  (alist)
  (if (atom alist)
    nil
    (if (gbc-alist-has-symmetric (cdar alist)
        (cdr alist))
      (gbc-alist-remove-symmetric (cdr alist))
      (cons (car alist)
        (gbc-alist-remove-symmetric (cdr alist))))))

gbc-rule-add-to-catalogfunction

(defun gbc-rule-add-to-catalog
  (rule ccat)
  (b* ((syntaxp (constraint-rule->syntaxp rule)) (alist (constraint-rule->lit-alist rule))
      (reduced-alist (if (equal syntaxp ''t)
          (gbc-alist-remove-symmetric alist)
          alist)))
    (hons-shrink-alist (gbc-rule-add-catalog-entries reduced-alist
        rule
        ccat)
      nil)))

gbc-add-rulemacro

(defmacro gbc-add-rule
  (name lit-alist syntaxp)
  `(table gl-bool-constraints
    nil
    (gbc-rule-add-to-catalog (constraint-rule ',GL::NAME
        ',GL::LIT-ALIST
        ',GL::SYNTAXP)
      (table-alist 'gl-bool-constraints world))
    :clear))

gbc-translate-lit-alistfunction

(defun gbc-translate-lit-alist
  (lit-patterns state)
  (declare (xargs :mode :program :stobjs state))
  (b* (((when (atom lit-patterns)) (value nil)) ((list var term) (car lit-patterns))
      ((er trans) (translate term
          t
          t
          nil
          'def-gl-boolean-constraint
          (w state)
          state))
      ((er rest) (gbc-translate-lit-alist (cdr lit-patterns)
          state)))
    (value (cons (cons var trans) rest))))

def-gl-boolean-constraint-fnfunction

(defun def-gl-boolean-constraint-fn
  (name lit-patterns
    syntaxp
    body
    hints
    state)
  (declare (xargs :mode :program :stobjs state))
  (b* (((er syntaxp-trans) (translate syntaxp
         t
         t
         nil
         'def-gl-boolean-constraint
         (w state)
         state)) ((er alist) (gbc-translate-lit-alist lit-patterns state))
      (body1 `(let ,(GL::PAIRLIS$ (GL::STRIP-CARS GL::LIT-PATTERNS)
  (GL::PAIRLIS$
   (GL::PAIRLIS$
    (GL::MAKE-LIST-AC (GL::LEN GL::LIT-PATTERNS) 'GL::GL-BOOL-FIX NIL)
    (GL::STRIP-CDRS GL::LIT-PATTERNS))
   NIL))
          ,GL::BODY)))
    (value `(progn (defthm ,GL::NAME
          ,GL::BODY1
          :hints ,GL::HINTS
          :rule-classes nil)
        (gbc-add-rule ,GL::NAME ,GL::ALIST ,GL::SYNTAXP-TRANS)))))

other

(defsection def-gl-boolean-constraint
  :parents (reference term-level-reasoning)
  :short "Define a rule that recognizes constraints among GL generated Boolean variables"
  :long "
<p>When using GL in a term-level style (see @(see term-level-reasoning)), GL
may generate new Boolean variables from terms that appear as IF tests.</p>

<p>Sometimes, the terms from which these variables are generated have
interdependent meanings.  For example, if Boolean variable @('a') represents
@('(logbitp 5 x)') and Boolean variable @('b') represents @('(integerp x)'), it
should be impossible for @('a') to be true when @('b') is false.  However, by
default, the Boolean variables generated this way are unconstrained.  When
this sort of interdependency among variables exists but is not accounted for,
it can cause GL to find @(see false-counterexamples).</p>

<p>@('Def-gl-boolean-constraint') provides a mechanism to make such constraints
known to GL.  While symbolically executing a form, GL maintains a constraint, a
Boolean formula known to always be true (under the evolving assignment of
Boolean variables to terms).  A constraint rule generated by
@('def-gl-boolean-constraint') is triggered when a Boolean variable is
generated from an IF condition term and can cause the constraint to be updated
with a new conjunct.</p>

<p>A Boolean constraint rule is formulated as follows:</p>
@({
 (def-gl-boolean-constraint gl-logbitp-implies-integerp
    :bindings ((bit    (logbitp n x))
               (intp   (integerp x)))
    :body (implies bit intp)
    ;; optional arguments:
    :syntaxp ...
    :hints ...)
 })
<p>This generates a proof obligation:</p>
@({
 (defthm gl-logbitp-implies-integerp
   (let ((bit    (gl-bool-fix (logbitp n x)))
         (intp   (gl-bool-fix (integerp x))))
     (implies bit intp))
  :hints ...
  :rule-classes nil)
 })
<p>(The optional :hints argument to def-gl-boolean-constraint provides the
hints for the proof obligation.)</p>

<p>Once this rule is established, GL will generate constraints as follows:</p>
<ul>
<li>When a Boolean variable @('a') is generated from an IF condition matching
@('(logbitp n x)'), GL will search for an existing generated Boolean variable
@('b') whose IF condition was @('(integerp x)') and, if it exists, add the
constraint @('(implies a b)').</li>

<li>Conversely, when a Boolean variable @('b') is generated from an IF
condition matching @('(integerp x)'), GL will search for existing generated
Boolean variables @('ai') matching @('(logbitp n x)'), and for each of them,
add the constraint @('(implies ai b)').</li>
</ul>

<p>To show that this rule works, you can verify that the following events fail
prior to introducing the constraint rule above, but succeed after:</p>

@({
 (def-gl-thm foo1
    :hyp t
    :concl (if (integerp x) t (not (logbitp n x)))
    :g-bindings nil
    :rule-classes nil)

 (def-gl-thm foo2
    :hyp t
    :concl (if (logbitp n x) (integerp x) t)
    :g-bindings nil
    :rule-classes nil)
 })
"
  (defmacro def-gl-boolean-constraint
    (name &key
      bindings
      (syntaxp ''t)
      body
      hints)
    `(make-event (def-gl-boolean-constraint-fn ',GL::NAME
        ',GL::BINDINGS
        ',GL::SYNTAXP
        ',GL::BODY
        ',GL::HINTS
        state))))

gbc-signaturefunction

(defun gbc-signature
  (common-vars subst)
  (if (atom common-vars)
    nil
    (hons (cdr (assoc (car common-vars) subst))
      (gbc-signature (cdr common-vars) subst))))

gbc-extend-substsfunction

(defun gbc-extend-substs
  (lit-subst partial-substs)
  (if (atom partial-substs)
    nil
    (cons (append lit-subst (car partial-substs))
      (gbc-extend-substs lit-subst
        (cdr partial-substs)))))

gbc-substs-check-syntaxpfunction

(defun gbc-substs-check-syntaxp
  (substs thmname syntaxp state)
  (declare (xargs :stobjs state :verify-guards nil))
  (b* (((when (atom substs)) nil) ((mv err ok) (magic-ev syntaxp (car substs) state t t))
      ((when (or err (not ok))) (gbc-substs-check-syntaxp (cdr substs)
          thmname
          syntaxp
          state)))
    (cons (cons thmname (car substs))
      (gbc-substs-check-syntaxp (cdr substs)
        thmname
        syntaxp
        state))))

gbc-sort-substs-into-sigtablefunction

(defun gbc-sort-substs-into-sigtable
  (substs common-vars sigtable)
  (b* (((when (atom substs)) sigtable) (subst (car substs))
      (sig (gbc-signature common-vars subst))
      (sig-substs (cdr (hons-get sig sigtable)))
      (sigtable (hons-acons sig
          (cons subst sig-substs)
          sigtable)))
    (gbc-sort-substs-into-sigtable (cdr substs)
      common-vars
      sigtable)))

gbc-unbound-lits-add-to-existing-tuplefunction

(defun gbc-unbound-lits-add-to-existing-tuple
  (rule existing-lits lit substs tuples)
  (b* (((when (atom tuples)) (mv nil tuples)) ((constraint-tuple x) (car tuples))
      ((unless (and (equal rule x.rule)
           (equal existing-lits x.existing-lits)
           (equal lit x.matching-lit))) (b* (((mv found rest) (gbc-unbound-lits-add-to-existing-tuple rule
               existing-lits
               lit
               substs
               (cdr tuples))) ((when found) (mv t (cons (car tuples) rest))))
          (mv nil tuples)))
      (sigtable (gbc-sort-substs-into-sigtable substs
          x.common-vars
          x.sig-table)))
    (mv t
      (cons (constraint-tuple rule
          existing-lits
          lit
          x.common-vars
          x.existing-vars
          sigtable)
        (cdr tuples)))))

gbc-unbound-lits-add-tuplesfunction

(defun gbc-unbound-lits-add-tuples
  (litvars rule
    existing-lits
    existing-vars
    substs
    ccat)
  (b* (((when (atom litvars)) ccat) (var (car litvars))
      ((constraint-rule r) rule)
      (lit (cdr (hons-assoc-equal var r.lit-alist)))
      (fnsym (car lit))
      (tuples (cdr (hons-get fnsym ccat)))
      ((mv found tuples) (gbc-unbound-lits-add-to-existing-tuple rule
          existing-lits
          var
          substs
          tuples))
      ((when found) (hons-acons fnsym tuples ccat))
      (lit-vars (mergesort (simple-term-vars lit)))
      (common-vars (intersect existing-vars lit-vars))
      (sigtable (gbc-sort-substs-into-sigtable substs
          common-vars
          nil))
      (new-tuple (constraint-tuple rule
          existing-lits
          var
          common-vars
          existing-vars
          sigtable)))
    (hons-acons fnsym
      (cons new-tuple tuples)
      ccat)))

gbc-process-new-lit-tuplefunction

(defun gbc-process-new-lit-tuple
  (lit tuple ccat state)
  (declare (xargs :stobjs state :verify-guards nil))
  (b* (((constraint-tuple x) tuple) ((constraint-rule r) x.rule)
      (pat (cdr (hons-assoc-equal x.matching-lit r.lit-alist)))
      ((mv ok lit-subst) (glcp-unify-term/gobj pat lit nil))
      ((unless ok) (mv nil ccat))
      (sig (gbc-signature x.common-vars lit-subst))
      (partial-substs (cdr (hons-get sig x.sig-table)))
      (new-substs (gbc-extend-substs lit-subst partial-substs))
      (rest-litvars (set-difference-eq (strip-cars r.lit-alist)
          (cons x.matching-lit x.existing-lits)))
      ((unless rest-litvars) (b* ((substs (gbc-substs-check-syntaxp new-substs
               r.thmname
               r.syntaxp
               state)))
          (mv substs ccat)))
      (new-existing-vars (union (mergesort (strip-cars lit-subst))
          x.existing-vars))
      (ccat (gbc-unbound-lits-add-tuples rest-litvars
          x.rule
          (insert x.matching-lit x.existing-lits)
          new-existing-vars
          new-substs
          ccat)))
    (mv nil ccat)))

gbc-process-new-lit-tuplesfunction

(defun gbc-process-new-lit-tuples
  (lit tuples ccat state)
  (declare (xargs :stobjs state :verify-guards nil))
  (b* (((when (atom tuples)) (mv nil ccat)) ((mv substs1 ccat) (gbc-process-new-lit-tuple lit
          (car tuples)
          ccat
          state))
      ((mv substs-rest ccat) (gbc-process-new-lit-tuples lit
          (cdr tuples)
          ccat
          state)))
    (mv (append substs1 substs-rest) ccat)))

other

(defund gbc-process-new-lit
  (lit ccat state)
  (declare (xargs :stobjs state :verify-guards nil))
  (b* (((unless (and (consp lit) (eq (tag lit) :g-apply))) (mv nil ccat)) (tuples (cdr (hons-get (g-apply->fn lit) ccat))))
    (gbc-process-new-lit-tuples lit
      tuples
      ccat
      state)))

gbc-tuples-make-fastfunction

(defun gbc-tuples-make-fast
  (x)
  (if (atom x)
    nil
    (cons (change-constraint-tuple (car x)
        :sig-table (make-fast-alist (constraint-tuple->sig-table (car x))))
      (gbc-tuples-make-fast (cdr x)))))

gbc-tuples-freefunction

(defun gbc-tuples-free
  (x)
  (if (atom x)
    nil
    (prog2$ (fast-alist-free (constraint-tuple->sig-table (car x)))
      (gbc-tuples-free (cdr x)))))

gbc-db-make-fast-recfunction

(defun gbc-db-make-fast-rec
  (x acc)
  (b* (((when (atom x)) acc) (acc (if (and (consp (car x))
            (not (hons-get (caar x) acc)))
          (hons-acons (caar x)
            (gbc-tuples-make-fast (cdar x))
            acc)
          acc)))
    (gbc-db-make-fast-rec (cdr x) acc)))

other

(defund gbc-db-make-fast
  (x)
  (gbc-db-make-fast-rec x nil))

gbc-db-free-recfunction

(defun gbc-db-free-rec
  (x)
  (if (atom x)
    nil
    (prog2$ (and (consp (car x)) (gbc-tuples-free (cdar x)))
      (gbc-db-free-rec (cdr x)))))

other

(defund gbc-db-free
  (x)
  (gbc-db-free-rec (fast-alist-free x)))