config

(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 "std/util/defconsts" :dir :system)

(include-book "std/strings/top" :dir :system)

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

(value-triple (tshell-ensure))

(defsection smt-config
  :parents (verified)
  :short "Define default Smtlink config and custom Smtlink config"
  (defprod smtlink-config
    :parents (smt-config)
    ((interface-dir stringp
       :default ""
       "The directory to the customized Python file") (smt-module stringp :default "" "The file/Module name")
      (smt-class stringp :default "" "The Python class name")
      (smt-cmd stringp :default "" "The Python command")
      (pythonpath stringp
        :default ""
        "The PYTHONPATH to libraries")))
  (local (defthm all-boundp-of-initial-glb
      (implies (state-p x)
        (all-boundp *initial-global-table*
          (global-table x)))))
  (defconsts *default-smtlink-config*
    (b* ((sys-dir (system-books-dir state)) ((unless (stringp sys-dir)) (er hard?
            'smt-config=>*default-smtlink-config*
            "Failed to find ~
where the system books are."))
        (relative-smtlink-dir "projects/smtlink/z3_interface")
        (interface-dir (concatenate 'string sys-dir relative-smtlink-dir)))
      (make-smtlink-config :interface-dir interface-dir
        :smt-module "ACL2_to_Z3"
        :smt-class "ACL22SMT"
        :smt-cmd "python"
        :pythonpath "")))
  (encapsulate (((custom-smt-cnf) => *))
    (local (define custom-smt-cnf
        nil
        (make-smtlink-config)))
    (defthm smtlink-config-p-of-custom-smt-cnf
      (smtlink-config-p (custom-smt-cnf))))
  (define default-smtlink-config
    nil
    (change-smtlink-config *default-smtlink-config*))
  (defattach custom-smt-cnf
    default-smtlink-config)
  (defalist string-string-alist
    :key-type string
    :val-type string
    :pred string-string-alistp
    :true-listp t)
  (define check-valid-option
    ((option stringp) (value stringp))
    :returns (valid? booleanp)
    :ignore-ok t
    (b* (((unless (or (equal option "interface-dir")
            (equal option "smt-module")
            (equal option "smt-class")
            (equal option "smt-cmd")
            (equal option "pythonpath"))) nil))
      t))
  (define extract-=-left-and-right
    ((lines string-listp))
    :returns (config-alist string-string-alistp)
    :measure (len lines)
    :hints (("Goal" :in-theory (enable string-list-fix)))
    (b* ((lines (string-list-fix lines)) ((unless (consp lines)) nil)
        ((cons first rest) lines)
        (extracted-line (strtok first (list #\=)))
        ((unless (and (consp extracted-line)
             (endp (cddr extracted-line))
             (stringp (car extracted-line))
             (stringp (cadr extracted-line)))) (er hard?
            'smt-config=>extract-=-left-and-right
            "Smtlink-config wrong ~
  format!~%~q0"
            first))
        ((list option value &) extracted-line)
        ((unless (check-valid-option option value)) (er hard?
            'smt-config=>extract-=-left-and-right
            "There's something
  wrong with the configuration setup in smtlink-config.")))
      (cons `(,(CAR SMT::EXTRACTED-LINE) . ,(CADR SMT::EXTRACTED-LINE))
        (extract-=-left-and-right rest))))
  (define process-config
    ((config-str stringp))
    :returns (config-alist string-string-alistp)
    (b* ((lines (strtok config-str (list #\
))) (config-alist (extract-=-left-and-right lines)))
      config-alist))
  (define change-smt-cnf
    ((config-alist string-string-alistp) (default-cnf smtlink-config-p))
    :returns (smt-cnf smtlink-config-p)
    :measure (len config-alist)
    :hints (("Goal" :in-theory (enable string-string-alist-fix)))
    (b* ((config-alist (string-string-alist-fix config-alist)) (default-cnf (smtlink-config-fix default-cnf))
        ((unless (consp config-alist)) default-cnf)
        ((cons first rest) config-alist)
        ((cons option value) first)
        (new-cnf (cond ((equal option "smt-cmd") (change-smtlink-config default-cnf
                :smt-cmd value))
            (t default-cnf))))
      (change-smt-cnf rest new-cnf)))
  (define file-exists
    ((smtconfig stringp) (dir stringp) state)
    :returns (mv (exist? booleanp) state)
    (b* ((cmd (concatenate 'string "test -f " dir "/" smtconfig)) ((mv exit-status & state) (time$ (tshell-call cmd :print t :save t)
            :msg "; test -f: `~s0`: ~st sec, ~sa bytes~%"
            :args (list cmd))))
      (if (equal exit-status 0)
        (mv t state)
        (mv nil state))))
  (define find-smtlink-config
    ((smtconfig stringp) (state t))
    :returns (mv (dir stringp) state)
    (b* (((mv & smt_home state) (getenv$ "SMT_HOME" state)) ((mv exists-in-smt_home state) (if (stringp smt_home)
            (file-exists smtconfig smt_home state)
            (mv nil state)))
        ((if exists-in-smt_home) (prog2$ (cw "Reading smtlink-config from $SMT_HOME...~%")
            (mv smt_home state)))
        ((mv & home state) (getenv$ "HOME" state))
        ((mv exists-in-home state) (if (stringp home)
            (file-exists smtconfig home state)
            (mv nil state)))
        ((if exists-in-home) (prog2$ (cw "Reading smtlink-config from $HOME...~%")
            (mv home state)))
        ((mv & smtlink-pwd state) (getenv$ "PWD" state))
        ((mv exists-in-smtlink-pwd state) (if (stringp smtlink-pwd)
            (file-exists smtconfig
              smtlink-pwd
              state)
            (mv nil state)))
        ((if exists-in-smtlink-pwd) (prog2$ (cw "Reading smtlink-config from Smtlink directory...~%")
            (mv smtlink-pwd state))))
      (mv (prog2$ (er hard?
            'smt-config=>find-smtlink-config
            "Failed to find smtlink-config.~%")
          "")
        state)))
  (defconsts (*smt-cnf* state)
    (b* ((smtconfig "smtlink-config") ((mv dir state) (find-smtlink-config smtconfig state))
        (res (read-file-into-string (concatenate 'string dir "/" smtconfig)))
        ((unless res) (mv (default-smtlink-config) state))
        (config-alist (process-config res)))
      (mv (change-smt-cnf config-alist
          (default-smtlink-config))
        state)))
  (define default-smt-cnf nil *smt-cnf*))