Undocumented
Placeholder for documentation topics that lack good :parents.
Many ACL2::macros such as std::deflist and other
ACL2::std/util macros can automatically generate xdoc
documentation topics.
When someone uses these macros but doesn't give any :parents for the
resulting documentation, we put the resulting documentation here. This seems
better than just dropping the documentation completely, since at least you can
at least see the boilerplate documentation and any embedded documentation that
the programmer did provide.
As ongoing documentation improvement work, most topics here can benefit from
being given more appropriate :parents.
Subtopics
- Interp-flags
- An 6-bit unsigned bitstruct type.
- Simpcode
- An 4-bit unsigned bitstruct type.
- Npn4
- An 27-bit unsigned bitstruct type.
- Cutinfo
- An 32-bit unsigned bitstruct type.
- Glcp-config-p
- Glmc-config-p
- Defsvtv-args
- Vl-renaming-alist-p
- (vl-renaming-alist-p x) recognizes association lists where every key satisfies stringp and each value satisfies stringp.
- Vcd-pathmap-p
- (vcd-pathmap-p x len) recognizes association lists where every key satisfies anyp and each value satisfies vcd-indexlist-p.
- Vcd-idxhash-p
- (vcd-idxhash-p x len) recognizes association lists where every key satisfies vcd-index-p and each value satisfies not.
- *atc-exec-binary-strict-pure-rules*
- Ecut-wirename-alistp
- (ecut-wirename-alistp x) recognizes association lists where every key satisfies symbolp and each value satisfies ecutnames-p.
- Context
- Fixtype of contexts.
- Incremental-extremize-config-p
- Block-headerp
- Ctrex-rule
- Execution-environmentp
- Glmc-fsm-p
- Transactionp
- Eqbylbp-config-p
- Proof-obligation
- Fixtype of proof obligations.
- Cgraph-edge
- Wcp-instance-rule-p
- Fgl-casesplit-config
- Wcp-witness-rule-p
- Obligation-hyp
- Fixtype of hypotheses for proof obligations.
- Vl-parsestate
- Ecutnames-p
- Te-args
- Fgl-satlink-monolithic-sat-config
- Fn-info-elt-p
- Wcp-template-p
- Truth-idx
- An 16-bit unsigned bitstruct type.
- Polarity4
- An 4-bit unsigned bitstruct type.
- Phase-fsm-params
- Propiso-info-p
- Cutscore
- An 12-bit unsigned bitstruct type.
- Vl-rhs
- A right-hand side for a variable initialization or procedural assignment.
- Truth6
- An 64-bit unsigned bitstruct type.
- Constraint-tuple
- Truth5
- An 32-bit unsigned bitstruct type.
- Truth4
- An 16-bit unsigned bitstruct type.
- Truth3
- An 8-bit unsigned bitstruct type.
- Svexl-node
- Ringosc3
- Prof-entry-p
- Constraint-tuple-p
- Fgl-rune
- Stv-spec-p
- Run-snippet-file-info
- Svex-scc-consts
- Fsm
- Machine-statep
- Run-snippet-info
- Svtv-precompose-data
- Pipeline-setup
- Maybe-svar-p
- Option type; svar or nil.
- Svl-module
- Maybe-fgl-generic-rule
- Option type; fgl-generic-rule or nil.
- Frames
- Abstract stobj that implements a two dimensional array
of bitps.
- Maybe-snippet-mismatch
- Option type; snippet-mismatch or nil.
- Cpuid-info-p
- Vl-warningtree
- Maybe-proof-obligation
- Fixtype of optional proof obligations.
- Svtv-override-check
- Maybe-svtv-chase-evaldata
- Option type; svtv-chase-evaldata or nil.
- Fty-info
- Prof-entry
- Substatep
- Vl-maybe-rhs
- Option type; vl-rhs or nil.
- Vl-parsed-ports
- Top-level, temporary representation for parsed ports.
- Svex-context
- An object that describes a reference to a particular svex subexpression.
- Account-statep
- Maybe-simpcode
- Option type; simpcode or nil.
- Maybe-rational
- Option type; rational or nil.
- Maybe-svex
- Option type; svex or nil.
- 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
- Top-level, temporary representation for the parsed port list.
- 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
- 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
- (fe-list-listp pfield::x p) recognizes lists where every element satisfies fe-listp.
- Fgl-ev-congruence-rulelist-correct-p
- (fgl-ev-congruence-rulelist-correct-p x) recognizes lists where every element satisfies fgl-ev-congruence-rule-correct-p.
- N-outputs-dom-supergates-sweep-config
- Svex-envlists-equivalent
- Svex-alistlist-eval-equiv
- Flatnorm-setup
- G-map-tag
- Obs-sdom-array
- Abstract stobj: logically this just represents a list of
|AIGNET|::|OBS-SDOM-INFO-P|s, but it is
implemented as an array.
- Dom-supergates-sweep-config
- Truth4arr
- Abstract stobj: logically this just represents a list of
|TRUTH|::|TRUTH4-P|s, but it is
implemented as an array.
- Npn4arr
- Abstract stobj: logically this just represents a list of
|TRUTH|::|MAYBE-NPN4-P|s, but it is
implemented as an array.
- Syndef::acid4
- Svex-envlists-similar
- Svex-alist-compose-equiv
- Sym-prod
- Fgl-congruence-rune
- Svex-envs-1mask-equiv
- U32arr
- Abstract stobj: logically this just represents a list of
|ACL2|::|NATP|s, but it is
implemented as an array.
- Litarr
- Abstract stobj: logically this just represents a list of
|SATLINK|::|LITP|s, but it is
implemented as an array.
- Aigtrans
- Abstract stobj: logically this just represents
an untyped list, but it is implemented as an
array.
- Svexlist-eval-equiv
- N-outputs-unreachability-config
- Svex-eval-equiv
- Unreachability-config
- Keys-equiv
- Vl-maybe-exprtype-list-p
- (vl-maybe-exprtype-list-p x) recognizes lists where every element satisfies vl-maybe-exprtype-p.
- Svex-alistlist
- A list of svex-alist-p objects.
- Svar-overridetype-p
- Fty::flexprod-listp
- (fty::flexprod-listp acl2::x) recognizes lists where every element satisfies fty::flexprod-p.
- Fty::flexprod-field-listp
- (fty::flexprod-field-listp acl2::x) recognizes lists where every element satisfies fty::flexprod-field-p.
- Vcd-indexlist-p
- (vcd-indexlist-p x len) recognizes lists where every element satisfies vcd-index-p.
- Alternative-spec-listp
- (alternative-spec-listp x) recognizes lists where every element satisfies alternative-specp.
- Variable-listp
- (variable-listp x) recognizes lists where every element satisfies variablep.
- Vcd-vectorlist-p
- (vcd-vectorlist-p x) recognizes lists where every element satisfies vcd-vector-p.
- Vcd-multivectorlist-p
- (vcd-multivectorlist-p x) recognizes lists where every element satisfies vcd-multivector-p.
- Field-spec-listp
- (field-spec-listp x) recognizes lists where every element satisfies field-specp.
- Neteval-ordering
- An alist mapping svar-p to neteval-sigordering-p.
- Prof-entrylist-p
- (prof-entrylist-p x) recognizes lists where every element satisfies prof-entry-p.
- Hyp-tuplelist-p
- (hyp-tuplelist-p x) recognizes lists where every element satisfies hyp-tuple-p.
- Glcp-obj-ctrexlist-p
- (glcp-obj-ctrexlist-p x) recognizes lists where every element satisfies glcp-obj-ctrex-p.
- Symbol-path-list-p
- (symbol-path-list-p x) recognizes lists where every element satisfies symbol-path-p.
- Pseudo-input-listp
- (pseudo-input-listp x) recognizes lists where every element satisfies pseudo-input-list-eltp.
- Input-listp
- (input-listp x str) recognizes lists where every element satisfies input-list-eltp.
- Ecutname-list-p
- (ecutname-list-p x) recognizes lists where every element satisfies ecutnames-p.
- Boundrw-substlist-p
- (boundrw-substlist-p x) recognizes lists where every element satisfies boundrw-subst-p.
- Constraintlist
- A list of constraint-p objects.
- Fgl-object-bindings
- An alist mapping pseudo-var-p to fgl-object-p.
- Fgl-generic-rule
- 4v-equiv
- Equivalence of four-valued constants, i.e., 4vps.
- Sdm-instruction-table
- An alist mapping nat-listp to sdm-instruction-table-entry-p.
- Svexl-node-array
- An alist mapping natp to svexl-node-p.
- Sig-path
- A list of sig-p objects.
- Func-alist
- An alist mapping symbolp to func-p.
- Fgl-generic-rune
- Fgl-ev-iff-equiv
- Pseudo-term-subst
- An alist mapping pseudo-var-p to pseudo-termp.
- Nth-lit-equiv
- Frames-equiv
- Eval-formula-equiv
- Svex-s4env
- An alist mapping svars to 4vecs. Often used as an
environment that gives variables their values in svex-eval.
- Svex-env-keys-equiv
- Svex-alist-keys-equiv
- Pseudo-term-alist
- An alist mapping pseudo-termp to pseudo-termp.
- Fgl-ev-equiv
- Lits-equiv
- Nth-nat-equiv
- Faig-const-equiv
- Equivalence of faig constants (faig-const-p).
- Bdd-equiv
- Byte-list
- A list of n08p objects.
- Vl-user-paramsettings
- A list of vl-user-paramsetting-p objects.
- Classname/params-unparam-map
- An alist mapping classname/params-p to stringp.
- Obligation-hyp-list
- Fixtype of lists of hypotheses for proof obligations.
- Svtv*-output-alist
- An alist mapping stringp to svtv-variable-p.
- Svtv*-input-alist
- An alist mapping stringp to svtv*-input-p.
- Svtv-probealist
- An alist mapping svar-p to svtv-probe-p.
- Svtv-override-triplemap
- An alist mapping svar-p to svtv-override-triple-p.
- Svtv-cyclephaselist
- A list of svtv-cyclephase-p objects.
- Svex/index-maybenat-alist
- An alist mapping svex/index-p to maybe-natp.
- Svex-context-alist
- An alist mapping svex-p to svex-contextlist-p.
- Segment-driver-map
- An alist mapping svar-p to segment-driverlist-p.
- Rangemap
- An alist mapping address-p to rangelist-p.
- Fnsym-svexlistlist-alist
- An alist mapping fnsym-p to svexlistlist-p.
- Tmp-occ-alist
- An alist mapping occ-name-p to tmp-occ-p.
- Svl-module-alist
- An alist mapping sv::modname-p to svl-module-p.
- Svexl-node-alist
- An alist mapping sv::svar-p to svexl-node-p.
- Occ-name-alist
- An alist mapping occ-name-p to occ-name-list-p.
- Integerp-of-svex-extn-list
- A list of integerp-of-svex-extn-p objects.
- Alias-alist
- An alist mapping sv::svar-p to svex-p.
- Special-char-alist
- An alist mapping characterp to character-listp.
- Fty-info-alist
- An alist mapping symbolp to fty-info-p.
- Bfr-updates
- An alist mapping bfr-varname-p to anything.
- Term-equivs
- An alist mapping fgl-object-p to nat-listp.
- Term-bvars
- An alist mapping fgl-object-p to natp.
- Sig-table
- An alist mapping fgl-objectlist-p to fgl-object-bindingslist-p.
- Fgl-function-mode-alist
- An alist mapping symbolp to fgl-function-mode-p.
- Ctrex-ruletable
- An alist mapping pseudo-fnsym-p to ctrex-rulelist-p.
- Constraint-db
- An alist mapping pseudo-fnsym-p to constraint-tuplelist-p.
- Congruence-rule-table
- An alist mapping pseudo-fnsym-p to congruence-rulelist-p.
- Cgraph-derivstates
- An alist mapping fgl-object-p to cgraph-derivstate-p.
- Cgraph-alist
- An alist mapping fgl-object-p to anything.
- Cgraph
- An alist mapping fgl-object-p to cgraph-edgelist-p.
- Casesplit-alist
- An alist mapping anything to pseudo-termp.
- Truthmap
- An alist mapping truth::truth4-p to lit-listp.
- Named-lit-list-map
- An alist mapping symbolp to lit-listp.
- Axi-map
- An alist mapping axi-term-p to axi-lit-p.
- Nth-equiv
- Faig-fix-equiv
- Syntactic equivalence of faigs under faig-fix.
- Vl-string/int-alist
- An alist mapping stringp to integerp.
- Vl-reservedtable
- An alist mapping stringp to stringp.
- Vl-echarlist
- A list of vl-echar-p objects.
- Vl-ctxexprlist
- A list of vl-ctxexpr-p objects.
- Vl-coredatatype-infolist
- A list of vl-coredatatype-info-p objects.
- Vl-usertypes
- An alist mapping stringp to anything.
- Vl-coredatatype-infolist
- A list of vl-coredatatype-info-p objects.
- Proof-obligation-list
- Fixtype of lists of proof obligations.
- Use-set-summaries
- An alist mapping modname-p to use-set-p.
- Svtv-rev-probealist
- An alist mapping svtv-probe-p to svar-p.
- Svex/index-nat-alist
- An alist mapping svex/index-p to natp.
- Svex/index-key-alist
- An alist mapping svex/index-p to anything.
- Svex-key-alist
- An alist mapping svex-p to anything.
- Svex-envlist
- A list of svex-env-p objects.
- Svar-widths
- An alist mapping svar-p to integerp.
- Svar-width-map
- An alist mapping svar-p to posp.
- Svar-splittab
- An alist mapping svar-p to svar-split-p.
- Svar-proplist
- An alist mapping symbolp to anything.
- Svar-key-alist
- An alist mapping svar-p to anything.
- Rsh-of-concat-alist
- An alist mapping natp to svex-p.
- Path-alist
- An alist mapping path-p to anything.
- Name-alist
- An alist mapping name-p to anything.
- Address-alist
- An alist mapping address-p to anything.
- Width-of-svex-extn-list
- A list of width-of-svex-extn-p objects.
- Svl-occ-alist
- An alist mapping anything to svl-occ-p.
- Svex-to-natp-alist
- An alist mapping svex-p to natp.
- Symbol-string-alist
- An alist mapping symbolp to stringp.
- Symbol-integer-alist
- An alist mapping symbolp to integerp.
- Sym-nat-alist
- An alist mapping symbolp to natp.
- String-string-alist
- An alist mapping stringp to stringp.
- Fty-types
- An alist mapping symbolp to fty-type-p.
- Fty-field-alist
- An alist mapping symbolp to symbolp.
- Any-table
- An alist mapping sig-path-p to booleanp.
- Obj-alist
- An alist mapping anything to anything.
- Nat-nat-alist
- An alist mapping natp to natp.
- Constraint-instancelist
- A list of constraint-instance-p objects.
- Congruence-rulelist
- A list of cmr::congruence-rule-p objects.
- Calist
- An alist mapping anything to bitp.
- Bvar-db-consistency-errorlist
- A list of bvar-db-consistency-error-p objects.
- Var-counts-alist
- An alist mapping pseudo-var-p to natp.
- Pseudo-var-list
- A list of pseudo-var-p objects.
- Equiv-contextslist
- A list of equiv-contextsp objects.
- Nat-val-alistp
- An alist mapping anything to natp.
- Id-neg-alist
- An alist mapping natp to bitp.
- String-keyed-alist-p
- Recognizer for alists whose keys are strings. Used to implement and
extend regex-get.
- Snippet-table
- A list of snippet-info-p objects.
- Snippet-mismatch-list
- A list of snippet-mismatch-p objects.
- Vl-reportcardkeylist
- A list of vl-reportcardkey-p objects.
- Partsumlist
- A list of partsum-elt-p objects.
- Partsum-elt
- A list of partsum-comp-p objects.
- Classname/paramslist
- A list of classname/params-p objects.
- Vl-reportcardkeylist
- A list of vl-reportcardkey-p objects.
- Vl-locationlist
- A list of vl-location-p objects.
- Vl-echarlist
- A list of vl-echar-p objects.
- Perm4-list
- A list of perm4p objects.
- Svtv*-phaselist
- A list of svtv*-phase-p objects.
- Svtv-override-triplemaplist
- A list of svtv-override-triplemap-p objects.
- Svtv-override-triplelist
- A list of svtv-override-triple-p objects.
- Svtv-override-checklist
- A list of svtv-override-check-p objects.
- Svtv-name-lhs-map-list
- A list of svtv-name-lhs-map-p objects.
- Svex/indexlist
- A list of svex/index-p objects.
- Svexlistlist
- A list of svexlist-p objects.
- Svex-override-triplelist
- A list of svex-override-triple-p objects.
- Svex-contextlist
- A list of svex-context-p objects.
- Svarlist-list
- A list of svarlist-p objects.
- Svar-widthslist
- A list of svar-widths-p objects.
- Svar-overridetypelist
- A list of svar-overridetype-p objects.
- Svar-override-triplelist
- A list of svar-override-triple-p objects.
- Segment-driverlist
- A list of segment-driver-p objects.
- Rangelist
- A list of range-p objects.
- Chase-stack
- A list of chase-position-p objects.
- Addresslist
- A list of address-p objects.
- 4veclistlist
- A list of 4veclist-p objects.
- 3col4vecs
- A list of 3col4vecline-p objects.
- Occ-name-list
- A list of occ-name-p objects.
- Alias-lst
- A list of alias-p objects.
- Word-list
- A list of wordp objects.
- Sig-path-list
- A list of sig-path-p objects.
- Function-option-name-lst
- A list of function-option-name-p objects.
- Any-trace
- A list of any-table-p objects.
- Bfr-varnamelist
- A list of bfr-varname-p objects.
- Aig-varlist
- A list of ACL2::aig-var-p objects.
- Scratch-nontagidxlist
- A list of scratch-nontagidx-p objects.
- Prof-entrylist
- A list of prof-entry-p objects.
- Interp-st-field-p
- Fgl-runelist
- A list of fgl-rune-p objects.
- Fgl-rulelist
- A list of fgl-rule-p objects.
- Fgl-object-bindingslist
- A list of fgl-object-bindings-p objects.
- Fgl-congruence-runelist
- A list of fgl-congruence-rune-p objects.
- Fgl-binder-runelist
- A list of fgl-binder-rune-p objects.
- Fgl-binder-rulelist
- A list of fgl-binder-rule-p objects.
- Ctrex-rulelist
- A list of ctrex-rule-p objects.
- Constraint-tuplelist
- A list of constraint-tuple-p objects.
- Cgraph-edgelist
- A list of cgraph-edge-p objects.
- Candidate-assigns
- A list of candidate-assign-p objects.
- Rw-pairlist
- A list of rw-pair-p objects.
- Rewritelist
- A list of rewrite-p objects.
- Equiv-contexts
- A list of pseudo-fnsym-p objects.
- Bindinglist
- A list of binding-p objects.
- Pos-list
- A list of natp objects.
- Obs-sdom-info-list
- A list of obs-sdom-info-p objects.
- Cutinfolist
- A list of cutinfo-p objects.
- Bit-list
- A list of bitp objects.
- Axi-termlist
- A list of axi-term-p objects.
- Axi-litlist
- A list of axi-lit-p objects.
- Symbol-pseudoterm-alist
- Fixtype of alists from symbols to pseudo-terms.
- Symbol-pseudoeventform-alist
- Fixtype of alists from symbols to pseudo event forms.
- Inst-list
- A list of inst-p objects.
- Vl-user-paramsettings-mode-p
- Svtv-data$c-field-p
- Ctrex-ruletype-p
- String-stringlist-alist
- Fixtype of alists from strings to lists of strings.
- 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
- Env$-field-p
- Axi
- *smt-architecture*
- *vl-directions-kwds*
- *vl-directions-kwd-alist*
- Rlp-trees
