		Search-engine friendly clone of the ACL2 documentation.

Smtlink-config

Make-smtlink-config

Basic constructor macro for smtlink-config structures.

Syntax

(make-smtlink-config [:interface-dir <interface-dir>] 
                     [:smt-module <smt-module>] 
                     [:smt-class <smt-class>] 
                     [:smt-cmd <smt-cmd>] 
                     [:pythonpath <pythonpath>])

This is the usual way to construct smtlink-config structures. It simply conses together a structure with the specified fields.

This macro generates a new smtlink-config structure from scratch. See also change-smtlink-config, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-smtlink-config

(defmacro make-smtlink-config (&rest args)
  (std::make-aggregate 'smtlink-config
                       args
                       '((:interface-dir . "")
                         (:smt-module . "")
                         (:smt-class . "")
                         (:smt-cmd . "")
                         (:pythonpath . ""))
                       'make-smtlink-config
                       nil))

Function: smtlink-config

(defun smtlink-config
       (interface-dir smt-module smt-class smt-cmd pythonpath)
  (declare (xargs :guard (and (stringp interface-dir)
                              (stringp smt-module)
                              (stringp smt-class)
                              (stringp smt-cmd)
                              (stringp pythonpath))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'smtlink-config))
    (declare (ignorable acl2::__function__))
    (b* ((interface-dir (mbe :logic (str-fix interface-dir)
                             :exec interface-dir))
         (smt-module (mbe :logic (str-fix smt-module)
                          :exec smt-module))
         (smt-class (mbe :logic (str-fix smt-class)
                         :exec smt-class))
         (smt-cmd (mbe :logic (str-fix smt-cmd)
                       :exec smt-cmd))
         (pythonpath (mbe :logic (str-fix pythonpath)
                          :exec pythonpath)))
      (list (cons 'interface-dir interface-dir)
            (cons 'smt-module smt-module)
            (cons 'smt-class smt-class)
            (cons 'smt-cmd smt-cmd)
            (cons 'pythonpath pythonpath)))))