• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
      • Z3-installation
      • Smt-hint
      • Tutorial
      • Status
      • Developer
        • Verified
        • Trusted
          • Translation-datatypes
          • Smt-run
          • Smt-prove
          • Smt-write
          • Smt-trusted-cp
          • Z3-py
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Trusted

Smt-prove

SMT-prove is the main functions for transliteration into SMT languages and calling the external SMT solver.

Definitions and Theorems

Function: make-fname

(defun make-fname (dir fname state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (stringp dir) (stringp fname))))
 (let ((acl2::__function__ 'make-fname))
  (declare (ignorable acl2::__function__))
  (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)))))))

Theorem: stringp-of-make-fname.full-fname

(defthm stringp-of-make-fname.full-fname
  (b* (((mv ?full-fname acl2::?state)
        (make-fname dir fname state)))
    (stringp full-fname))
  :rule-classes :rewrite)

Function: smt-prove

(defun smt-prove (term smtlink-hint state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp term)
                             (smtlink-hint-p smtlink-hint))))
 (let ((acl2::__function__ 'smt-prove))
   (declare (ignorable acl2::__function__))
   (b* ((term (pseudo-term-fix term))
        (smtlink-hint (smtlink-hint-fix smtlink-hint))
        (flextypes-table (table-alist 'fty::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))))