trusted-cp

(in-package "SMT")

(include-book "std/util/bstar" :dir :system)

(include-book "prove")

(set-state-ok t)

(defsection smt-trusted-cp
  :parents (trusted)
  :short "The trusted clause processor"
  (defstub smt-prove-stub
    (term smtlink-hint state)
    (mv t nil state))
  (program)
  (defttag :smtlink)
  (progn (progn! (set-raw-mode-on state)
      (defun smt-prove-stub
        (term smtlink-hint state)
        (smt-prove term smtlink-hint state)))
    (define smt-trusted-cp-main
      ((cl pseudo-term-listp) (smtlink-hint)
        (custom-p booleanp)
        state)
      :stobjs state
      :mode :program (b* ((smt-cnf (if custom-p
             (custom-smt-cnf)
             (default-smt-cnf))) (smtlink-hint (change-smtlink-hint smtlink-hint
              :smt-cnf smt-cnf))
          ((mv res smt-precond state) (smt-prove-stub (disjoin cl)
              smtlink-hint
              state))
          (subgoal-lst `(((hint-please '(:in-theory (enable magic-fix hint-please type-hyp)
                  :expand ((:free (x) (hide x))))) ,SMT::SMT-PRECOND
               ,(SMT::DISJOIN SMT::CL)))))
        (if res
          (prog2$ (cw "Proved!~%")
            (mv nil subgoal-lst state))
          (mv (cons "NOTE: Unable to prove goal with ~
                      SMT-trusted-cp and indicated hint."
              nil)
            (list cl)
            state))))
    (push-untouchable smt-prove-stub t))
  (logic)
  (define smt-trusted-cp
    ((cl pseudo-term-listp) (smtlink-hint smtlink-hint-p)
      state)
    :mode :program :stobjs state
    (prog2$ (cw "Using default SMT-trusted-cp...~%")
      (smt-trusted-cp-main cl
        smtlink-hint
        nil
        state)))
  (define smt-trusted-cp-custom
    ((cl pseudo-term-listp) (smtlink-hint smtlink-hint-p)
      state)
    :mode :program :stobjs state
    (prog2$ (cw "Using custom SMT-trusted-cp...~%")
      (smt-trusted-cp-main cl
        smtlink-hint
        t
        state)))
  (define-trusted-clause-processor smt-trusted-cp
    nil
    :ttag smtlink)
  (define-trusted-clause-processor smt-trusted-cp-custom
    nil
    :ttag smtlink-custom))