• 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-regvals

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

Signature

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

Arguments

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

regvals — Bit array stobj which will be overwritten with the register values.

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

aignet — AIG network.

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

Returns

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

Definitions and Theorems

Function: aignet-get-ipasir-ctrex-regvals

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

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

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

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

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

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

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

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

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

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

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