		Search-engine friendly clone of the ACL2 documentation.

Fgl-solving

Fgl-sat-check/print-counterexample

Check satisfiability during FGL interpretation and print counterexamples.

Signature
(fgl-sat-check/print-counterexample params msg x) → *

Similar to fgl-sat-check, but this version additionally prints the counterexample bindings, when satisfiable, for the context from which it was called. Its functionality depends on the rewrite rule fgl-sat-check/print-counterexample-rw. The extra argument msg should be a string or message identifying the particular SAT check.

Definitions and Theorems

Function: fgl-sat-check/print-counterexample

(defun fgl-sat-check/print-counterexample (params msg x)
  (declare (ignore params msg))
  (declare (xargs :guard t))
  (let ((__function__ 'fgl-sat-check/print-counterexample))
    (declare (ignorable __function__))
    (if x t nil)))

Theorem: fgl-sat-check/print-counterexample-rw

(defthm fgl-sat-check/print-counterexample-rw
 (equal
  (fgl-sat-check/print-counterexample params msg x)
  (b*
   ((ans (fgl-sat-check params x))
    (unsatp (syntax-bind unsat (eq ans nil)))
    ((when unsatp) ans)
    ((list (list error bindings vars) &)
     (syntax-bind
          alists
          (show-counterexample-bind params interp-st state)))
    ((when error)
     (b* ((?ignore (cw "~@0: ~@1" msg error)))
       ans))
    (?ignore
         (cw "~@0: Counterexample -- bindings: ~x1 variables: ~x2~%"
             msg bindings vars)))
   ans)))