• Top
  • Documentation
    • Xdoc
      • Undocumented
        • Interp-flags
        • Simpcode
        • Npn4
          • !npn4->truth-idx
          • !npn4->polarity
          • !npn4->negate
          • !npn4->perm
          • Npn4-fix
          • Npn4->polarity
          • Npn4->truth-idx
          • Npn4->negate
          • Npn4-p
          • Npn4->perm
        • 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
        • 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

• Npn4

!npn4->truth-idx

Update the |TRUTH|::|TRUTH-IDX| field of a npn4 bit structure.

Signature

(!npn4->truth-idx truth-idx x) → new-x

Arguments

truth-idx — Guard (truth-idx-p truth-idx).

x — Guard (npn4-p x).

Returns

new-x — Type (npn4-p new-x).

Definitions and Theorems

Function: !npn4->truth-idx

(defun !npn4->truth-idx (truth-idx x)
 (declare (xargs :guard (and (truth-idx-p truth-idx)
                             (npn4-p x))))
 (mbe
     :logic
     (b* ((truth-idx (mbe :logic (truth-idx-fix truth-idx)
                          :exec truth-idx))
          (x (npn4-fix x)))
       (part-install truth-idx x
                     :width 16
                     :low 0))
     :exec (the (unsigned-byte 27)
                (logior (the (unsigned-byte 27)
                             (logand (the (unsigned-byte 27) x)
                                     (the (signed-byte 17) -65536)))
                        (the (unsigned-byte 16) truth-idx)))))

Theorem: npn4-p-of-!npn4->truth-idx

(defthm npn4-p-of-!npn4->truth-idx
  (b* ((new-x (!npn4->truth-idx truth-idx x)))
    (npn4-p new-x))
  :rule-classes :rewrite)

Theorem: !npn4->truth-idx-of-truth-idx-fix-truth-idx

(defthm !npn4->truth-idx-of-truth-idx-fix-truth-idx
  (equal (!npn4->truth-idx (truth-idx-fix truth-idx)
                           x)
         (!npn4->truth-idx truth-idx x)))

Theorem: !npn4->truth-idx-truth-idx-equiv-congruence-on-truth-idx

(defthm !npn4->truth-idx-truth-idx-equiv-congruence-on-truth-idx
  (implies (truth-idx-equiv truth-idx truth-idx-equiv)
           (equal (!npn4->truth-idx truth-idx x)
                  (!npn4->truth-idx truth-idx-equiv x)))
  :rule-classes :congruence)

Theorem: !npn4->truth-idx-of-npn4-fix-x

(defthm !npn4->truth-idx-of-npn4-fix-x
  (equal (!npn4->truth-idx truth-idx (npn4-fix x))
         (!npn4->truth-idx truth-idx x)))

Theorem: !npn4->truth-idx-npn4-equiv-congruence-on-x

(defthm !npn4->truth-idx-npn4-equiv-congruence-on-x
  (implies (npn4-equiv x x-equiv)
           (equal (!npn4->truth-idx truth-idx x)
                  (!npn4->truth-idx truth-idx x-equiv)))
  :rule-classes :congruence)

Theorem: !npn4->truth-idx-is-npn4

(defthm !npn4->truth-idx-is-npn4
  (equal (!npn4->truth-idx truth-idx x)
         (change-npn4 x :truth-idx truth-idx)))

Theorem: npn4->truth-idx-of-!npn4->truth-idx

(defthm npn4->truth-idx-of-!npn4->truth-idx
  (b* ((?new-x (!npn4->truth-idx truth-idx x)))
    (equal (npn4->truth-idx new-x)
           (truth-idx-fix truth-idx))))

Theorem: !npn4->truth-idx-equiv-under-mask

(defthm !npn4->truth-idx-equiv-under-mask
  (b* ((?new-x (!npn4->truth-idx truth-idx x)))
    (npn4-equiv-under-mask new-x x -65536)))