• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
      • Aignet-copy-init
      • 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-with-tracking
      • Aignet-complete-copy
      • Aignet-eval
      • Semantics
      • Aignet-transforms
      • Aignet-simplify-marked
      • Aignet-read-aiger
      • Aignet-write-aiger
      • Aignet-abc-interface
      • Utilities
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Aignet-ipasir

Aignet-vals-sat-care-masks-lits

Mark a subset of inputs and registers that, when assigned the same values as in the input assignment, produce the same value on the given lits.

Signature

(aignet-vals-sat-care-masks-lits 
     lits inmasks regmasks 
     invals regvals vals mark aignet state) 
 
  → 
(mv new-inmasks new-regmasks new-mark new-state)

Arguments

lits — Literals to traverse.
    Guard (lit-listp lits).

inmasks — Bit array accumulating the care set for the inputs.

regmasks — Bit array accumulating the care set for the registers.

invals — Bit array recording the satisfying assignment for the inputs.

regvals — Bit array recording the satisfying assignment for the registers.

vals — Bit array recording the values of all nodes under the satisfying assignment.

mark — Bit array marking nodes known to be in the care set.

aignet — AIG network.

state — ACL2 state, used for random number generation (coin flips).

Returns

new-inmasks — Updated care set of inputs.

new-regmasks — Updated care set of registers.

new-mark — Updated care set of all nodes.

new-state — Updated state.

Definitions and Theorems

Function: aignet-vals-sat-care-masks-lits

(defun aignet-vals-sat-care-masks-lits
       (lits inmasks regmasks
             invals regvals vals mark aignet state)
 (declare
    (xargs :stobjs (inmasks regmasks
                            invals regvals vals mark aignet state)))
 (declare (xargs :guard (lit-listp lits)))
 (declare
  (xargs
   :guard
   (and (aignet-lit-listp lits aignet)
        (non-exec
             (equal vals
                    (aignet-record-vals nil invals regvals aignet)))
        (<= (num-ins aignet)
            (bits-length inmasks))
        (<= (num-regs aignet)
            (bits-length regmasks))
        (<= (num-ins aignet)
            (bits-length invals))
        (<= (num-regs aignet)
            (bits-length regvals))
        (< (lits-max-id-val lits)
           (bits-length vals))
        (< (lits-max-id-val lits)
           (bits-length mark)))))
 (let ((__function__ 'aignet-vals-sat-care-masks-lits))
   (declare (ignorable __function__))
   (b* (((when (atom lits))
         (mv inmasks regmasks mark state))
        ((mv inmasks regmasks mark state)
         (aignet-vals-sat-care-masks-rec
              (lit->var (car lits))
              inmasks regmasks
              invals regvals vals mark aignet state)))
     (aignet-vals-sat-care-masks-lits
          (cdr lits)
          inmasks regmasks invals
          regvals vals mark aignet state))))

Theorem: aignet-vals-sat-care-masks-lits-normalize-input

(defthm aignet-vals-sat-care-masks-lits-normalize-input
  (implies (syntaxp (not (equal vals ''nil)))
           (equal (aignet-vals-sat-care-masks-lits
                       lits inmasks regmasks
                       invals regvals vals mark aignet state)
                  (aignet-vals-sat-care-masks-lits
                       lits inmasks regmasks
                       invals regvals nil mark aignet state))))

Theorem: aignet-vals-sat-care-masks-lits-preserve-marks

(defthm aignet-vals-sat-care-masks-lits-preserve-marks
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-lits
             lits inmasks regmasks
             invals regvals vals mark aignet state)))
    (implies (equal (nth n mark) 1)
             (equal (nth n new-mark) 1))))

Theorem: aignet-vals-sat-care-masks-lits-preserve-inmasks

(defthm aignet-vals-sat-care-masks-lits-preserve-inmasks
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-lits
             lits inmasks regmasks
             invals regvals vals mark aignet state)))
    (implies (equal (nth n inmasks) 1)
             (equal (nth n new-inmasks) 1))))

Theorem: aignet-vals-sat-care-masks-lits-preserve-regmasks

(defthm aignet-vals-sat-care-masks-lits-preserve-regmasks
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-lits
             lits inmasks regmasks
             invals regvals vals mark aignet state)))
    (implies (equal (nth n regmasks) 1)
             (equal (nth n new-regmasks) 1))))

Theorem: inmasks-length-of-aignet-vals-sat-care-masks-lits

