		Search-engine friendly clone of the ACL2 documentation.

Vl-simpconfig

Change-vl-simpconfig

Modifying constructor for vl-simpconfig structures.

Syntax

(change-vl-simpconfig x 
                      [:compress-p <compress-p>] 
                      [:problem-mods <problem-mods>] 
                      [:already-annotated <already-annotated>] 
                      [:unroll-limit <unroll-limit>] 
                      [:sc-limit <sc-limit>] 
                      [:elab-limit <elab-limit>] 
                      [:uniquecase-conservative <uniquecase-conservative>] 
                      [:uniquecase-constraints <uniquecase-constraints>] 
                      [:enum-constraints <enum-constraints>] 
                      [:enum-fixups <enum-fixups>] 
                      [:sv-simplify <sv-simplify>] 
                      [:sv-simplify-verbosep <sv-simplify-verbosep>] 
                      [:sv-include-atts <sv-include-atts>] 
                      [:nb-latch-delay-hack <nb-latch-delay-hack>] 
                      [:name-without-default-params <name-without-default-params>] 
                      [:unparam-bad-instance-fatalp <unparam-bad-instance-fatalp>] 
                      [:defer-argresolve <defer-argresolve>] 
                      [:suppress-fatal-warning-types <suppress-fatal-warning-types>] 
                      [:user-paramsettings <user-paramsettings>] 
                      [:user-paramsettings-mode <user-paramsettings-mode>] 
                      [:pre-elab-topmods <pre-elab-topmods>] 
                      [:pre-elab-filter <pre-elab-filter>] 
                      [:post-elab-topmods <post-elab-topmods>] 
                      [:post-elab-filter <post-elab-filter>] 
                      [:allow-bad-topmods <allow-bad-topmods>])

This is an often useful alternative to make-vl-simpconfig.

We construct a new vl-simpconfig 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-vl-simpconfig

(defmacro change-vl-simpconfig (x &rest args)
 (std::change-aggregate
     'vl-simpconfig
     x args
     '((:compress-p . vl-simpconfig->compress-p)
       (:problem-mods . vl-simpconfig->problem-mods)
       (:already-annotated . vl-simpconfig->already-annotated)
       (:unroll-limit . vl-simpconfig->unroll-limit)
       (:sc-limit . vl-simpconfig->sc-limit)
       (:elab-limit . vl-simpconfig->elab-limit)
       (:uniquecase-conservative
            .
            vl-simpconfig->uniquecase-conservative)
       (:uniquecase-constraints
            . vl-simpconfig->uniquecase-constraints)
       (:enum-constraints . vl-simpconfig->enum-constraints)
       (:enum-fixups . vl-simpconfig->enum-fixups)
       (:sv-simplify . vl-simpconfig->sv-simplify)
       (:sv-simplify-verbosep . vl-simpconfig->sv-simplify-verbosep)
       (:sv-include-atts . vl-simpconfig->sv-include-atts)
       (:nb-latch-delay-hack . vl-simpconfig->nb-latch-delay-hack)
       (:name-without-default-params
            .
            vl-simpconfig->name-without-default-params)
       (:unparam-bad-instance-fatalp
            .
            vl-simpconfig->unparam-bad-instance-fatalp)
       (:defer-argresolve . vl-simpconfig->defer-argresolve)
       (:suppress-fatal-warning-types
            .
            vl-simpconfig->suppress-fatal-warning-types)
       (:user-paramsettings . vl-simpconfig->user-paramsettings)
       (:user-paramsettings-mode
            .
            vl-simpconfig->user-paramsettings-mode)
       (:pre-elab-topmods . vl-simpconfig->pre-elab-topmods)
       (:pre-elab-filter . vl-simpconfig->pre-elab-filter)
       (:post-elab-topmods . vl-simpconfig->post-elab-topmods)
       (:post-elab-filter . vl-simpconfig->post-elab-filter)
       (:allow-bad-topmods . vl-simpconfig->allow-bad-topmods))
     'change-vl-simpconfig
     'nil))