		Search-engine friendly clone of the ACL2 documentation.

Fgl-config

Change-fgl-config

Modifying constructor for fgl-config structures.

Syntax

(change-fgl-config x 
                   [: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 an often useful alternative to make-fgl-config.

We construct a new fgl-config structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

Definition

This is an ordinary change- macro introduced by defprod.

Macro: change-fgl-config

(defmacro change-fgl-config (x &rest args)
  (std::change-aggregate
       'fgl-config
       x args
       '((:trace-rewrites . fgl-config->trace-rewrites)
         (:reclimit . fgl-config->reclimit)
         (:make-ites . fgl-config->make-ites)
         (:rewrite-rule-table . fgl-config->rewrite-rule-table)
         (:branch-merge-rules . fgl-config->branch-merge-rules)
         (:function-modes . fgl-config->function-modes)
         (:prof-enabledp . fgl-config->prof-enabledp)
         (:sat-config . fgl-config->sat-config)
         (:sat-config-vacuity . fgl-config->sat-config-vacuity)
         (:toplevel-sat-check . fgl-config->toplevel-sat-check)
         (:skip-vacuity-check . fgl-config->skip-vacuity-check))
       'change-fgl-config
       'remake-fgl-config))