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

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 id.

Signature

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

Arguments

id — ID to traverse.
    Guard (natp id).

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-rec

(defun aignet-vals-sat-care-masks-rec
       (id inmasks regmasks
           invals regvals vals mark aignet state)
 (declare
    (xargs :stobjs (inmasks regmasks
                            invals regvals vals mark aignet state)))
 (declare (xargs :guard (natp id)))
 (declare
  (xargs
   :guard
   (and (id-existsp id aignet)
        (non-exec
             (equal vals
                    (aignet-record-vals nil invals regvals aignet)))
        (not (equal (id->type id aignet) (out-type)))
        (<= (num-ins aignet)
            (bits-length inmasks))
        (<= (num-regs aignet)
            (bits-length regmasks))
        (<= (num-ins aignet)
            (bits-length invals))
        (<= (num-regs aignet)
            (bits-length regvals))
        (< id (bits-length vals))
        (< id (bits-length mark)))))
 (let ((__function__ 'aignet-vals-sat-care-masks-rec))
  (declare (ignorable __function__))
  (b* (((when (eql 1 (get-bit id mark)))
        (mv inmasks regmasks mark state))
       (mark (set-bit id 1 mark)))
   (aignet-case
    (id->type id aignet)
    :in
    (if (eql 1 (id->regp id aignet))
        (b* ((regmasks (set-bit (ci-id->ionum id aignet)
                                1 regmasks)))
          (mv inmasks regmasks mark state))
      (b* ((inmasks (set-bit (ci-id->ionum id aignet)
                             1 inmasks)))
        (mv inmasks regmasks mark state)))
    :out (mv inmasks regmasks mark state)
    :const (mv inmasks regmasks mark state)
    :gate
    (b* ((val (mbe :logic (id-eval id invals regvals aignet)
                   :exec (get-bit id vals)))
         (f0 (gate-id->fanin0 id aignet))
         (f1 (gate-id->fanin1 id aignet))
         ((when (or (eql val 1)
                    (eql (id->regp id aignet) 1)))
          (b* (((mv inmasks regmasks mark state)
                (aignet-vals-sat-care-masks-rec
                     (lit-id f0)
                     inmasks regmasks
                     invals regvals vals mark aignet state)))
            (aignet-vals-sat-care-masks-rec
                 (lit-id f1)
                 inmasks regmasks
                 invals regvals vals mark aignet state)))
         ((when (eql (mbe :logic (lit-eval f0 invals regvals aignet)
                          :exec (aignet-eval-lit f0 vals))
                     1))
          (aignet-vals-sat-care-masks-rec
               (lit-id f1)
               inmasks regmasks
               invals regvals vals mark aignet state))
         ((when (eql (mbe :logic (lit-eval f1 invals regvals aignet)
                          :exec (aignet-eval-lit f1 vals))
                     1))
          (aignet-vals-sat-care-masks-rec
               (lit-id f0)
               inmasks regmasks
               invals regvals vals mark aignet state))
         ((when (or (eql 1 (get-bit (lit-id f0) mark))
                    (eql 1 (get-bit (lit-id f1) mark))))
          (mv inmasks regmasks mark state))
         ((mv coinflip state) (random$ 2 state)))
      (if (eql 1 coinflip)
          (aignet-vals-sat-care-masks-rec
               (lit-id f1)
               inmasks regmasks
               invals regvals vals mark aignet state)
        (aignet-vals-sat-care-masks-rec
             (lit-id f0)
             inmasks regmasks invals
             regvals vals mark aignet state)))))))

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

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

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

(defthm aignet-vals-sat-care-masks-preserve-marks
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-rec
             id 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-preserve-inmasks

(defthm aignet-vals-sat-care-masks-preserve-inmasks
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-rec
             id 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-preserve-regmasks

(defthm aignet-vals-sat-care-masks-preserve-regmasks
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-rec
             id 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

(defthm inmasks-length-of-aignet-vals-sat-care-masks
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-rec
             id 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

(defthm regmasks-length-of-aignet-vals-sat-care-masks
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-rec
             id 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

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

Function: aignet-vals-sat-care-masks-mark-ok

(defun aignet-vals-sat-care-masks-mark-ok
       (node mark invals regvals aignet)
 (declare (xargs :non-executable t))
 (prog2$
  (acl2::throw-nonexec-error 'aignet-vals-sat-care-masks-mark-ok
                             (list node mark invals regvals aignet))
  (implies
   (equal (nth node mark) 1)
   (and
    (implies
     (equal (stype (car (lookup-id node aignet)))
            (and-stype))
     (and
      (implies
         (equal (id-eval node invals regvals aignet)
                1)
         (and (equal (nth (lit-id (fanin 0 (lookup-id node aignet)))
                          mark)
                     1)
              (equal (nth (lit-id (fanin 1 (lookup-id node aignet)))
                          mark)
                     1)))
      (implies
       (and
        (equal (id-eval node invals regvals aignet)
               0)
        (not
         (and (equal (lit-eval (fanin 0 (lookup-id node aignet))
                               invals regvals aignet)
                     0)
              (equal (nth (lit-id (fanin 0 (lookup-id node aignet)))
                          mark)
                     1))))
       (and (equal (lit-eval (fanin 1 (lookup-id node aignet))
                             invals regvals aignet)
                   0)
            (equal (nth (lit-id (fanin 1 (lookup-id node aignet)))
                        mark)
                   1)))))
    (implies
         (equal (stype (car (lookup-id node aignet)))
                (xor-stype))
         (and (equal (nth (lit-id (fanin 0 (lookup-id node aignet)))
                          mark)
                     1)
              (equal (nth (lit-id (fanin 1 (lookup-id node aignet)))
                          mark)
                     1)))))))

Theorem: aignet-vals-sat-care-masks-mark-invar-necc

(defthm aignet-vals-sat-care-masks-mark-invar-necc
  (implies (aignet-vals-sat-care-masks-mark-invar
                id mark invals regvals aignet)
           (implies (<= (nfix node) (nfix id))
                    (aignet-vals-sat-care-masks-mark-ok
                         node mark invals regvals aignet))))

Theorem: aignet-vals-sat-care-masks-mark-invar-rw

(defthm aignet-vals-sat-care-masks-mark-invar-rw
 (implies
  (and (aignet-vals-sat-care-masks-mark-invar
            id mark invals regvals aignet)
       (<= (nfix node) (nfix id))
       (equal (nth node mark) 1))
  (and
   (implies
    (equal (stype (car (lookup-id node aignet)))
           (and-stype))
    (and
     (implies
         (equal (id-eval node invals regvals aignet)
                1)
         (and (equal (nth (lit-id (fanin 0 (lookup-id node aignet)))
                          mark)
                     1)
              (equal (nth (lit-id (fanin 1 (lookup-id node aignet)))
                          mark)
                     1)))
     (implies
         (and (equal (id-eval node invals regvals aignet)
                     0)
              (equal (lit-eval (fanin 0 (lookup-id node aignet))
                               invals regvals aignet)
                     1))
         (and (equal (lit-eval (fanin 1 (lookup-id node aignet))
                               invals regvals aignet)
                     0)
              (equal (nth (lit-id (fanin 1 (lookup-id node aignet)))
                          mark)
                     1)))
     (implies
      (and
         (equal (id-eval node invals regvals aignet)
                0)
         (not (equal (nth (lit-id (fanin 0 (lookup-id node aignet)))
                          mark)
                     1)))
      (and (equal (lit-eval (fanin 1 (lookup-id node aignet))
                            invals regvals aignet)
                  0)
           (equal (nth (lit-id (fanin 1 (lookup-id node aignet)))
                       mark)
                  1)))
     (implies
         (and (equal (id-eval node invals regvals aignet)
                     0)
              (equal (lit-eval (fanin 1 (lookup-id node aignet))
                               invals regvals aignet)
                     1))
         (and (equal (lit-eval (fanin 0 (lookup-id node aignet))
                               invals regvals aignet)
                     0)
              (equal (nth (lit-id (fanin 0 (lookup-id node aignet)))
                          mark)
                     1)))
     (implies
      (and
         (equal (id-eval node invals regvals aignet)
                0)
         (not (equal (nth (lit-id (fanin 1 (lookup-id node aignet)))
                          mark)
                     1)))
      (and (equal (lit-eval (fanin 0 (lookup-id node aignet))
                            invals regvals aignet)
                  0)
           (equal (nth (lit-id (fanin 0 (lookup-id node aignet)))
                       mark)
                  1)))))
   (implies
        (equal (stype (car (lookup-id node aignet)))
               (xor-stype))
        (and (equal (nth (lit-id (fanin 0 (lookup-id node aignet)))
                         mark)
                    1)
             (equal (nth (lit-id (fanin 1 (lookup-id node aignet)))
                         mark)
                    1))))))

Theorem: aignet-vals-sat-care-masks-mark-invar-when-lesser-id

(defthm aignet-vals-sat-care-masks-mark-invar-when-lesser-id
  (implies (and (aignet-vals-sat-care-masks-mark-invar
                     id mark invals regvals aignet)
                (<= (nfix id2) (nfix id)))
           (aignet-vals-sat-care-masks-mark-invar
                id2 mark invals regvals aignet)))

Theorem: aignet-vals-sat-care-masks-mark-invar-of-mark-greater-id

(defthm aignet-vals-sat-care-masks-mark-invar-of-mark-greater-id
 (implies
   (and (aignet-vals-sat-care-masks-mark-invar
             id mark invals regvals aignet)
        (< (nfix id) (nfix id2)))
   (aignet-vals-sat-care-masks-mark-invar id (update-nth id2 1 mark)
                                          invals regvals aignet)))

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

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

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

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

Theorem: aignet-vals-sat-care-masks-mark-ok-of-update-mark

(defthm aignet-vals-sat-care-masks-mark-ok-of-update-mark
 (implies
     (and (aignet-vals-sat-care-masks-mark-ok
               node mark invals regvals aignet)
          (not (equal (nfix id) (nfix node))))
     (aignet-vals-sat-care-masks-mark-ok node (update-nth id 1 mark)
                                         invals regvals aignet)))

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

(defthm aignet-vals-sat-care-masks-mark-ok-preserved
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-rec
             id 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-mark-invar-preserved

(defthm aignet-vals-sat-care-masks-mark-invar-preserved
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-rec
             id 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-marked-inputs-are-masked-necc

(defthm aignet-marked-inputs-are-masked-necc
 (implies
     (aignet-marked-inputs-are-masked mark inmasks aignet)
     (implies
          (and (< (nfix n) (num-ins aignet))
               (equal 1
                      (nth (fanin-count (lookup-stype n :pi aignet))
                           mark)))
          (equal (nth n inmasks) 1))))

Theorem: aignet-marked-inputs-are-masked-of-update-non-input

(defthm aignet-marked-inputs-are-masked-of-update-non-input
 (implies (and (aignet-marked-inputs-are-masked mark inmasks aignet)
               (not (equal (stype (car (lookup-id id aignet)))
                           :pi)))
          (aignet-marked-inputs-are-masked (update-nth id 1 mark)
                                           inmasks aignet)))

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

(defthm aignet-vals-sat-care-masks-preserves-marked-inputs-masked
 (b* (((mv ?new-inmasks
           ?new-regmasks ?new-mark ?new-state)
       (aignet-vals-sat-care-masks-rec
            id 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-marked-regs-are-masked-necc

(defthm aignet-marked-regs-are-masked-necc
 (implies
    (aignet-marked-regs-are-masked mark regmasks aignet)
    (implies
         (and (< (nfix n) (num-regs aignet))
              (equal 1
                     (nth (fanin-count (lookup-stype n :reg aignet))
                          mark)))
         (equal (nth n regmasks) 1))))

Theorem: aignet-marked-regs-are-masked-of-update-non-input

(defthm aignet-marked-regs-are-masked-of-update-non-input
  (implies (and (aignet-marked-regs-are-masked mark regmasks aignet)
                (not (equal (stype (car (lookup-id id aignet)))
                            :reg)))
           (aignet-marked-regs-are-masked (update-nth id 1 mark)
                                          regmasks aignet)))

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

(defthm aignet-vals-sat-care-masks-preserves-marked-regs-masked
 (b* (((mv ?new-inmasks
           ?new-regmasks ?new-mark ?new-state)
       (aignet-vals-sat-care-masks-rec
            id 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: vals-equiv-under-masks-necc

(defthm vals-equiv-under-masks-necc
  (implies (vals-equiv-under-masks masks invals1 invals2)
           (implies (equal (nth n masks) 1)
                    (equal (nth n invals1)
                           (nth n invals2)))))

Theorem: aignet-vals-sat-care-masks-rec-invariants-imply-counterexample-holds-under-masks

(defthm
 aignet-vals-sat-care-masks-rec-invariants-imply-counterexample-holds-under-masks
 (implies (and (aignet-vals-sat-care-masks-mark-invar
                    max-id mark invals regvals aignet)
               (aignet-marked-inputs-are-masked mark inmasks aignet)
               (aignet-marked-regs-are-masked mark regmasks aignet)
               (vals-equiv-under-masks inmasks invals invals1)
               (vals-equiv-under-masks regmasks regvals regvals1)
               (equal (nth id mark) 1)
               (not (equal (id->type id aignet) (out-type)))
               (<= (nfix id) (nfix max-id)))
          (equal (id-eval id invals regvals aignet)
                 (id-eval id invals1 regvals1 aignet))))

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

(defthm aignet-vals-sat-care-masks-rec-counterexample-under-masks
  (b* (((mv ?new-inmasks
            ?new-regmasks ?new-mark ?new-state)
        (aignet-vals-sat-care-masks-rec
             id 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
                   id mark invals regvals aignet)
              (aignet-marked-inputs-are-masked mark inmasks aignet)
              (aignet-marked-regs-are-masked mark regmasks aignet)
              (not (equal (id->type id aignet)
                          (out-type))))
         (equal (id-eval id invals1 regvals1 aignet)
                (id-eval id invals regvals aignet)))))

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

(defthm
 aignet-vals-sat-care-masks-rec-counterexample-under-masks-lit-eval
 (b* (((mv ?new-inmasks
           ?new-regmasks ?new-mark ?new-state)
       (aignet-vals-sat-care-masks-rec
            id 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
                  id mark invals regvals aignet)
             (aignet-marked-inputs-are-masked mark inmasks aignet)
             (aignet-marked-regs-are-masked mark regmasks aignet)
             (not (equal (id->type id aignet) (out-type)))
             (equal (lit-id x) (nfix id)))
        (equal (lit-eval x invals1 regvals1 aignet)
               (lit-eval x invals regvals aignet)))))

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

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

Theorem: aignet-vals-sat-care-masks-rec-of-nfix-id

(defthm aignet-vals-sat-care-masks-rec-of-nfix-id
  (equal (aignet-vals-sat-care-masks-rec
              (nfix id)
              inmasks regmasks
              invals regvals vals mark aignet state)
         (aignet-vals-sat-care-masks-rec
              id inmasks regmasks
              invals regvals vals mark aignet state)))

Theorem: aignet-vals-sat-care-masks-rec-nat-equiv-congruence-on-id

(defthm aignet-vals-sat-care-masks-rec-nat-equiv-congruence-on-id
  (implies (nat-equiv id id-equiv)
           (equal (aignet-vals-sat-care-masks-rec
                       id inmasks regmasks
                       invals regvals vals mark aignet state)
                  (aignet-vals-sat-care-masks-rec
                       id-equiv inmasks regmasks
                       invals regvals vals mark aignet state)))
  :rule-classes :congruence)

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

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

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

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