Basic constructor macro for obs-constprop-config structures.
(make-obs-constprop-config [:gatesimp <gatesimp>] [:constprop-iterations <constprop-iterations>] [:obs-hyp-max-size <obs-hyp-max-size>] [:obs-concl-min-size <obs-concl-min-size>] [:obs-min-ratio <obs-min-ratio>])
This is the usual way to construct obs-constprop-config structures. It simply conses together a structure with the specified fields.
This macro generates a new obs-constprop-config structure from scratch. See also change-obs-constprop-config, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-obs-constprop-config (&rest args) (std::make-aggregate 'obs-constprop-config args '((:gatesimp default-gatesimp) (:constprop-iterations . 1) (:obs-hyp-max-size . 3000) (:obs-concl-min-size . 5000) (:obs-min-ratio . 10)) 'make-obs-constprop-config nil))
Function:
(defun obs-constprop-config (gatesimp constprop-iterations obs-hyp-max-size obs-concl-min-size obs-min-ratio) (declare (xargs :guard (and (gatesimp-p gatesimp) (natp constprop-iterations) (acl2::maybe-natp obs-hyp-max-size) (acl2::maybe-natp obs-concl-min-size) (rationalp obs-min-ratio)))) (declare (xargs :guard t)) (let ((__function__ 'obs-constprop-config)) (declare (ignorable __function__)) (b* ((gatesimp (mbe :logic (gatesimp-fix gatesimp) :exec gatesimp)) (constprop-iterations (mbe :logic (nfix constprop-iterations) :exec constprop-iterations)) (obs-hyp-max-size (mbe :logic (acl2::maybe-natp-fix obs-hyp-max-size) :exec obs-hyp-max-size)) (obs-concl-min-size (mbe :logic (acl2::maybe-natp-fix obs-concl-min-size) :exec obs-concl-min-size)) (obs-min-ratio (mbe :logic (rfix obs-min-ratio) :exec obs-min-ratio))) (cons :obs-constprop-config (list (cons 'gatesimp gatesimp) (cons 'constprop-iterations constprop-iterations) (cons 'obs-hyp-max-size obs-hyp-max-size) (cons 'obs-concl-min-size obs-concl-min-size) (cons 'obs-min-ratio obs-min-ratio))))))