		Search-engine friendly clone of the ACL2 documentation.

Trusted

Smt-run

SMT-run runs the configured SMT solver then interprets the result and feed it back to ACL2.

Definitions and Theorems

Function: smt-run

(defun smt-run (fname smt-conf state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (stringp fname)
                              (smtlink-config-p smt-conf))))
  (let ((acl2::__function__ 'smt-run))
    (declare (ignorable acl2::__function__))
    (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)))))

Theorem: natp-of-smt-run.exit-status

(defthm natp-of-smt-run.exit-status
  (b* (((mv ?exit-status ?lines acl2::?state)
        (smt-run fname smt-conf state)))
    (natp exit-status))
  :rule-classes :rewrite)

Theorem: string-listp-of-smt-run.lines

(defthm string-listp-of-smt-run.lines
  (b* (((mv ?exit-status ?lines acl2::?state)
        (smt-run fname smt-conf state)))
    (string-listp lines))
  :rule-classes :rewrite)

Theorem: state-p1-of-smt-run.state

(defthm state-p1-of-smt-run.state
  (implies (state-p1 state)
           (b* (((mv ?exit-status ?lines acl2::?state)
                 (smt-run fname smt-conf state)))
             (state-p1 state)))
  :rule-classes :rewrite)

Function: smt-interpret

(defun smt-interpret (fname rm-file smt-conf state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (stringp fname)
                             (booleanp rm-file)
                             (smtlink-config-p smt-conf))))
 (declare (xargs :stobjs state))
 (let ((acl2::__function__ 'smt-interpret))
  (declare (ignorable acl2::__function__))
  (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))))

Theorem: booleanp-of-smt-interpret.proved?

(defthm booleanp-of-smt-interpret.proved?
  (b* (((mv ?proved? acl2::?state)
        (smt-interpret fname rm-file smt-conf state)))
    (booleanp proved?))
  :rule-classes :rewrite)