• 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-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
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Aignet

Aignet-simplify-with-tracking

Signature

(aignet-simplify-with-tracking aignet assum-lits 
                               pres-lits track-lits config state) 
 
  → 
(mv new-aignet new-assum-lits 
    new-pres-lits new-track-lits new-state) 

Arguments

aignet — AIG to be transformed.

assum-lits — Literals that are assumed.
    Guard (lit-listp assum-lits).

pres-lits — Literals to be preserved.
    Guard (lit-listp pres-lits).

track-lits — Specifies literals to be tracked (again not necessarily preserved), ordered. They will be added as outputs ot the transformed AIG after the assumption and preserved lits. This is provided so that users may provide output numbers for these literals as hints to transformations.
    Guard (lit-listp track-lits).

config — Combinational transformation config.

Returns

new-assum-lits — Type (lit-listp new-assum-lits).

new-pres-lits — Type (lit-listp new-pres-lits).

new-track-lits — Type (lit-listp new-track-lits).

Definitions and Theorems

Function: aignet-simplify-with-tracking

(defun
 aignet-simplify-with-tracking
 (aignet assum-lits
         pres-lits track-lits config state)
 (declare (xargs :stobjs (aignet state)))
 (declare (xargs :guard (and (lit-listp assum-lits)
                             (lit-listp pres-lits)
                             (lit-listp track-lits))))
 (declare (xargs :guard (and (aignet-lit-listp assum-lits aignet)
                             (aignet-lit-listp pres-lits aignet)
                             (aignet-lit-listp track-lits aignet))))
 (let ((__function__ 'aignet-simplify-with-tracking))
      (declare (ignorable __function__))
      (b* (((local-stobjs aignet2)
            (mv aignet2 aignet new-assum-lits
                new-pres-lits new-track-lits state))
           (aignet2 (aignet-raw-copy-fanins-top aignet aignet2))
           (aignet2 (aignet-add-outs assum-lits aignet2))
           (assum-outs (num-outs aignet2))
           (aignet2 (aignet-add-outs pres-lits aignet2))
           (preserved-outs (num-outs aignet2))
           (aignet2 (aignet-add-outs track-lits aignet2))
           (tracked-outs (num-outs aignet2))
           ((mv aignet2 state)
            (apply-m-assumption-n-output-transforms!
                 assum-outs (- preserved-outs assum-outs)
                 aignet2 config state))
           (lits (aignet-output-lits 0 aignet2))
           (new-assum-lits (take assum-outs lits))
           (new-pres-lits (take (- preserved-outs assum-outs)
                                (nthcdr assum-outs lits)))
           (new-track-lits (take (- tracked-outs preserved-outs)
                                 (nthcdr preserved-outs lits)))
           (aignet (aignet-raw-copy-fanins-top aignet2 aignet)))
          (mv aignet2 aignet new-assum-lits
              new-pres-lits new-track-lits state))))

Theorem: lit-listp-of-aignet-simplify-with-tracking.new-assum-lits

(defthm lit-listp-of-aignet-simplify-with-tracking.new-assum-lits
        (b* (((mv ?new-aignet
                  ?new-assum-lits ?new-pres-lits
                  ?new-track-lits ?new-state)
              (aignet-simplify-with-tracking
                   aignet assum-lits
                   pres-lits track-lits config state)))
            (lit-listp new-assum-lits))
        :rule-classes :rewrite)

Theorem: lit-listp-of-aignet-simplify-with-tracking.new-pres-lits

(defthm lit-listp-of-aignet-simplify-with-tracking.new-pres-lits
        (b* (((mv ?new-aignet
                  ?new-assum-lits ?new-pres-lits
                  ?new-track-lits ?new-state)
              (aignet-simplify-with-tracking
                   aignet assum-lits
                   pres-lits track-lits config state)))
            (lit-listp new-pres-lits))
        :rule-classes :rewrite)

Theorem: lit-listp-of-aignet-simplify-with-tracking.new-track-lits

(defthm lit-listp-of-aignet-simplify-with-tracking.new-track-lits
        (b* (((mv ?new-aignet
                  ?new-assum-lits ?new-pres-lits
                  ?new-track-lits ?new-state)
              (aignet-simplify-with-tracking
                   aignet assum-lits
                   pres-lits track-lits config state)))
            (lit-listp new-track-lits))
        :rule-classes :rewrite)

Theorem: stype-count-of-aignet-simplify-with-tracking

(defthm stype-count-of-aignet-simplify-with-tracking
        (b* (((mv ?new-aignet
                  ?new-assum-lits ?new-pres-lits
                  ?new-track-lits ?new-state)
              (aignet-simplify-with-tracking
                   aignet assum-lits
                   pres-lits track-lits config state)))
            (and (equal (stype-count :pi new-aignet)
                        (stype-count :pi aignet))
                 (equal (stype-count :reg new-aignet)
                        (stype-count :reg aignet))
                 (equal (stype-count :po new-aignet) 0)
                 (equal (stype-count :nxst new-aignet)
                        0))))

Theorem: eval-of-aignet-simplify-with-tracking-when-preserved

(defthm
 eval-of-aignet-simplify-with-tracking-when-preserved
 (b*
  (((mv ?new-aignet
        ?new-assum-lits ?new-pres-lits
        ?new-track-lits ?new-state)
    (aignet-simplify-with-tracking
         aignet assum-lits
         pres-lits track-lits config state)))
  (implies
   (and
     (aignet-lit-listp pres-lits aignet)
     (equal
          (aignet-eval-conjunction assum-lits invals regvals aignet)
          1))
   (equal (lit-eval (nth n new-pres-lits)
                    invals regvals new-aignet)
          (lit-eval (nth n pres-lits)
                    invals regvals aignet)))))

Theorem: eval-of-aignet-simplify-with-tracking-when-assumption

(defthm eval-of-aignet-simplify-with-tracking-when-assumption
        (b* (((mv ?new-aignet
                  ?new-assum-lits ?new-pres-lits
                  ?new-track-lits ?new-state)
              (aignet-simplify-with-tracking
                   aignet assum-lits
                   pres-lits track-lits config state)))
            (implies (aignet-lit-listp assum-lits aignet)
                     (equal (lit-eval (nth n new-assum-lits)
                                      invals regvals new-aignet)
                            (lit-eval (nth n assum-lits)
                                      invals regvals aignet)))))

Theorem: aignet-lit-listp-of-aignet-simplify-with-tracking-pres-lits

(defthm aignet-lit-listp-of-aignet-simplify-with-tracking-pres-lits
        (b* (((mv ?new-aignet
                  ?new-assum-lits ?new-pres-lits
                  ?new-track-lits ?new-state)
              (aignet-simplify-with-tracking
                   aignet assum-lits
                   pres-lits track-lits config state)))
            (implies (aignet-lit-listp pres-lits aignet)
                     (aignet-lit-listp new-pres-lits new-aignet))))

Theorem: aignet-lit-listp-of-aignet-simplify-with-tracking-assum-lits

(defthm aignet-lit-listp-of-aignet-simplify-with-tracking-assum-lits
        (b* (((mv ?new-aignet
                  ?new-assum-lits ?new-pres-lits
                  ?new-track-lits ?new-state)
              (aignet-simplify-with-tracking
                   aignet assum-lits
                   pres-lits track-lits config state)))
            (implies (aignet-lit-listp assum-lits aignet)
                     (aignet-lit-listp new-assum-lits new-aignet))))

Theorem: aignet-lit-listp-of-aignet-simplify-with-tracking-track-lits

(defthm aignet-lit-listp-of-aignet-simplify-with-tracking-track-lits
        (b* (((mv ?new-aignet
                  ?new-assum-lits ?new-pres-lits
                  ?new-track-lits ?new-state)
              (aignet-simplify-with-tracking
                   aignet assum-lits
                   pres-lits track-lits config state)))
            (implies (aignet-lit-listp track-lits aignet)
                     (aignet-lit-listp new-track-lits new-aignet))))

Theorem: len-of-aignet-simplify-with-tracking-pres-lits

(defthm len-of-aignet-simplify-with-tracking-pres-lits
        (b* (((mv ?new-aignet
                  ?new-assum-lits ?new-pres-lits
                  ?new-track-lits ?new-state)
              (aignet-simplify-with-tracking
                   aignet assum-lits
                   pres-lits track-lits config state)))
            (equal (len new-pres-lits)
                   (len pres-lits))))

Theorem: len-of-aignet-simplify-with-tracking-assum-lits

(defthm len-of-aignet-simplify-with-tracking-assum-lits
        (b* (((mv ?new-aignet
                  ?new-assum-lits ?new-pres-lits
                  ?new-track-lits ?new-state)
              (aignet-simplify-with-tracking
                   aignet assum-lits
                   pres-lits track-lits config state)))
            (equal (len new-assum-lits)
                   (len assum-lits))))

Theorem: len-of-aignet-simplify-with-tracking-track-lits

(defthm len-of-aignet-simplify-with-tracking-track-lits
        (b* (((mv ?new-aignet
                  ?new-assum-lits ?new-pres-lits
                  ?new-track-lits ?new-state)
              (aignet-simplify-with-tracking
                   aignet assum-lits
                   pres-lits track-lits config state)))
            (equal (len new-track-lits)
                   (len track-lits))))

Theorem: w-state-of-aignet-simplify-with-tracking

(defthm w-state-of-aignet-simplify-with-tracking
        (b* (((mv ?new-aignet
                  ?new-assum-lits ?new-pres-lits
                  ?new-track-lits ?new-state)
              (aignet-simplify-with-tracking
                   aignet assum-lits
                   pres-lits track-lits config state)))
            (equal (w new-state) (w state))))