		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>] 
                 [:make-ites <make-ites>] 
                 [:rewrite-rule-table <rewrite-rule-table>] 
                 [:branch-merge-rules <branch-merge-rules>] 
                 [:function-modes <function-modes>] 
                 [: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>])

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)
                         (:reclimit . 1000000)
                         (:make-ites)
                         (:rewrite-rule-table)
                         (:branch-merge-rules)
                         (:function-modes)
                         (:prof-enabledp . t)
                         (:sat-config)
                         (:sat-config-vacuity)
                         (:toplevel-sat-check . t)
                         (:skip-vacuity-check))
                       'make-fgl-config
                       nil))

Function: fgl-config

(defun fgl-config
       (trace-rewrites reclimit make-ites
                       rewrite-rule-table branch-merge-rules
                       function-modes prof-enabledp
                       sat-config sat-config-vacuity
                       toplevel-sat-check skip-vacuity-check)
 (declare
  (xargs
      :guard (and (booleanp trace-rewrites)
                  (posp reclimit)
                  (booleanp make-ites)
                  (fgl-function-mode-alist-p function-modes)
                  (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))
    (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))
    (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 reclimit)
       (std::prod-cons
            make-ites
            (std::prod-cons rewrite-rule-table branch-merge-rules)))
    (std::prod-cons
         (std::prod-cons function-modes
                         (std::prod-cons prof-enabledp sat-config))
         (std::prod-cons sat-config-vacuity
                         (std::prod-cons toplevel-sat-check
                                         skip-vacuity-check)))))))