		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>] 
                   [:skip-toplevel-sat-check <skip-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)
    (:skip-toplevel-sat-check . fgl-config->skip-toplevel-sat-check)
    (:skip-vacuity-check . fgl-config->skip-vacuity-check))
  'change-fgl-config
  'remake-fgl-config))