bfr-sat

(in-package "GL")

(include-book "bfr")

(include-book "centaur/misc/hons-extra" :dir :system)

(encapsulate (((bfr-sat *) => (mv * * *)))
  (local (defun bfr-sat
      (prop)
      (declare (xargs :guard t))
      (mv nil nil prop)))
  (defthm bfr-sat-nvals
    (equal (len (bfr-sat prop)) 3))
  (defthm bfr-sat-true-listp
    (true-listp (bfr-sat prop)))
  (defthm bfr-sat-unsat
    (mv-let (sat succeeded ctrex)
      (bfr-sat prop)
      (declare (ignore ctrex))
      (implies (and succeeded (not sat))
        (not (bfr-eval prop env))))))

(defun bfr-sat-bdd
  (prop)
  (declare (xargs :guard t))
  (if (bfr-mode)
    (mv nil nil nil)
    (let ((sat? (eval-bdd prop (bdd-sat-dfs prop))))
      (mv sat? t prop))))

(defthmd bfr-sat-bdd-unsat
  (mv-let (sat succeeded ctrex)
    (bfr-sat-bdd prop)
    (declare (ignore ctrex))
    (implies (and succeeded (not sat))
      (not (bfr-eval prop env))))
  :hints (("Goal" :in-theory (e/d (bfr-eval) (eval-bdd-ubdd-fix))
     :use ((:instance eval-bdd-ubdd-fix (x prop))))))

