• 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
            • Wcp-witness-rule
            • Make-wcp-witness-rule
            • Change-wcp-witness-rule
            • Honsed-wcp-witness-rule
            • Make-honsed-wcp-witness-rule
            • Wcp-witness-rule->theorem
            • Wcp-witness-rule->term
            • Wcp-witness-rule->restriction
            • Wcp-witness-rule->name
            • Wcp-witness-rule->generalize
            • Wcp-witness-rule->expr
            • Wcp-witness-rule->enabledp
          • 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
          • 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
          • 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
          • Fty::flexprod-listp
          • Fty::flexprod-field-listp
          • 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
          • 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
          • 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
  • Undocumented

Wcp-witness-rule-p

(wcp-witness-rule-p x) is a std::defaggregate of the following fields.

  • name — Invariant (symbolp name).
  • enabledp
  • term — Invariant (pseudo-termp term).
  • expr — Invariant (pseudo-termp expr).
  • restriction
  • theorem — Invariant (symbolp theorem).
  • generalize — Invariant (and (alistp generalize) (pseudo-term-listp (strip-cars generalize)) (symbol-listp (strip-cdrs generalize))) .

Source link: wcp-witness-rule-p

Subtopics

Wcp-witness-rule
Raw constructor for wcp-witness-rule-p structures.
Make-wcp-witness-rule
Constructor macro for wcp-witness-rule-p structures.
Change-wcp-witness-rule
A copying macro that lets you create new wcp-witness-rule-p structures, based on existing structures.
Honsed-wcp-witness-rule
Raw constructor for honsed wcp-witness-rule-p structures.
Make-honsed-wcp-witness-rule
Constructor macro for honsed wcp-witness-rule-p structures.
Wcp-witness-rule->theorem
Access the theorem field of a wcp-witness-rule-p structure.
Wcp-witness-rule->term
Access the term field of a wcp-witness-rule-p structure.
Wcp-witness-rule->restriction
Access the restriction field of a wcp-witness-rule-p structure.
Wcp-witness-rule->name
Access the name field of a wcp-witness-rule-p structure.
Wcp-witness-rule->generalize
Access the generalize field of a wcp-witness-rule-p structure.
Wcp-witness-rule->expr
Access the expr field of a wcp-witness-rule-p structure.
Wcp-witness-rule->enabledp
Access the enabledp field of a wcp-witness-rule-p structure.