Included Books
other
(in-package "ACL2")
include-book
(include-book "witness")
include-book
(include-book "subset")
include-book
(include-book "misc/untranslate-patterns" :dir :system)
other
(add-untranslate-pattern (q-ite-fn ?x ?y ?z) (q-ite ?x ?y ?z))
other
(add-untranslate-pattern (q-implies-fn ?x ?y) (q-implies ?x ?y))
other
(add-untranslate-pattern (q-or-c2-fn ?x ?y) (q-or-c2 ?x ?y))
other
(add-untranslate-pattern (q-and-c1-fn ?x ?y) (q-and-c1 ?x ?y))
other
(add-untranslate-pattern (q-and-c2-fn ?x ?y) (q-and-c2 ?x ?y))
other
(theory-invariant (incompatible (:rewrite |(qs-subset x nil)|) (:rewrite bdd-equality-is-double-containment)))
other
(theory-invariant (incompatible (:rewrite |(qs-subset t x)|) (:rewrite bdd-equality-is-double-containment)))
other
(theory-invariant (incompatible (:rewrite equal-by-eval-bdds) (:rewrite bdd-equality-is-double-containment)))
other
(def-ruleset non-qs-subset-mode-rules '(|(qs-subset x nil)| |(qs-subset t x)| equal-by-eval-bdds eval-bdd-cp-hint))
qs-subset-modemacro
(defmacro qs-subset-mode (value) (declare (xargs :guard (booleanp value))) (if value '(in-theory (e/d* ((:ruleset qs-subset-mode-rules)) ((:ruleset non-qs-subset-mode-rules)))) '(in-theory (e/d* nil ((:ruleset qs-subset-mode-rules))))))
other
(qs-subset-mode nil)
other
(def-ruleset non-q-witness-mode-rules '(equal-by-eval-bdds eval-bdd-diff-witness eval-bdd-diff-witness-corr eval-bdd-when-qs-subset))
q-witness-modemacro
(defmacro q-witness-mode (value) (declare (xargs :guard (booleanp value))) (if value '(in-theory (e/d* ((:ruleset q-witness-mode-rules)) ((:ruleset non-q-witness-mode-rules)))) '(in-theory (e/d* nil ((:ruleset q-witness-mode-rules))))))
other
(q-witness-mode nil)
other
(theory-invariant (incompatible (:definition eval-bdd-cp-hint) (:rewrite equal-by-eval-bdds)))
other
(theory-invariant (incompatible (:definition eval-bdd-cp-hint) (:rewrite bdd-equality-is-double-containment)))