g-assert

(in-package "GL")

(include-book "bfr-sat")

(include-book "gl-mbe")

(include-book "g-primitives-help")

(include-book "g-if")

(include-book "eval-g-base")

(include-book "ctrex-utils")

(local (include-book "hyp-fix"))

(local (include-book "eval-g-base-help"))

(def-g-fn gl-assert-fn$inline
  `(b* (((mv x-nonnil x-unknown & hyp) (gtests x hyp)) (false (bfr-and (bfr-hyp->bfr hyp)
          (bfr-not x-unknown)
          (bfr-not x-nonnil)))
      ((mv false-sat false-succ ?false-ctrex) (bfr-sat false))
      (gmsg (if (general-concretep gmsg)
          (general-concrete-obj gmsg)
          "GL-ASSERT failed!"))
      ((when (and false-sat false-succ)) (make-fast-alist false-ctrex)
        (ec-call (glcp-print-single-ctrex false-ctrex
            "Error:"
            gmsg
            config
            bvar-db
            state))
        (er hard? 'gl-assert "~@0" gmsg)
        (g-if (gret x) (gret t) (gret nil)))
      ((when (not false-succ)) (er hard?
          'gl-assert
          "Assertion failed to prove.~%~@0"
          gmsg)
        (g-if (gret x) (gret t) (gret nil)))
      (unk (bfr-and (bfr-hyp->bfr hyp) x-unknown))
      ((mv unk-sat unk-succ ?unk-ctrex) (bfr-sat unk))
      ((when (and unk-sat unk-succ)) (er hard?
          'gl-assert
          "Assertion failed with unknown.~%~@0"
          gmsg)
        (g-if (gret x) (gret t) (gret nil)))
      ((when (not unk-succ)) (er hard?
          'gl-assert
          "Assertion failed to prove absence of unknowns.~%~@0"
          gmsg)
        (g-if (gret x) (gret t) (gret nil))))
    (gret t)))

(verify-g-guards gl-assert-fn$inline)

(local (defun instantiate-bfr-sat-hint
    (clause env)
    (if (atom clause)
      nil
      (let ((lit (car clause)))
        (case-match lit
          (('mv-nth ''0 ('bfr-sat term)) (cons `(:instance bfr-sat-unsat
                (prop ,GL::TERM)
                (env ,GL::ENV))
              (instantiate-bfr-sat-hint (cdr clause) env)))
          (& (instantiate-bfr-sat-hint (cdr clause) env)))))))

(def-gobj-dependency-thm gl-assert-fn$inline
  :hints `(("goal" :expand (,GL::GCALL)
     :in-theory (disable (:d ,GL::GFN)))))

(def-g-correct-thm gl-assert-fn$inline
  eval-g-base
  :hints `(("goal" :do-not-induct t
     :expand (,GL::GCALL)
     :in-theory (disable bfr-sat-unsat)) (and stable-under-simplificationp
      (let ((insts (instantiate-bfr-sat-hint clause '(car env))))
        (if insts
          `(:computed-hint-replacement t :use ,GL::INSTS)
          (cw "clause: ~x0~%" clause))))))