prove

(in-package "SMT")

(include-book "centaur/fty/top" :dir :system)

(include-book "xdoc/top" :dir :system)

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

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

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

(include-book "../verified/expand-cp")

(include-book "../config")

(include-book "./run")

(include-book "./write")

(include-book "./z3-py/names")

(include-book "./z3-py/translator")

(include-book "./z3-py/header")

(defttag :tshell)

(value-triple (tshell-ensure))

(defsection smt-prove
  :parents (trusted)
  :short "SMT-prove is the main functions for transliteration into SMT languages and calling the external SMT solver."
  (encapsulate nil
    (local (defthm lemma-1
        (implies (and (string-listp x) x)
          (consp x))))
    (local (defthm lemma-2
        (b* (((mv ?exit-status ?lines) (tshell-call cmd :print print :save save)))
          (implies lines (consp lines)))))
    (local (defthm lemma-3
        (implies (and (string-listp x) x)
          (stringp (car x)))))
    (local (defthm lemma-4
        (b* (((mv ?exit-status ?lines) (tshell-call cmd :print print :save save)))
          (implies lines (stringp (car lines))))))
    (local (in-theory (enable string-or-symbol-p)))
    (define make-fname
      ((dir stringp) (fname stringp) state)
      :returns (mv (full-fname stringp) state)
      :guard-debug t
      (b* ((dir (str-fix dir)) (fname (str-fix fname))
          (dir (if (equal dir "")
              "/tmp/py_file"
              dir))
          ((unless (equal fname "")) (mv (concatenate 'string dir "/" fname)
              state))
          (cmd (concatenate 'string
              "mkdir -p "
              dir
              " && "
              "mktemp "
              dir
              "/smtlink.XXXXX")))
        (mv-let (exit-status lines state)
          (time$ (tshell-call cmd :print nil :save t)
            :msg ""
            :args (list cmd))
          (if (and (equal exit-status 0)
              (not (equal lines nil)))
            (mv (car lines) state)
            (prog2$ (er hard?
                'smt-prove=>make-fname
                "Error: Command ~x0 ~
                                                      failed."
                cmd)
              (mv "" state)))))))
  (define smt-prove
    ((term pseudo-termp) (smtlink-hint smtlink-hint-p)
      (state))
    :mode :program (b* ((term (pseudo-term-fix term)) (smtlink-hint (smtlink-hint-fix smtlink-hint))
        (flextypes-table (table-alist 'flextypes-table (w state)))
        ((unless (alistp flextypes-table)) (mv nil nil state))
        (smtlink-hint1 (generate-fty-info-alist smtlink-hint
            flextypes-table))
        (smtlink-hint2 (generate-fty-types-top smtlink-hint1
            flextypes-table))
        ((smtlink-hint h) smtlink-hint2)
        (c h.smt-cnf)
        ((mv smt-file state) (make-fname h.smt-dir h.smt-fname state))
        ((mv smt-term smt-precond) (smt-translation term h state))
        ((mv head import) (smt-head c))
        (state (smt-write-file smt-file
            head
            import
            smt-term
            state))
        ((mv result state) (smt-interpret smt-file
            h.rm-file
            c
            state)))
      (mv result smt-precond state))))