|
|
|---|
|
|
|
|---|
Basic constructor macro for smtlink-hint structures.
(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.
This is an ordinary
Macro:
(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:
(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)))))