(defattach (bfr-sat bfr-sat-bdd)
  :hints (("goal" :in-theory '(bfr-sat-bdd-unsat)) (and stable-under-simplificationp
      '(:in-theory (enable bfr-sat-bdd)))))

(in-theory (disable bfr-sat-bdd-unsat bfr-sat-unsat))

(defstub bfr-counterex-mode nil t)

(defun bfr-counterex-alist
  nil
  (declare (xargs :guard t))
  t)

(defun bfr-counterex-bdd
  nil
  (declare (xargs :guard t))
  nil)

(defattach bfr-counterex-mode bfr-counterex-bdd)

(defun to-satisfying-assign
  (lst bdd)
  (declare (xargs :hints (("goal" :in-theory (enable acl2-count)))
      :guard (true-listp lst)))
  (cond ((atom bdd) lst)
    ((eq (cdr bdd) nil) (cons t (to-satisfying-assign lst (car bdd))))
    ((eq (car bdd) nil) (cons nil (to-satisfying-assign lst (cdr bdd))))
    (t (cons (car lst)
        (to-satisfying-assign (cdr lst)
          (if (car lst)
            (car bdd)
            (cdr bdd)))))))

(defthm to-satisfying-assign-correct
  (implies (and bdd (ubddp bdd))
    (eval-bdd bdd
      (to-satisfying-assign lst bdd)))
  :hints (("Goal" :in-theory (enable eval-bdd ubddp))))

(defun bfr-ctrex-to-satisfying-assign
  (assign ctrex)
  (declare (xargs :guard (true-listp assign)))
  (if (eq (bfr-counterex-mode) t)
    ctrex
    (to-satisfying-assign assign ctrex)))

(defund bfr-known-value
  (x)
  (declare (xargs :guard t))
  (bfr-case :bdd (and x t) :aig (aig-eval x nil)))

(defsection bfr-constcheck
  (defund bfr-constcheck
    (x pathcond)
    (declare (xargs :guard t))
    (if (eq pathcond t)
      (mv t
        (if (bfr-known-value x)
          (b* (((mv sat ok &) (bfr-sat (bfr-not x))))
            (if (or sat (not ok))
              x
              t))
          (b* (((mv sat ok &) (bfr-sat x)))
            (if (or sat (not ok))
              x
              nil))))
      (b* (((mv sat ok ctrex) (bfr-sat pathcond)) ((unless ok) (mv t x))
          ((unless sat) (mv nil nil))
          (env (bfr-ctrex-to-satisfying-assign nil ctrex))
          ((with-fast env))
          (known-val (bfr-eval x env))
          ((mv sat ok &) (bfr-sat (bfr-and pathcond
                (if known-val
                  (bfr-not x)
                  x))))
          ((unless (or sat (not ok))) (mv t known-val)))
        (mv t x))))
  (local (in-theory (enable bfr-constcheck)))
  (defthmd bfr-constcheck-pathcond-unsat
    (b* (((mv ?pc-sat ?xx) (bfr-constcheck x pathcond)))
      (implies (not pc-sat)
        (not (bfr-eval pathcond env))))
    :hints (("Goal" :in-theory (enable bfr-sat-unsat))))
  (defthm bfr-eval-of-bfr-constcheck
    (b* (((mv ?pc-sat ?xx) (bfr-constcheck x pathcond)))
      (implies (bfr-eval pathcond env)
        (and pc-sat
          (equal (bfr-eval xx env)
            (bfr-eval x env)))))
    :hints (("goal" :use ((:instance bfr-sat-unsat
          (prop (bfr-and pathcond x))) (:instance bfr-sat-unsat
           (prop (bfr-and pathcond (bfr-not x))))
         (:instance bfr-sat-unsat (prop x))
         (:instance bfr-sat-unsat (prop (bfr-not x)))
         (:instance bfr-sat-unsat (prop pathcond))))))
  (defthm pbfr-depends-on-of-bfr-constcheck
    (b* (((mv ?pc-sat ?xx) (bfr-constcheck x pathcond)))
      (implies (not (pbfr-depends-on k p x))
        (not (pbfr-depends-on k p xx))))))

(defsection bfr-check-true
  (defund bfr-check-true
    (x pathcond)
    (declare (xargs :guard t))
    (if (eq pathcond t)
      (if (bfr-known-value x)
        (b* (((mv sat ok &) (bfr-sat (bfr-not x))))
          (if (or sat (not ok))
            x
            t))
        x)
      (b* (((mv sat ok &) (bfr-sat (bfr-and pathcond (bfr-not x)))))
        (if (or sat (not ok))
          x
          t))))
  (local (in-theory (enable bfr-check-true)))
  (defthm bfr-eval-of-bfr-check-true
    (implies (bfr-eval pathcond env)
      (equal (bfr-eval (bfr-check-true x pathcond)
          env)
        (bfr-eval x env)))
    :hints (("goal" :use ((:instance bfr-sat-unsat (prop (bfr-not x))) (:instance bfr-sat-unsat
           (prop (bfr-and pathcond (bfr-not x))))))))
  (defthm pbfr-depends-on-of-bfr-check-true
    (implies (not (pbfr-depends-on k p x))
      (not (pbfr-depends-on k
          p
          (bfr-check-true x pathcond))))))

(defsection bfr-check-false
  (defund bfr-check-false
    (x pathcond)
    (declare (xargs :guard t))
    (if (eq pathcond t)
      (if (bfr-known-value x)
        x
        (b* (((mv sat ok &) (bfr-sat x)))
          (if (or sat (not ok))
            x
            nil)))
      (b* (((mv sat ok &) (bfr-sat (bfr-and pathcond x))))
        (if (or sat (not ok))
          x
          nil))))
  (local (in-theory (enable bfr-check-false)))
  (defthm bfr-eval-of-bfr-check-false
    (implies (bfr-eval pathcond env)
      (equal (bfr-eval (bfr-check-false x pathcond)
          env)
        (bfr-eval x env)))
    :hints (("goal" :use ((:instance bfr-sat-unsat (prop x)) (:instance bfr-sat-unsat
           (prop (bfr-and pathcond x)))))))
  (defthm pbfr-depends-on-of-bfr-check-false
    (implies (not (pbfr-depends-on k p x))
      (not (pbfr-depends-on k
          p
          (bfr-check-false x pathcond))))))

(defsection bfr-force-check
  (defund bfr-force-check
    (x pathcond direction)
    (declare (xargs :guard t))
    (case direction
      ((t) (mv t (bfr-check-true x pathcond)))
      ((nil) (mv t (bfr-check-false x pathcond)))
      (otherwise (bfr-constcheck x pathcond))))
  (local (in-theory (enable bfr-force-check)))
  (defthm bfr-eval-of-bfr-force-check
    (b* (((mv ?pc-sat ?xx) (bfr-force-check x pathcond dir)))
      (implies (bfr-eval pathcond env)
        (and pc-sat
          (equal (bfr-eval xx env)
            (bfr-eval x env)))))
    :hints (("goal" :use ((:instance bfr-sat-unsat (prop x)) (:instance bfr-sat-unsat
           (prop (bfr-and pathcond x)))))))
  (defthm pbfr-depends-on-of-bfr-force-check
    (b* (((mv ?pc-sat ?xx) (bfr-force-check x pathcond dir)))
      (implies (not (pbfr-depends-on k p x))
        (not (pbfr-depends-on k p xx))))))

(encapsulate (((bfr-vacuity-check *) => (mv * * *)))
  (local (defun bfr-vacuity-check
      (prop)
      (declare (xargs :guard t))
      (mv nil nil prop)))
  (defthm bfr-vacuity-check-nvals
    (equal (len (bfr-vacuity-check prop)) 3))
  (defthm bfr-vacuity-check-true-listp
    (true-listp (bfr-vacuity-check prop)))
  (defthm bfr-vacuity-check-unsat
    (mv-let (sat succeeded ctrex)
      (bfr-vacuity-check prop)
      (declare (ignore ctrex))
      (implies (and succeeded (not sat))
        (not (bfr-eval prop env))))))

(defattach (bfr-vacuity-check bfr-sat)
  :hints (("goal" :use bfr-sat-unsat)))

(in-theory (disable bfr-vacuity-check-unsat bfr-sat-unsat))