		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>] 
                 [:skip-toplevel-sat-check <skip-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)
                                 (:skip-toplevel-sat-check)
                                 (: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
                 skip-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)
                         (booleanp skip-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))
    (skip-toplevel-sat-check
         (mbe :logic (bool-fix skip-toplevel-sat-check)
              :exec skip-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 skip-toplevel-sat-check
                                         skip-vacuity-check)))))))