(defthm inmasks-length-of-aignet-vals-sat-care-masks-lits
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-lits
             lits inmasks regmasks
             invals regvals vals mark aignet state)))
    (implies (<= (num-ins aignet) (len inmasks))
             (equal (len new-inmasks)
                    (len inmasks)))))

Theorem: regmasks-length-of-aignet-vals-sat-care-masks-lits

(defthm regmasks-length-of-aignet-vals-sat-care-masks-lits
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-lits
             lits inmasks regmasks
             invals regvals vals mark aignet state)))
    (implies (<= (num-regs aignet) (len regmasks))
             (equal (len new-regmasks)
                    (len regmasks)))))

Theorem: mark-length-of-aignet-vals-sat-care-masks-lits

(defthm mark-length-of-aignet-vals-sat-care-masks-lits
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-lits
             lits inmasks regmasks
             invals regvals vals mark aignet state)))
    (implies (< (lits-max-id-val lits) (len mark))
             (equal (len new-mark) (len mark)))))

Theorem: aignet-vals-sat-care-masks-lits-preserves-marks-above-id

(defthm aignet-vals-sat-care-masks-lits-preserves-marks-above-id
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-lits
             lits inmasks regmasks
             invals regvals vals mark aignet state)))
    (implies (< (lits-max-id-val lits) (nfix node))
             (equal (nth node new-mark)
                    (nth node mark)))))

Theorem: aignet-vals-sat-care-masks-lits-marks-id

(defthm aignet-vals-sat-care-masks-lits-marks-id
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-lits
             lits inmasks regmasks
             invals regvals vals mark aignet state)))
    (implies (member (lit-fix lit)
                     (lit-list-fix lits))
             (equal (nth (lit->var lit) new-mark)
                    1))))

Theorem: aignet-vals-sat-care-masks-lits-mark-ok-preserved

(defthm aignet-vals-sat-care-masks-lits-mark-ok-preserved
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-lits
             lits inmasks regmasks
             invals regvals vals mark aignet state)))
    (implies (aignet-vals-sat-care-masks-mark-ok
                  node mark invals regvals aignet)
             (aignet-vals-sat-care-masks-mark-ok
                  node new-mark invals regvals aignet))))

Theorem: aignet-vals-sat-care-masks-lits-mark-invar-preserved

(defthm aignet-vals-sat-care-masks-lits-mark-invar-preserved
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-lits
             lits inmasks regmasks
             invals regvals vals mark aignet state)))
    (implies (aignet-vals-sat-care-masks-mark-invar
                  id mark invals regvals aignet)
             (aignet-vals-sat-care-masks-mark-invar
                  id new-mark invals regvals aignet))))

Theorem: aignet-vals-sat-care-masks-lits-preserves-marked-inputs-masked

(defthm
     aignet-vals-sat-care-masks-lits-preserves-marked-inputs-masked
 (b* (((mv ?new-inmasks
           ?new-regmasks ?new-mark ?new-state)
       (aignet-vals-sat-care-masks-lits
            lits inmasks regmasks
            invals regvals vals mark aignet state)))
  (implies
    (aignet-marked-inputs-are-masked mark inmasks aignet)
    (aignet-marked-inputs-are-masked new-mark new-inmasks aignet))))

Theorem: aignet-vals-sat-care-masks-lits-preserves-marked-regs-masked

(defthm aignet-vals-sat-care-masks-lits-preserves-marked-regs-masked
 (b* (((mv ?new-inmasks
           ?new-regmasks ?new-mark ?new-state)
       (aignet-vals-sat-care-masks-lits
            lits inmasks regmasks
            invals regvals vals mark aignet state)))
  (implies
     (aignet-marked-regs-are-masked mark regmasks aignet)
     (aignet-marked-regs-are-masked new-mark new-regmasks aignet))))

Theorem: aignet-vals-sat-care-masks-lits-counterexample-under-masks

(defthm aignet-vals-sat-care-masks-lits-counterexample-under-masks
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-lits
             lits inmasks regmasks
             invals regvals vals mark aignet state)))
    (implies
         (and (vals-equiv-under-masks new-inmasks invals invals1)
              (vals-equiv-under-masks new-regmasks regvals regvals1)
              (aignet-vals-sat-care-masks-mark-invar
                   (lits-max-id-val lits)
                   mark invals regvals aignet)
              (aignet-marked-inputs-are-masked mark inmasks aignet)
              (aignet-marked-regs-are-masked mark regmasks aignet)
              (member-equal (lit-fix lit)
                            (lit-list-fix lits)))
         (equal (id-eval (lit->var lit)
                         invals1 regvals1 aignet)
                (id-eval (lit->var lit)
                         invals regvals aignet)))))

