Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Gl
Esim
Vl2014
Sv
Svex-stvs
Svtv-data
Defsvtv$
Svtv-run
Defsvtv-phasewise
Svtv
Svtv-chase
Svtv-p
Svtv-to-fsm
Svtv-to-fsm-defs
Svtv-spec-fsm-bindings-for-alist
Svtv-spec-fsm-bindings-for-alists
Svtv-spec-fsm-constraints-for-alist
Svtv-spec-fsm-constraints-for-alists
Lhprobe
Svtv-spec-fsm-bindings-for-lhprobe
Svtv-spec-fsm-constraints-for-lhprobe
Lhprobe-map-overridemux-eval
Svtv-fsm-namemap-alistlist
Lhprobe-constraintlist-overridemux-eval
Lhs-overridemux-eval-signx
Svtv-fsm-namemap-envlist
Lhprobe/4vec-overridemux-eval
Lhprobe-constraintlist-max-stage
Lhprobe-constraint-overridemux-eval
Svex-envlists-agree
Lhprobe-overridemux-eval
Lhs-overridemux-eval-zero
Lhatom-overridemux-eval
Svar/4vec-alist-eval
Svtv-probealist-to-lhprobe-map
Svex-envlists-ovtestsimilar
Lhprobe-map-max-stage
Lhprobe-constraint
Svar/4vec-alistlist-eval
Lhprobe-map-eval
Lhprobe-constraint-max-stage
Lhprobe/4vec-change-override
Lhprobe-constraintlist-eval
Svtv-probe-to-lhprobe
Svar/4vec-eval
Lhs-eval-signx
Lhprobe-signedness-for-alist
Lhprobe-change-override
Svtv-spec-fsm-bindings
Svtv-spec-cycle-fsm-inputsubsts
Lhprobe/4vec-p
Lhprobe-constraint-eval
Svtv-spec-fsm-constraints
Svex-envlist-keys-list
Svtv-spec-non-test-vars
Svar/4vec-p
Svtv-spec->override-val-alists*
Svtv-spec->override-test-alists*
Svtv-spec->in-alists*
Lhprobe-map
Svar/4vec-alist
Svar/4vec-alist-fix
Svar/4vec-alist-p
Svar/4vec-alist-equiv
Svar/4vec-alistlist
Lhprobe-constraintlist
Force-execute
Defnamemap
Parse-svtv-to-fsm-thm
Svex-envs-check-ovtests-ok-rec
Svtv-to-fsm-final-thm-var-bindings
Svex-envlists-ovtests-ok
Svtv-override-triplemaplist-relevant-vars
Svtv-override-triplemap-relevant-vars
Svex-envlists-check-ovtests-ok
Svtv-override-triple-relevant-vars
Svtv-override-triplemaplist-test-only-p
Svex-envlists-ovtestequiv
Svtv-override-triplemap-test-only-p
Svex-envlists-ovtestsubsetp
Svtv-override-triple-test-only-p
Svex-envlists-check-ovtests-ok-rec
Svex-envs-check-ovtests-ok
Svex-alistlist-removekeys
Svtv-to-fsm-final-thm
Svtv-to-fsm-first-thm-input-var-bindings
Svtv-to-fsm-first-thm
Svtv-to-fsm-thm-fn
Make-svtv
Svtv-fix
Change-svtv
Svtv-equiv
Svtv->orig-overrides
Svtv->orig-internals
Svtv->expanded-overrides
Svtv->states
Svtv->nextstate
Svtv->expanded-ins
Svtv->outmasks
Svtv->outexprs
Svtv->orig-outs
Svtv->orig-ins
Svtv->inmasks
Svtv->nphases
Svtv->name
Svtv->labels
Svtv->inmap
Svtv->form
Svtv-spec
Defsvtv
Process.lisp
Svtv-doc
Svtv-chase$
Svtv-versus-stv
Svtv-debug-fsm
Structure.lisp
Svtv-debug
Def-pipeline-thm
Expand.lisp
Def-cycle-thm
Svtv-utilities
Svtv-debug$
Defsvtv$-phasewise
Svex-decomposition-methodology
Sv-versus-esim
Svex-decomp
Svex-compose-dfs
Svex-compilation
Moddb
Svmods
Svstmt
Sv-tutorial
Expressions
Symbolic-test-vector
Vl-to-svex
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Svtv-to-fsm-defs
Svar/4vec-alist
An alist mapping
svar-p
to
svar/4vec-p
.
This is an ordinary
defalist
.
Subtopics
Svar/4vec-alist-fix
(svar/4vec-alist-fix x)
is an
fty
alist fixing function that follows the drop-keys strategy.
Svar/4vec-alist-p
Recognizer for
svar/4vec-alist
.
Svar/4vec-alist-equiv
Basic equivalence relation for
svar/4vec-alist
structures.