• Top
    • Documentation
      • Xdoc
        • Undocumented
          • Interp-flags
          • Simpcode
          • Npn4
          • Cutinfo
          • Glcp-config-p
          • Glmc-config-p
          • Defsvtv-args
          • Vl-renaming-alist-p
          • Vcd-pathmap-p
          • Vcd-idxhash-p
          • *atc-exec-binary-strict-pure-rules*
          • Ecut-wirename-alistp
          • Context
          • Incremental-extremize-config-p
          • Block-headerp
          • Ctrex-rule
          • Execution-environmentp
          • Glmc-fsm-p
          • Transactionp
          • Eqbylbp-config-p
          • Proof-obligation
          • Cgraph-edge
          • Wcp-instance-rule-p
          • Fgl-casesplit-config
          • Wcp-witness-rule-p
          • Obligation-hyp
          • Vl-parsestate
          • Ecutnames-p
          • Te-args
          • Fgl-satlink-monolithic-sat-config
          • Fn-info-elt-p
          • Wcp-template-p
          • Truth-idx
          • Polarity4
          • Phase-fsm-params
          • Propiso-info-p
          • Cutscore
          • Vl-rhs
          • Truth6
          • Constraint-tuple
          • Truth5
          • Truth4
          • Truth3
          • Svexl-node
          • Ringosc3
          • Prof-entry-p
          • Constraint-tuple-p
          • Fgl-rune
          • Stv-spec-p
          • Run-snippet-file-info
          • Svex-scc-consts
          • Fsm
          • Machine-statep
          • Xor-signature-p
          • Run-snippet-info
          • Svtv-precompose-data
          • Pipeline-setup
          • Maybe-svar-p
          • Svl-module
          • Maybe-fgl-generic-rule
          • Frames
          • Maybe-snippet-mismatch
          • Cpuid-info-p
          • Vl-warningtree
          • Maybe-proof-obligation
          • Svtv-override-check
          • Maybe-svtv-chase-evaldata
          • Fty-info
          • Prof-entry
          • Substatep
          • Vl-maybe-rhs
          • Vl-parsed-ports
          • Svex-context
          • Account-statep
          • Maybe-simpcode
          • Maybe-rational
          • Maybe-svex
          • Flatten-res
          • Svex-reduce-config
          • Fty-type
          • Rewrite
          • Snippet-info
          • Addnames-indices
          • Svtv*-phase
          • Segment-driver
          • Satlink-parser-state
          • Fgl-binder-rune
          • Congruence-rule
          • Snippet-mismatch
          • Vl-ctxexpr
          • Rsh-of-concat-table
          • Chase-position
          • Hyp-tuple-p
          • Glcp-obj-ctrex-p
          • Glcp-bit-ctrex-p
          • Block$-p
          • Boundrw-subst-p
          • Svtv-cyclephase
          • Svar-split
          • Scopetree
          • Flatnorm-res
          • Fgl-rule
          • Constraint-rule
          • Vl-user-paramsetting
          • Svtv-override-triple
          • Svtv-evaldata
          • Svtv-composedata
          • Width-of-svex-extn
          • Array-fieldinfo-p
          • Wcp-example-app-p
          • Svtv*-input
          • Svex-override-triple
          • Svar-override-triple
          • 3col4vecline
          • Constraint-rule-p
          • Vl-parsed-ports
          • Svtv-chase-evaldata
          • Svtv-assigns-override-config
          • Svex/index
          • Svl-env
          • Svl-aliasdb
          • Inverter
          • Fgl-binder-rule
          • Bvar-db-consistency-error
          • Wcp-lit-actions-p
          • Vcd-multivector-p
          • Svtv-fsm
          • Svexl
            • Svexl-fix
            • Svexl-equiv
            • Make-svexl
            • Svexl->node-array
            • Svexl->top-node
            • Change-svexl
              • Svexl-p
            • Constraint-instance
            • Vl-parsestate
            • Partsum-comp
            • Classname/params
            • Vcd-vector-p
            • Tmp-occ
            • Svl-occ
            • Svexllist
            • Svexl-alist
            • Integerp-of-svex-extn
            • Uninterpreted
            • Rw-pair
            • Vl-echar-raw
            • Vl-echar-raw
            • Use-set
            • Svtv-probe
            • Svex-phase-varname
            • Svex-cycle-varname
            • Range
            • Phase-fsm-config
            • Overridekey-syntaxcheck-data
            • Constraint
            • Alias
            • Sig
            • Sandwich
            • Cgraph-derivstate
            • Candidate-assign
            • Svex-alist-eval-equiv!
            • Svex-alist-eval-equiv
            • Scalar-fieldinfo-p
            • Fe-list-listp
            • Fgl-ev-congruence-rulelist-correct-p
            • N-outputs-dom-supergates-sweep-config
            • Svex-envlists-equivalent
            • Svex-alistlist-eval-equiv
            • Flatnorm-setup
            • G-map-tag
            • Obs-sdom-array
            • Dom-supergates-sweep-config
            • Truth4arr
            • Npn4arr
            • Syndef::acid4
            • Svex-envlists-similar
            • Svex-alist-compose-equiv
            • Sym-prod
            • Fgl-congruence-rune
            • Svex-envs-1mask-equiv
            • U32arr
            • Litarr
            • Aigtrans
            • Svexlist-eval-equiv
            • N-outputs-unreachability-config
            • Svex-eval-equiv
            • Unreachability-config
            • Keys-equiv
            • Vl-maybe-exprtype-list-p
            • Svex-alistlist
            • Svar-overridetype-p
            • Vcd-indexlist-p
            • Alternative-spec-listp
            • Variable-listp
            • Vcd-vectorlist-p
            • Vcd-multivectorlist-p
            • Field-spec-listp
            • Neteval-ordering
            • Prof-entrylist-p
            • Hyp-tuplelist-p
            • Glcp-obj-ctrexlist-p
            • Symbol-path-list-p
            • Pseudo-input-listp
            • Input-listp
            • Ecutname-list-p
            • Boundrw-substlist-p
            • Constraintlist
            • Fgl-object-bindings
            • Fgl-generic-rule
            • 4v-equiv
            • Sdm-instruction-table
            • Svexl-node-array
            • Sig-path
            • Func-alist
            • Fgl-generic-rune
            • Fgl-ev-iff-equiv
            • Pseudo-term-subst
            • Nth-lit-equiv
            • Frames-equiv
            • Eval-formula-equiv
            • Svex-s4env
            • Svex-env-keys-equiv
            • Svex-alist-keys-equiv
            • Pseudo-term-alist
            • Fgl-ev-equiv
            • Lits-equiv
            • Nth-nat-equiv
            • Faig-const-equiv
            • Bdd-equiv
            • Byte-list
            • Vl-user-paramsettings
            • Classname/params-unparam-map
            • Obligation-hyp-list
            • Svtv*-output-alist
            • Svtv*-input-alist
            • Svtv-probealist
            • Svtv-override-triplemap
            • Svtv-cyclephaselist
            • Svex/index-maybenat-alist
            • Svex-context-alist
            • Segment-driver-map
            • Rangemap
            • Fnsym-svexlistlist-alist
            • Tmp-occ-alist
            • Svl-module-alist
            • Svexl-node-alist
            • Occ-name-alist
            • Integerp-of-svex-extn-list
            • Alias-alist
            • Special-char-alist
            • Fty-info-alist
            • Bfr-updates
            • Term-equivs
            • Term-bvars
            • Sig-table
            • Fn-indices
            • Fgl-function-mode-alist
            • Ctrex-ruletable
            • Constraint-db
            • Congruence-rule-table
            • Cgraph-derivstates
            • Cgraph-alist
            • Cgraph
            • Casesplit-alist
            • Truthmap
            • Named-lit-list-map
            • Axi-map
            • Nth-equiv
            • Faig-fix-equiv
            • Vl-string/int-alist
            • Vl-reservedtable
            • Vl-echarlist
            • Vl-ctxexprlist
            • Vl-coredatatype-infolist
            • Vl-usertypes
            • Vl-coredatatype-infolist
            • Proof-obligation-list
            • Use-set-summaries
            • Svtv-rev-probealist
            • Svex/index-nat-alist
            • Svex/index-key-alist
            • Svex-key-alist
            • Svex-envlist
            • Svar-widths
            • Svar-width-map
            • Svar-splittab
            • Svar-proplist
            • Svar-key-alist
            • Rsh-of-concat-alist
            • Path-alist
            • Name-alist
            • Address-alist
            • Width-of-svex-extn-list
            • Svl-occ-alist
            • Svex-to-natp-alist
            • Symbol-string-alist
            • Symbol-integer-alist
            • Sym-nat-alist
            • String-string-alist
            • Fty-types
            • Fty-field-alist
            • Any-table
            • Obj-alist
            • Nat-nat-alist
            • Constraint-instancelist
            • Congruence-rulelist
            • Calist
            • Bvar-db-consistency-errorlist
            • Var-counts-alist
            • Pseudo-var-list
            • Equiv-contextslist
            • Nat-val-alistp
            • Id-neg-alist
            • String-keyed-alist-p
            • Snippet-table
            • Snippet-mismatch-list
            • Vl-reportcardkeylist
            • Partsumlist
            • Partsum-elt
            • Classname/paramslist
            • Vl-reportcardkeylist
            • Vl-locationlist
            • Vl-echarlist
            • Perm4-list
            • Svtv*-phaselist
            • Svtv-override-triplemaplist
            • Svtv-override-triplelist
            • Svtv-override-checklist
            • Svtv-name-lhs-map-list
            • Svex/indexlist
            • Svexlistlist
            • Svex-override-triplelist
            • Svex-contextlist
            • Svarlist-list
            • Svar-widthslist
            • Svar-overridetypelist
            • Svar-override-triplelist
            • Segment-driverlist
            • Rangelist
            • Chase-stack
            • Addresslist
            • 4veclistlist
            • 3col4vecs
            • Occ-name-list
            • Alias-lst
            • Word-list
            • Sig-path-list
            • Function-option-name-lst
            • Any-trace
            • Bfr-varnamelist
            • Aig-varlist
            • Scratch-nontagidxlist
            • Prof-entrylist
            • Interp-st-field-p
            • Fgl-runelist
            • Fgl-rulelist
            • Fgl-object-bindingslist
            • Fgl-congruence-runelist
            • Fgl-binder-runelist
            • Fgl-binder-rulelist
            • Ctrex-rulelist
            • Constraint-tuplelist
            • Cgraph-edgelist
            • Candidate-assigns
            • Rw-pairlist
            • Rewritelist
            • Equiv-contexts
            • Bindinglist
            • Pos-list
            • Obs-sdom-info-list
            • Cutinfolist
            • Bit-list
            • Axi-termlist
            • Axi-litlist
            • Symbol-pseudoterm-alist
            • Symbol-pseudoeventform-alist
            • Inst-list
            • Vl-user-paramsettings-mode-p
            • Svtv-data$c-field-p
            • Ctrex-ruletype-p
            • String-stringlist-alist
            • Ipasir-status-p
            • Fgl-toplevel-sat-check-mode-p
            • Axi-op-p
            • Vl-opacity-p
            • St-hyp-method-p
            • Scratchobj-kind-p
            • Logicman-field-p
            • Bvar-db$c-field-p
            • Env$-field-p
            • Axi
            • *smt-architecture*
            • *vl-directions-kwds*
            • *vl-directions-kwd-alist*
            • Rlp-trees
          • Save
          • Defsection
          • Markup
          • Preprocessor
          • Terminal
          • Emacs-links
          • Defxdoc
          • Katex-integration
          • Constructors
          • Entities
          • Defxdoc+
          • Save-rendered
          • Add-resource-directory
          • Testing
          • Order-subtopics
          • Save-rendered-event
          • Archive-matching-topics
          • Archive-xdoc
          • Xdoc-extend
          • Set-default-parents
          • Missing-parents
          • Defpointer
          • Defxdoc-raw
          • Xdoc-tests
          • Xdoc-prepend
          • Defsection-progn
          • Gen-xdoc-for-file
        • ACL2-doc
        • Recursion-and-induction
        • Loop$-primer
        • Operational-semantics
        • Pointers
        • Doc
        • Documentation-copyright
        • Course-materials
        • Args
        • ACL2-doc-summary
        • Finding-documentation
        • Broken-link
        • Doc-terminal-test-2
        • Doc-terminal-test-1
      • Books
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Svexl

    Change-svexl

    Modifying constructor for svexl structures.

    Syntax
    (change-svexl x 
                  [:top-node <top-node>] 
                  [:node-array <node-array>]) 
    

    This is an often useful alternative to make-svexl.

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

    (defmacro change-svexl (x &rest args)
      (std::change-aggregate 'svexl
                             x args
                             '((:top-node . svexl->top-node)
                               (:node-array . svexl->node-array))
                             'change-svexl
                             'nil))