• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
      • Aignet-copy-init
      • Aignet-simplify-with-tracking
      • Aignet-simplify-marked-with-tracking
      • Aignet-cnf
        • Aignet-lit->cnf
        • Aignet-ipasir
          • Aignet-vals-sat-care-masks-rec
          • Aignet-vals-sat-care-masks-lits
          • Aignet-lits-ipasir-sat-minimize
          • Aignet-lit-ipasir-sat-minimize
          • Aignet-lits-ipasir-sat-check
          • Aignet-get-ipasir-ctrex-regvals
          • Aignet-get-ipasir-ctrex-invals
          • Aignet-lit->ipasir
      • Aignet-simplify-marked
      • Aignet-complete-copy
      • Aignet-transforms
      • Aignet-eval
      • Semantics
      • Aignet-read-aiger
      • Aignet-write-aiger
      • Aignet-abc-interface
      • Utilities
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Aignet-ipasir

Aignet-get-ipasir-ctrex-invals

Records the input values for a satisfying assignment from an ipasir SAT check.

Signature

(aignet-get-ipasir-ctrex-invals n invals sat-lits aignet ipasir) 
  → 
new-invals

Arguments

n — Iterator -- should start at 0.
    Guard (natp n).

invals — Bit array stobj which will be overwritten with the input values.

sat-lits — Records assignment of SAT variables to aignet nodes.

aignet — AIG network.

ipasir — Incremental solver -- must be in :sat state.

Returns

new-invals — Updated bit array stobj containing the input values.

Definitions and Theorems

Function: aignet-get-ipasir-ctrex-invals

(defun aignet-get-ipasir-ctrex-invals
       (n invals sat-lits aignet ipasir)
 (declare (xargs :stobjs (invals sat-lits aignet ipasir)))
 (declare (xargs :guard (natp n)))
 (declare
      (xargs :guard (and (sat-lits-wfp sat-lits aignet)
                         (<= n (num-ins aignet))
                         (<= (num-ins aignet)
                             (bits-length invals))
                         (non-exec (equal (ipasir$a->status ipasir)
                                          :sat)))))
 (let ((__function__ 'aignet-get-ipasir-ctrex-invals))
  (declare (ignorable __function__))
  (b*
   (((when (mbe :logic (zp (- (num-ins aignet) (nfix n)))
                :exec (eql (num-ins aignet) n)))
     invals)
    (id (innum->id n aignet))
    (sat-lit (aignet-id->sat-lit id sat-lits))
    ((when (eql 0 sat-lit))
     (aignet-get-ipasir-ctrex-invals (1+ (lnfix n))
                                     invals sat-lits aignet ipasir))
    (val (ipasir-val ipasir sat-lit))
    ((unless val)
     (aignet-get-ipasir-ctrex-invals (1+ (lnfix n))
                                     invals sat-lits aignet ipasir))
    (invals (set-bit n val invals)))
   (aignet-get-ipasir-ctrex-invals (1+ (lnfix n))
                                   invals sat-lits aignet ipasir))))

Theorem: invals-length-of-aignet-get-ipasir-ctrex-invals

(defthm invals-length-of-aignet-get-ipasir-ctrex-invals
  (b* ((?new-invals (aignet-get-ipasir-ctrex-invals
                         n invals sat-lits aignet ipasir)))
    (implies (<= (num-ins aignet) (len invals))
             (equal (len new-invals) (len invals)))))

Theorem: aignet-get-ipasir-ctrex-invals-of-nfix-n

(defthm aignet-get-ipasir-ctrex-invals-of-nfix-n
 (equal
  (aignet-get-ipasir-ctrex-invals (nfix n)
                                  invals sat-lits aignet ipasir)
  (aignet-get-ipasir-ctrex-invals n invals sat-lits aignet ipasir)))

Theorem: aignet-get-ipasir-ctrex-invals-nat-equiv-congruence-on-n

(defthm aignet-get-ipasir-ctrex-invals-nat-equiv-congruence-on-n
 (implies
  (nat-equiv n n-equiv)
  (equal
    (aignet-get-ipasir-ctrex-invals n invals sat-lits aignet ipasir)
    (aignet-get-ipasir-ctrex-invals
         n-equiv invals sat-lits aignet ipasir)))
 :rule-classes :congruence)

Theorem: aignet-get-ipasir-ctrex-invals-of-node-list-fix-aignet

(defthm aignet-get-ipasir-ctrex-invals-of-node-list-fix-aignet
 (equal
  (aignet-get-ipasir-ctrex-invals
       n invals sat-lits (node-list-fix aignet)
       ipasir)
  (aignet-get-ipasir-ctrex-invals n invals sat-lits aignet ipasir)))

Theorem: aignet-get-ipasir-ctrex-invals-node-list-equiv-congruence-on-aignet

(defthm
 aignet-get-ipasir-ctrex-invals-node-list-equiv-congruence-on-aignet
 (implies
  (node-list-equiv aignet aignet-equiv)
  (equal
    (aignet-get-ipasir-ctrex-invals n invals sat-lits aignet ipasir)
    (aignet-get-ipasir-ctrex-invals
         n invals sat-lits aignet-equiv ipasir)))
 :rule-classes :congruence)