• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
    • Gl
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Fgl
      • Fgl-rewrite-rules
      • Fgl-function-mode
      • Fgl-object
      • Fgl-solving
      • Fgl-handling-if-then-elses
      • Fgl-counterexamples
      • Fgl-getting-bits-from-objects
      • Fgl-primitive-and-meta-rules
      • Fgl-interpreter-overview
      • Fgl-correctness-of-binding-free-variables
      • Fgl-debugging
      • Fgl-testbenches
      • Def-fgl-boolean-constraint
      • Fgl-stack
      • Def-fgl-param-thm
      • Fgl-rewrite-tracing
      • Def-fgl-thm
        • Fgl-config
          • Fgl-config-fix
          • Make-fgl-config
          • Fgl-config-p
          • Fgl-config->counterexample-analysis-enabledp
          • Change-fgl-config
          • Fgl-config-equiv
          • Fgl-config->toplevel-sat-check
          • Fgl-config->function-modes
          • Fgl-config->skip-vacuity-check
          • Fgl-config->trace-rewrites
          • Fgl-config->prof-enabledp
          • Fgl-config->steplimit
          • Fgl-config->stacklimit
          • Fgl-config->reclimit
          • Fgl-config->make-ites
          • Fgl-config->sat-config-vacuity
          • Fgl-config->rewrite-rule-table
          • Fgl-config->branch-merge-rules
          • Fgl-config->sat-config
          • Fgl-config->evisc-tuple
      • Fgl-fast-alist-support
      • Fgl-array-support
      • Advanced-equivalence-checking-with-fgl
      • Fgl-fty-support
      • Fgl-internals
    • Removable-runes
    • Efficiency
    • Rewrite-bounds
    • Bash
    • Def-dag-measure
    • Bdd
    • Remove-hyps
    • Contextual-rewriting
    • Simp
    • Rewrite$-hyps
    • Bash-term-to-dnf
    • Use-trivial-ancestors-check
    • Minimal-runes
    • Clause-processor-tools
    • Fn-is-body
    • Without-subsumption
    • Rewrite-equiv-hint
    • Def-bounds
    • Rewrite$-context
    • Try-gl-concls
    • Hint-utils
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Fgl-config

Change-fgl-config

Modifying constructor for fgl-config structures.

Syntax

(change-fgl-config x 
                   [:trace-rewrites <trace-rewrites>] 
                   [:reclimit <reclimit>] 
                   [:stacklimit <stacklimit>] 
                   [:steplimit <steplimit>] 
                   [:make-ites <make-ites>] 
                   [:rewrite-rule-table <rewrite-rule-table>] 
                   [:branch-merge-rules <branch-merge-rules>] 
                   [:function-modes <function-modes>] 
                   [:counterexample-analysis-enabledp <counterexample-analysis-enabledp>] 
                   [: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>] 
                   [:evisc-tuple <evisc-tuple>]) 

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)
         (:stacklimit . fgl-config->stacklimit)
         (:steplimit . fgl-config->steplimit)
         (: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)
         (:counterexample-analysis-enabledp
              .
              fgl-config->counterexample-analysis-enabledp)
         (: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)
         (:evisc-tuple . fgl-config->evisc-tuple))
       'change-fgl-config
       'remake-fgl-config))