		Search-engine friendly clone of the ACL2 documentation.

Fgl-config

Make-fgl-config

Basic constructor macro for fgl-config structures.

Syntax

(make-fgl-config [:trace-rewrites <trace-rewrites>] 
                 [:reclimit <reclimit>] 
                 [:stacklimit <stacklimit>] 
                 [:steplimit <steplimit>] 
                 [:make-ites <make-ites>] 
                 [:rewrite-rule-table <rewrite-rule-table>] 
                 [:branch-merge-rules <branch-merge-rules>] 
                 [:function-modes <function-modes>] 
                 [:counterexample-analysis-enabledp <counterexample-analysis-enabledp>] 
                 [:prof-enabledp <prof-enabledp>] 
                 [:sat-config <sat-config>] 
                 [:sat-config-vacuity <sat-config-vacuity>] 
                 [:toplevel-sat-check <toplevel-sat-check>] 
                 [:skip-vacuity-check <skip-vacuity-check>] 
                 [:evisc-tuple <evisc-tuple>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-fgl-config

(defmacro make-fgl-config (&rest args)
  (std::make-aggregate 'fgl-config
                       args
                       '((:trace-rewrites quote nil)
                         (:reclimit quote 1000000)
                         (:stacklimit quote 1000000)
                         (:steplimit quote 1000000000)
                         (:make-ites quote nil)
                         (:rewrite-rule-table)
                         (:branch-merge-rules)
                         (:function-modes)
                         (:counterexample-analysis-enabledp quote t)
                         (:prof-enabledp quote t)
                         (:sat-config)
                         (:sat-config-vacuity)
                         (:toplevel-sat-check quote t)
                         (:skip-vacuity-check quote nil)
                         (:evisc-tuple quote (nil 12 100 nil)))
                       'make-fgl-config
                       nil))

Function: fgl-config

(defun fgl-config
       (trace-rewrites reclimit stacklimit
                       steplimit make-ites rewrite-rule-table
                       branch-merge-rules function-modes
                       counterexample-analysis-enabledp
                       prof-enabledp sat-config
                       sat-config-vacuity toplevel-sat-check
                       skip-vacuity-check evisc-tuple)
 (declare
  (xargs
      :guard (and (booleanp trace-rewrites)
                  (posp reclimit)
                  (posp stacklimit)
                  (posp steplimit)
                  (booleanp make-ites)
                  (fgl-function-mode-alist-p function-modes)
                  (booleanp counterexample-analysis-enabledp)
                  (booleanp prof-enabledp)
                  (fgl-toplevel-sat-check-mode-p toplevel-sat-check)
                  (booleanp skip-vacuity-check))))
 (declare (xargs :guard t))
 (let ((__function__ 'fgl-config))
  (declare (ignorable __function__))
  (b*
   ((trace-rewrites (mbe :logic (bool-fix trace-rewrites)
                         :exec trace-rewrites))
    (reclimit (mbe :logic (pos-fix reclimit)
                   :exec reclimit))
    (stacklimit (mbe :logic (pos-fix stacklimit)
                     :exec stacklimit))
    (steplimit (mbe :logic (pos-fix steplimit)
                    :exec steplimit))
    (make-ites (mbe :logic (bool-fix make-ites)
                    :exec make-ites))
    (function-modes
         (mbe :logic (fgl-function-mode-alist-fix function-modes)
              :exec function-modes))
    (counterexample-analysis-enabledp
         (mbe :logic (bool-fix counterexample-analysis-enabledp)
              :exec counterexample-analysis-enabledp))
    (prof-enabledp (mbe :logic (bool-fix prof-enabledp)
                        :exec prof-enabledp))
    (toplevel-sat-check
     (mbe
         :logic (fgl-toplevel-sat-check-mode-fix toplevel-sat-check)
         :exec toplevel-sat-check))
    (skip-vacuity-check (mbe :logic (bool-fix skip-vacuity-check)
                             :exec skip-vacuity-check)))
   (std::prod-cons
    (std::prod-cons
       (std::prod-cons trace-rewrites
                       (std::prod-cons reclimit stacklimit))
       (std::prod-cons
            (std::prod-cons steplimit make-ites)
            (std::prod-cons rewrite-rule-table branch-merge-rules)))
    (std::prod-cons
         (std::prod-cons
              (std::prod-cons function-modes
                              counterexample-analysis-enabledp)
              (std::prod-cons prof-enabledp sat-config))
         (std::prod-cons
              (std::prod-cons sat-config-vacuity toplevel-sat-check)
              (std::prod-cons skip-vacuity-check evisc-tuple)))))))