		Search-engine friendly clone of the ACL2 documentation.

Z3-py

Smt-header

SMT-header contains string definitions for the header of a Z3 file.

Definitions and Theorems

Function: smt-head

(defun smt-head (smt-conf)
  (declare (xargs :guard (smtlink-config-p smt-conf)))
  (let ((acl2::__function__ 'smt-head))
    (declare (ignorable acl2::__function__))
    (b* ((smt-conf (mbe :logic (smtlink-config-fix smt-conf)
                        :exec smt-conf))
         ((smtlink-config c) smt-conf))
      (mv (list "from sys import path" #\Newline
                "path.insert(1,\"" c.interface-dir "\")"
                #\Newline "path.insert(2,\"" c.pythonpath
                "\")" #\Newline "from " c.smt-module
                " import *" #\Newline #\Newline)
          (list #\Newline "_SMT_ = "
                c.smt-class "()" #\Newline)))))

Theorem: paragraphp-of-smt-head.head

(defthm paragraphp-of-smt-head.head
  (b* (((mv ?head common-lisp::?import)
        (smt-head smt-conf)))
    (paragraphp head))
  :rule-classes :rewrite)

Theorem: paragraphp-of-smt-head.import

(defthm paragraphp-of-smt-head.import
  (b* (((mv ?head common-lisp::?import)
        (smt-head smt-conf)))
    (paragraphp import))
  :rule-classes :rewrite)