		Search-engine friendly clone of the ACL2 documentation.

Smtlink-hint

Make-smtlink-hint

Basic constructor macro for smtlink-hint structures.

Syntax

(make-smtlink-hint [:functions <functions>] 
                   [:hypotheses <hypotheses>] 
                   [:main-hint <main-hint>] 
                   [:let-binding <let-binding>] 
                   [:symbols <symbols>] 
                   [:abs <abs>] 
                   [:fty <fty>] 
                   [:fty-info <fty-info>] 
                   [:fty-types <fty-types>] 
                   [:int-to-rat <int-to-rat>] 
                   [:smt-dir <smt-dir>] 
                   [:rm-file <rm-file>] 
                   [:smt-fname <smt-fname>] 
                   [:smt-params <smt-params>] 
                   [:fast-functions <fast-functions>] 
                   [:type-decl-list <type-decl-list>] 
                   [:expanded-clause-w/-hint <expanded-clause-w/-hint>] 
                   [:expanded-g/type <expanded-g/type>] 
                   [:smt-cnf <smt-cnf>] 
                   [:wrld-fn-len <wrld-fn-len>] 
                   [:custom-p <custom-p>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-smtlink-hint

(defmacro make-smtlink-hint (&rest args)
  (std::make-aggregate 'smtlink-hint
                       args
                       '((:functions)
                         (:hypotheses)
                         (:main-hint)
                         (:let-binding make-let-binding)
                         (:symbols)
                         (:abs)
                         (:fty)
                         (:fty-info)
                         (:fty-types)
                         (:int-to-rat)
                         (:smt-dir . "")
                         (:rm-file . t)
                         (:smt-fname . "")
                         (:smt-params)
                         (:fast-functions)
                         (:type-decl-list)
                         (:expanded-clause-w/-hint make-hint-pair)
                         (:expanded-g/type)
                         (:smt-cnf make-smtlink-config)
                         (:wrld-fn-len . 0)
                         (:custom-p))
                       'make-smtlink-hint
                       nil))

Function: smtlink-hint

(defun smtlink-hint
       (functions hypotheses main-hint let-binding
                  symbols abs fty fty-info fty-types
                  int-to-rat smt-dir rm-file smt-fname
                  smt-params fast-functions type-decl-list
                  expanded-clause-w/-hint expanded-g/type
                  smt-cnf wrld-fn-len custom-p)
 (declare (xargs :guard (and (func-listp functions)
                             (hint-pair-listp hypotheses)
                             (true-listp main-hint)
                             (let-binding-p let-binding)
                             (symbol-listp symbols)
                             (symbol-listp abs)
                             (symbol-listp fty)
                             (fty-info-alist-p fty-info)
                             (fty-types-p fty-types)
                             (booleanp int-to-rat)
                             (stringp smt-dir)
                             (booleanp rm-file)
                             (stringp smt-fname)
                             (true-listp smt-params)
                             (func-alistp fast-functions)
                             (pseudo-termp type-decl-list)
                             (hint-pair-p expanded-clause-w/-hint)
                             (pseudo-termp expanded-g/type)
                             (smtlink-config-p smt-cnf)
                             (natp wrld-fn-len)
                             (booleanp custom-p))))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'smtlink-hint))
   (declare (ignorable acl2::__function__))
   (b*
     ((functions (mbe :logic (func-list-fix functions)
                      :exec functions))
      (hypotheses (mbe :logic (hint-pair-list-fix hypotheses)
                       :exec hypotheses))
      (main-hint (mbe :logic (true-list-fix main-hint)
                      :exec main-hint))
      (let-binding (mbe :logic (let-binding-fix let-binding)
                        :exec let-binding))
      (symbols (mbe :logic (symbol-list-fix symbols)
                    :exec symbols))
      (abs (mbe :logic (symbol-list-fix abs)
                :exec abs))
      (fty (mbe :logic (symbol-list-fix fty)
                :exec fty))
      (fty-info (mbe :logic (fty-info-alist-fix fty-info)
                     :exec fty-info))
      (fty-types (mbe :logic (fty-types-fix fty-types)
                      :exec fty-types))
      (int-to-rat (mbe :logic (acl2::bool-fix int-to-rat)
                       :exec int-to-rat))
      (smt-dir (mbe :logic (str-fix smt-dir)
                    :exec smt-dir))
      (rm-file (mbe :logic (acl2::bool-fix rm-file)
                    :exec rm-file))
      (smt-fname (mbe :logic (str-fix smt-fname)
                      :exec smt-fname))
      (smt-params (mbe :logic (true-list-fix smt-params)
                       :exec smt-params))
      (fast-functions (mbe :logic (func-alist-fix fast-functions)
                           :exec fast-functions))
      (type-decl-list (mbe :logic (pseudo-term-fix type-decl-list)
                           :exec type-decl-list))
      (expanded-clause-w/-hint
           (mbe :logic (hint-pair-fix expanded-clause-w/-hint)
                :exec expanded-clause-w/-hint))
      (expanded-g/type (mbe :logic (pseudo-term-fix expanded-g/type)
                            :exec expanded-g/type))
      (smt-cnf (mbe :logic (smtlink-config-fix smt-cnf)
                    :exec smt-cnf))
      (wrld-fn-len (mbe :logic (nfix wrld-fn-len)
                        :exec wrld-fn-len))
      (custom-p (mbe :logic (acl2::bool-fix custom-p)
                     :exec custom-p)))
     (list (cons 'functions functions)
           (cons 'hypotheses hypotheses)
           (cons 'main-hint main-hint)
           (cons 'let-binding let-binding)
           (cons 'symbols symbols)
           (cons 'abs abs)
           (cons 'fty fty)
           (cons 'fty-info fty-info)
           (cons 'fty-types fty-types)
           (cons 'int-to-rat int-to-rat)
           (cons 'smt-dir smt-dir)
           (cons 'rm-file rm-file)
           (cons 'smt-fname smt-fname)
           (cons 'smt-params smt-params)
           (cons 'fast-functions fast-functions)
           (cons 'type-decl-list type-decl-list)
           (cons 'expanded-clause-w/-hint
                 expanded-clause-w/-hint)
           (cons 'expanded-g/type expanded-g/type)
           (cons 'smt-cnf smt-cnf)
           (cons 'wrld-fn-len wrld-fn-len)
           (cons 'custom-p custom-p)))))