run

(in-package "SMT")

(include-book "std/io/read-string" :dir :system)

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

(include-book "system/f-put-global" :dir :system)

(include-book "../verified/hint-interface")

(defttag :tshell)

(value-triple (tshell-ensure))

(defttag :read-string)

(set-state-ok t)

(defsection smt-run
  :parents (trusted)
  :short "SMT-run runs the configured SMT solver then interprets the result and feed it back to ACL2."
  (define smt-run
    ((fname stringp) (smt-conf smtlink-config-p)
      state)
    :returns (mv (exit-status natp)
      (lines string-listp)
      (state state-p1 :hyp (state-p1 state)))
    (let ((cmd (concatenate 'string
           (smtlink-config->smt-cmd smt-conf)
           " "
           fname)))
      (time$ (tshell-call cmd :print nil :save t)
        :msg "; SMT solver: `~s0`: ~st sec, ~sa bytes~%"
        :args (list cmd))))
  (define smt-interpret
    ((fname stringp) (rm-file booleanp)
      (smt-conf smtlink-config-p)
      (state))
    (declare (xargs :stobjs state))
    :returns (mv (proved? booleanp) (state))
    :verify-guards nil
    (b* (((mv exit-status lines state) (smt-run fname smt-conf state)) ((unless (equal exit-status 0)) (mv (er hard?
              'smt-run=>smt-interpret
              "Z3 failure: ~q0"
              lines)
            state))
        ((if (equal lines nil)) (mv (er hard?
              'smt-run=>smt-interpret
              "Nothing returned from SMT solver.")
            state))
        ((if (equal (car lines) "proved")) (b* (((unless (equal rm-file nil)) (mv t state)) (cmd (concatenate 'string "rm -f " fname))
              ((mv exit-status-rm lines-rm state) (time$ (tshell-call cmd :print nil :save t)
                  :msg ""
                  :args (list cmd))))
            (if (equal exit-status-rm 0)
              (mv t state)
              (mv (er hard?
                  'smt-run=>smt-interpret
                  "Remove file error.~% ~p0~%"
                  lines-rm)
                state))))
        ((mv err str state) (read-string (car lines) nil :state state))
        ((unless (equal err nil)) (prog2$ (er hard?
              'smt-run=>smt-interpret
              "Read-string error.~%~p0~%"
              err)
            (mv nil state)))
        ((unless (and (true-listp str)
             (listp (car str))
             (equal (caar str) 'quote)
             (consp (cdar str)))) (prog2$ (er hard?
              'smt-run=>smt-interpret
              "We can't prove anything about the ~
thing returned by read-string. So we add a check for it. It's surprising that ~
the check for (true-listp str) and (consp (car str)) failed: ~q0"
              str)
            (mv nil state)))
        (- (cw "Possible counter-example found: ~p0~%One can access it ~
                 through global variable SMT-cex by doing (@ SMT-cex).~%"
            (unquote (car str))))
        (state (f-put-global 'smt-cex nil state))
        (state (f-put-global 'smt-cex (car str) state)))
      (mv nil state)))
  (encapsulate nil
    (local (defthm endp-of-not-consp-of-string-listp
        (implies (and (string-listp x) (not (consp x)))
          (not x))
        :rule-classes nil))
    (local (defthm stringp-of-consp-of-string-listp
        (implies (and (string-listp x) (consp x))
          (stringp (car x)))
        :rule-classes nil))
    (verify-guards smt-interpret
      :guard-debug t
      :hints (("goal" :in-theory (disable f-put-global)
         :use ((:instance endp-of-not-consp-of-string-listp
            (x (mv-nth 1
                (smt-run fname smt-conf state)))) (:instance stringp-of-consp-of-string-listp
             (x (mv-nth 1
                 (smt-run fname smt-conf state))))))))))