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

• Aignet

Aignet-simplify-with-tracking

Signature

(aignet-simplify-with-tracking aignet assum-lits 
                               pres-lits litmap config state) 
 
  → 
(mv new-aignet new-assum-lits new-pres-lits new-litmap 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).

litmap — Specifies literals to be tracked, each list of literals labeled by a name (symbol). They will be added as outputs ot the transformed AIG after the nodes specified by bitarr and mark, i.e. the first literal will be set as the N+Mth output where N is the number of bits set in bitarr and N is the number set in mark. These names can be used in transform configurations as hints. The litmap resulting from the transforms will be returned -- this likely, but not necessarily, preserves the same named fields and the logical function of the literals, depending on the transforms used.
    Guard (named-lit-list-map-p litmap).

config — Combinational transformation config.

Returns

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

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

new-litmap — Type (named-lit-list-map-p new-litmap).

Definitions and Theorems

Function: aignet-simplify-with-tracking

(defun aignet-simplify-with-tracking
       (aignet assum-lits
               pres-lits litmap config state)
 (declare (xargs :stobjs (aignet state)))
 (declare (xargs :guard (and (lit-listp assum-lits)
                             (lit-listp pres-lits)
                             (named-lit-list-map-p litmap))))
 (declare
   (xargs
        :guard (and (aignet-lit-listp assum-lits aignet)
                    (aignet-lit-listp pres-lits aignet)
                    (named-lit-list-map-aignet-okp litmap 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-from-lit-list-map litmap aignet2))
    (outmap (list* (cons nil assum-outs)
                   (cons nil (- preserved-outs assum-outs))
                   (named-lit-list-map-to-output-range-map litmap)))
    ((mv aignet2 res-outmap state)
     (apply-m-assumption-n-output-transforms!
          assum-outs (- preserved-outs assum-outs)
          aignet2 config outmap state))
    (lits (aignet-output-lits-range 0 preserved-outs aignet2))
    (new-assum-lits (take assum-outs lits))
    (new-pres-lits (nthcdr assum-outs lits))
    (new-litmap
         (output-range-map-to-lit-list-map 0 res-outmap aignet2))
    (aignet (aignet-raw-copy-fanins-top aignet2 aignet)))
   (mv aignet2 aignet new-assum-lits
       new-pres-lits new-litmap 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-litmap ?new-state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap 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-litmap ?new-state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap config state)))
   (lit-listp new-pres-lits))
  :rule-classes :rewrite)

Theorem: named-lit-list-map-p-of-aignet-simplify-with-tracking.new-litmap

(defthm
   named-lit-list-map-p-of-aignet-simplify-with-tracking.new-litmap
  (b*
   (((mv ?new-aignet ?new-assum-lits
         ?new-pres-lits ?new-litmap ?new-state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap config state)))
   (named-lit-list-map-p new-litmap))
  :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-litmap ?new-state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap 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-litmap ?new-state)
    (aignet-simplify-with-tracking aignet assum-lits
                                   pres-lits litmap 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-litmap ?new-state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap 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-litmap ?new-state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap 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-litmap ?new-state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap config state)))
   (implies (aignet-lit-listp assum-lits aignet)
            (aignet-lit-listp new-assum-lits new-aignet))))

Theorem: named-lit-list-map-aignet-okp-of-aignet-simplify-with-tracking

(defthm
     named-lit-list-map-aignet-okp-of-aignet-simplify-with-tracking
  (b*
   (((mv ?new-aignet ?new-assum-lits
         ?new-pres-lits ?new-litmap ?new-state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap config state)))
   (named-lit-list-map-aignet-okp new-litmap 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-litmap ?new-state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap 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-litmap ?new-state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap config state)))
   (equal (len new-assum-lits)
          (len assum-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-litmap ?new-state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap config state)))
   (equal (w new-state) (w state))))

Theorem: aignet-simplify-with-tracking-of-node-list-fix-aignet

(defthm aignet-simplify-with-tracking-of-node-list-fix-aignet
 (equal
     (aignet-simplify-with-tracking (node-list-fix aignet)
                                    assum-lits
                                    pres-lits litmap config state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap config state)))

Theorem: aignet-simplify-with-tracking-node-list-equiv-congruence-on-aignet

(defthm
 aignet-simplify-with-tracking-node-list-equiv-congruence-on-aignet
 (implies
  (node-list-equiv aignet aignet-equiv)
  (equal
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap config state)
     (aignet-simplify-with-tracking aignet-equiv assum-lits
                                    pres-lits litmap config state)))
 :rule-classes :congruence)

Theorem: aignet-simplify-with-tracking-of-lit-list-fix-assum-lits

(defthm aignet-simplify-with-tracking-of-lit-list-fix-assum-lits
 (equal
     (aignet-simplify-with-tracking aignet (lit-list-fix assum-lits)
                                    pres-lits litmap config state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap config state)))

Theorem: aignet-simplify-with-tracking-lit-list-equiv-congruence-on-assum-lits

(defthm
 aignet-simplify-with-tracking-lit-list-equiv-congruence-on-assum-lits
 (implies
  (satlink::lit-list-equiv assum-lits assum-lits-equiv)
  (equal
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap config state)
     (aignet-simplify-with-tracking aignet assum-lits-equiv
                                    pres-lits litmap config state)))
 :rule-classes :congruence)

Theorem: aignet-simplify-with-tracking-of-lit-list-fix-pres-lits

(defthm aignet-simplify-with-tracking-of-lit-list-fix-pres-lits
 (equal
  (aignet-simplify-with-tracking aignet
                                 assum-lits (lit-list-fix pres-lits)
                                 litmap config state)
  (aignet-simplify-with-tracking aignet assum-lits
                                 pres-lits litmap config state)))

Theorem: aignet-simplify-with-tracking-lit-list-equiv-congruence-on-pres-lits

(defthm
 aignet-simplify-with-tracking-lit-list-equiv-congruence-on-pres-lits
 (implies
  (satlink::lit-list-equiv pres-lits pres-lits-equiv)
  (equal
       (aignet-simplify-with-tracking aignet assum-lits
                                      pres-lits litmap config state)
       (aignet-simplify-with-tracking
            aignet assum-lits
            pres-lits-equiv litmap config state)))
 :rule-classes :congruence)

Theorem: aignet-simplify-with-tracking-of-named-lit-list-map-fix-litmap

(defthm
     aignet-simplify-with-tracking-of-named-lit-list-map-fix-litmap
 (equal
     (aignet-simplify-with-tracking aignet assum-lits pres-lits
                                    (named-lit-list-map-fix litmap)
                                    config state)
     (aignet-simplify-with-tracking aignet assum-lits
                                    pres-lits litmap config state)))

Theorem: aignet-simplify-with-tracking-named-lit-list-map-equiv-congruence-on-litmap

(defthm
 aignet-simplify-with-tracking-named-lit-list-map-equiv-congruence-on-litmap
 (implies
  (named-lit-list-map-equiv litmap litmap-equiv)
  (equal
       (aignet-simplify-with-tracking aignet assum-lits
                                      pres-lits litmap config state)
       (aignet-simplify-with-tracking
            aignet assum-lits
            pres-lits litmap-equiv config state)))
 :rule-classes :congruence)