		Search-engine friendly clone of the ACL2 documentation.

Def-svtv-data-export

Svtv-data-obj

A non-stobj representation of a svtv-data stobj, as produced by def-svtv-data-export.

This is a product type introduced by defprod.

Fields

design — design
user-names — svtv-namemap
namemap — svtv-name-lhs-map
namemap-validp — booleanp
flatten — flatten-res
flatten-validp — booleanp
flatnorm-setup — flatnorm-setup
flatnorm — flatnorm-res
flatnorm-validp — booleanp
phase-fsm-setup — phase-fsm-config
phase-fsm — fsm
phase-fsm-validp — booleanp
cycle-phases — svtv-cyclephaselist
cycle-fsm — fsm
cycle-fsm-validp — booleanp
pipeline-setup — pipeline-setup
pipeline — svex-alist
pipeline-validp — booleanp

All fields are just as in the svtv-data stobj, except that the moddb and aliases fields are missing since they are stobjs themselves and can be fairly quickly regenerated.

Subtopics

Make-svtv-data-obj: Basic constructor macro for svtv-data-obj structures.
Svtv-data-obj-fix: Fixing function for svtv-data-obj structures.
Svtv-data-obj-p: Recognizer for svtv-data-obj structures.
Svtv-data-obj-equiv: Basic equivalence relation for svtv-data-obj structures.
Change-svtv-data-obj: Modifying constructor for svtv-data-obj structures.
Svtv-data-obj->pipeline-validp: Get the pipeline-validp field from a svtv-data-obj.
Svtv-data-obj->pipeline-setup: Get the pipeline-setup field from a svtv-data-obj.
Svtv-data-obj->phase-fsm-validp: Get the phase-fsm-validp field from a svtv-data-obj.
Svtv-data-obj->phase-fsm-setup: Get the phase-fsm-setup field from a svtv-data-obj.
Svtv-data-obj->namemap-validp: Get the namemap-validp field from a svtv-data-obj.
Svtv-data-obj->flatten-validp: Get the flatten-validp field from a svtv-data-obj.
Svtv-data-obj->flatnorm-validp: Get the flatnorm-validp field from a svtv-data-obj.
Svtv-data-obj->flatnorm-setup: Get the flatnorm-setup field from a svtv-data-obj.
Svtv-data-obj->cycle-phases: Get the cycle-phases field from a svtv-data-obj.
Svtv-data-obj->cycle-fsm-validp: Get the cycle-fsm-validp field from a svtv-data-obj.
Svtv-data-obj->user-names: Get the user-names field from a svtv-data-obj.
Svtv-data-obj->namemap: Get the namemap field from a svtv-data-obj.
Svtv-data-obj->pipeline: Get the pipeline field from a svtv-data-obj.
Svtv-data-obj->phase-fsm: Get the phase-fsm field from a svtv-data-obj.
Svtv-data-obj->flatten: Get the flatten field from a svtv-data-obj.
Svtv-data-obj->flatnorm: Get the flatnorm field from a svtv-data-obj.
Svtv-data-obj->design: Get the design field from a svtv-data-obj.
Svtv-data-obj->cycle-fsm: Get the cycle-fsm field from a svtv-data-obj.