header

(in-package "SMT")

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

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

(include-book "translator")

(defsection smt-header
  :parents (z3-py)
  :short "SMT-header contains string definitions for the header of a Z3 file."
  (local (in-theory (enable paragraphp wordp)))
  (define smt-head
    ((smt-conf smtlink-config-p))
    :returns (mv (head paragraphp)
      (import paragraphp))
    (b* ((smt-conf (mbe :logic (smtlink-config-fix smt-conf)
           :exec smt-conf)) ((smtlink-config c) smt-conf))
      (mv (list "from sys import path"
          #\

          "path.insert(1,""
          c.interface-dir
          "")"
          #\

          "path.insert(2,""
          c.pythonpath
          "")"
          #\

          "from "
          c.smt-module
          " import *"
          #\

          #\
)
        (list #\
 "_SMT_ = " c.smt-class "()" #\
)))))