Theorem: aignet-vals-sat-care-masks-lits-counterexample-under-masks-lit-eval

(defthm
 aignet-vals-sat-care-masks-lits-counterexample-under-masks-lit-eval
 (b* (((mv ?new-inmasks
           ?new-regmasks ?new-mark ?new-state)
       (aignet-vals-sat-care-masks-lits
            lits inmasks regmasks
            invals regvals vals mark aignet state)))
   (implies
        (and (vals-equiv-under-masks new-inmasks invals invals1)
             (vals-equiv-under-masks new-regmasks regvals regvals1)
             (aignet-vals-sat-care-masks-mark-invar
                  (lits-max-id-val lits)
                  mark invals regvals aignet)
             (aignet-marked-inputs-are-masked mark inmasks aignet)
             (aignet-marked-regs-are-masked mark regmasks aignet)
             (member-equal (lit-fix lit)
                           (lit-list-fix lits)))
        (equal (lit-eval lit invals1 regvals1 aignet)
               (lit-eval lit invals regvals aignet)))))

Theorem: aignet-vals-sat-care-masks-lits-counterexample-under-masks-aignet-eval-conjunction

(defthm
 aignet-vals-sat-care-masks-lits-counterexample-under-masks-aignet-eval-conjunction
 (b* (((mv ?new-inmasks
           ?new-regmasks ?new-mark ?new-state)
       (aignet-vals-sat-care-masks-lits
            lits inmasks regmasks
            invals regvals vals mark aignet state)))
  (implies
    (and (vals-equiv-under-masks new-inmasks invals invals1)
         (vals-equiv-under-masks new-regmasks regvals regvals1)
         (aignet-vals-sat-care-masks-mark-invar
              (lits-max-id-val lits)
              mark invals regvals aignet)
         (aignet-marked-inputs-are-masked mark inmasks aignet)
         (aignet-marked-regs-are-masked mark regmasks aignet)
         (subsetp-equal (lit-list-fix lits1)
                        (lit-list-fix lits)))
    (equal (aignet-eval-conjunction lits1 invals1 regvals1 aignet)
           (aignet-eval-conjunction lits1 invals regvals aignet)))))

Theorem: w-state-of-aignet-vals-sat-care-masks-lits

(defthm w-state-of-aignet-vals-sat-care-masks-lits
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-lits
             lits inmasks regmasks
             invals regvals vals mark aignet state)))
    (equal (w new-state) (w state))))

Theorem: aignet-vals-sat-care-masks-lits-of-lit-list-fix-lits

(defthm aignet-vals-sat-care-masks-lits-of-lit-list-fix-lits
  (equal (aignet-vals-sat-care-masks-lits
              (lit-list-fix lits)
              inmasks regmasks
              invals regvals vals mark aignet state)
         (aignet-vals-sat-care-masks-lits
              lits inmasks regmasks
              invals regvals vals mark aignet state)))

Theorem: aignet-vals-sat-care-masks-lits-lit-list-equiv-congruence-on-lits

(defthm
  aignet-vals-sat-care-masks-lits-lit-list-equiv-congruence-on-lits
  (implies (satlink::lit-list-equiv lits lits-equiv)
           (equal (aignet-vals-sat-care-masks-lits
                       lits inmasks regmasks
                       invals regvals vals mark aignet state)
                  (aignet-vals-sat-care-masks-lits
                       lits-equiv inmasks regmasks
                       invals regvals vals mark aignet state)))
  :rule-classes :congruence)

Theorem: aignet-vals-sat-care-masks-lits-of-node-list-fix-aignet

(defthm aignet-vals-sat-care-masks-lits-of-node-list-fix-aignet
  (equal (aignet-vals-sat-care-masks-lits
              lits inmasks regmasks invals
              regvals vals mark (node-list-fix aignet)
              state)
         (aignet-vals-sat-care-masks-lits
              lits inmasks regmasks
              invals regvals vals mark aignet state)))

Theorem: aignet-vals-sat-care-masks-lits-node-list-equiv-congruence-on-aignet

(defthm
 aignet-vals-sat-care-masks-lits-node-list-equiv-congruence-on-aignet
 (implies (node-list-equiv aignet aignet-equiv)
          (equal (aignet-vals-sat-care-masks-lits
                      lits inmasks regmasks
                      invals regvals vals mark aignet state)
                 (aignet-vals-sat-care-masks-lits
                      lits inmasks regmasks invals
                      regvals vals mark aignet-equiv state)))
 :rule-classes :congruence)