• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
        • Aignet-copy-init
        • Aignet-simplify-with-tracking
        • Aignet-simplify-marked-with-tracking
        • Aignet-cnf
        • Aignet-simplify-marked
        • Aignet-complete-copy
        • Aignet-transforms
          • Aignet-output-ranges
          • Aignet-comb-transforms
            • Fraig
              • Fraig-config
                • Make-fraig-config
                • Fraig-config-fix
                • Fraig-config-p
                • Change-fraig-config
                  • Fraig-config-equiv
                  • Fraig-config->save-candidate-equivs-as
                  • Fraig-config->remove-candidate-equivs
                  • Fraig-config->ipasir-recycle-count
                  • Fraig-config->delete-class-on-fail
                  • Fraig-config->ctrex-queue-limit
                  • Fraig-config->random-seed-name
                  • Fraig-config->output-types
                  • Fraig-config->initial-sim-words
                  • Fraig-config->initial-sim-rounds
                  • Fraig-config->final-force-resim
                  • Fraig-config->ctrex-force-resim
                  • Fraig-config->miters-only
                  • Fraig-config->level-limit
                  • Fraig-config->ipasir-limit
                  • Fraig-config->sim-words
                  • Fraig-config->outs-only
                  • Fraig-config->gatesimp
                • Fraig-sweep-node
                • Fraig-sweep-aux
                • Fraig-finish-copy-nonstrict
                • Fraig-core-aux
                • Fraig-output-type
                • Ipasir-check-aignet-equivalence
                • Fraig-store-ctrex-aux
                • Fraig-finish-copy-outs
                • Fraig-core
                • Fraig-ctrexes-maybe-resim
                • Fraig-sweep
                • Fraig-store-ctrex
                • S32v-row-repeat-bitcols
                • Fraig-ctrexes-resim-aux
                • Fraig-config-normalized-output-map
                • S32v-copy-cares
                • Ipasir-maybe-recycle
                • Fraig-ctrexes-ok
                • Fraig-add-equiv-class-outputs-aux-2
                • Fraig-add-equiv-class-outputs-aux-1
                • Fraig-ctrexes-resim
                • Fraig-create-aignet-node-mask
                • Fraig-classes-maybe-delete-class
                • Aignet-copy-outs-range
                • Fraig-record-sat-ctrex-rec
                • Fraig-ctrex-has-relevant-disagreement
                • S32v-bitcol-nth-set
                • Fraig-output-map-mark-non-simplified
                • Fraig-output-map-mark-simplified
                • Fraig-output-map-initial-equiv-start/count
                • Fraig-minimize-sat-ctrex-rec
                • Fraig-create-output-map
                • Bitarr-copy-cares-to-s32v-col
                • S32v-install-bit
                • S32v-bitcol-count-set
                • Fraig-ctrexes-init
                • Bitarr-or-cares-with-s32v-col
                • Fraig-ctrex-find-agreeable
                • S32v-repeat-bitcols
                • S32v-add-salt
                • Bitarr-remove-marked
                • Print-fraig-stats-noninitial
                • Fraig-ctrex-regvals->vecsim
                • Fraig-ctrex-invals->vecsim
                • Bitarr-to-s32v-col
                • Fraig-output-map-entry
                • Aignet-unmark-higher-levels
                • Aignet-mark-output-node-range
                • Fraig-initial-sim
                • Fraig-ctrexes-reinit
                • Fraig-add-equiv-class-outputs
                • Aignet-maybe-update-refs
                • S32v-randomize-rows
                • S32v-get-bit
                • Fraig-level-limit-ok
                • Aignet-vals->regvals-after-invals
                • Aignet-mark-fanout-cones-of-marked
                • Fraig-debug-output-ranges
                • S32v-zero-rows
                • Fraig-output-map-total-count
                • Fraig-output-map-has-multiple-initial-equivs
                • Fraig-output-map-has-initial-equivs
                • Fraig-output-type-map
                • Aignet-vals->in/regvals
                • Fraig-output-map
                • Fraig-total-checks
                • Fraig-stats-count-sat-call
                • Fraig-ctrex-ncols
                • Fraig-ctrex-data-rows
                • Fraig-stats-update-last-chance
                • Print-fraig-stats-initial
                • Print-classes-counts-with-mark
                • Fraig-stats-increment-forced-proved
                • Fraig-stats-increment-coincident-nodes
                • Print-classes-counts
                • Fraig-ctrex-in/reg-rows
              • Parametrize
              • Observability-fix
              • Constprop
              • Apply-m-assumption-n-output-output-transform-default
              • Balance
              • Apply-n-output-comb-transform-default
              • Apply-comb-transform-default
              • Obs-constprop
              • Rewrite
              • Comb-transform
              • Abc-comb-simplify
              • Prune
              • Rewrite!
              • M-assumption-n-output-comb-transform->name
              • N-output-comb-transform->name
              • Comb-transform->name
              • N-output-comb-transformlist
              • M-assumption-n-output-comb-transformlist
              • Comb-transformlist
              • Apply-comb-transform
            • Aignet-m-assumption-n-output-transforms
            • Aignet-n-output-comb-transforms
          • Aignet-eval
          • Semantics
          • Aignet-read-aiger
          • Aignet-write-aiger
          • Aignet-abc-interface
          • Utilities
        • Aig
        • Satlink
        • Truth
        • Ubdds
        • Bdd
        • Faig
        • Bed
        • 4v
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Fraig-config

    Change-fraig-config

    Modifying constructor for fraig-config structures.

    Syntax
    (change-fraig-config x 
                         [:initial-sim-words <initial-sim-words>] 
                         [:initial-sim-rounds <initial-sim-rounds>] 
                         [:sim-words <sim-words>] 
                         [:ipasir-limit <ipasir-limit>] 
                         [:ipasir-recycle-count <ipasir-recycle-count>] 
                         [:ctrex-queue-limit <ctrex-queue-limit>] 
                         [:ctrex-force-resim <ctrex-force-resim>] 
                         [:final-force-resim <final-force-resim>] 
                         [:random-seed-name <random-seed-name>] 
                         [:outs-only <outs-only>] 
                         [:miters-only <miters-only>] 
                         [:delete-class-on-fail <delete-class-on-fail>] 
                         [:gatesimp <gatesimp>] 
                         [:level-limit <level-limit>] 
                         [:output-types <output-types>] 
                         [:save-candidate-equivs-as <save-candidate-equivs-as>] 
                         [:remove-candidate-equivs <remove-candidate-equivs>]) 
    

    This is an often useful alternative to make-fraig-config.

    We construct a new fraig-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 fty::defprod.

    Macro: change-fraig-config

    (defmacro change-fraig-config (x &rest args)
     (std::change-aggregate
          'fraig-config
          x args
          '((:initial-sim-words . fraig-config->initial-sim-words)
            (:initial-sim-rounds . fraig-config->initial-sim-rounds)
            (:sim-words . fraig-config->sim-words)
            (:ipasir-limit . fraig-config->ipasir-limit)
            (:ipasir-recycle-count . fraig-config->ipasir-recycle-count)
            (:ctrex-queue-limit . fraig-config->ctrex-queue-limit)
            (:ctrex-force-resim . fraig-config->ctrex-force-resim)
            (:final-force-resim . fraig-config->final-force-resim)
            (:random-seed-name . fraig-config->random-seed-name)
            (:outs-only . fraig-config->outs-only)
            (:miters-only . fraig-config->miters-only)
            (:delete-class-on-fail . fraig-config->delete-class-on-fail)
            (:gatesimp . fraig-config->gatesimp)
            (:level-limit . fraig-config->level-limit)
            (:output-types . fraig-config->output-types)
            (:save-candidate-equivs-as
                 .
                 fraig-config->save-candidate-equivs-as)
            (:remove-candidate-equivs
                 .
                 fraig-config->remove-candidate-equivs))
          'change-fraig-config
          'nil))