• 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-output-ranges
        • Aignet-comb-transforms
          • Fraig
          • Parametrize
          • Observability-fix
          • Constprop
          • Apply-m-assumption-n-output-output-transform-default
          • Balance
          • Apply-n-output-comb-transform-default
          • Apply-comb-transform-default
          • Obs-constprop
          • Rewrite
          • Comb-transform
          • Abc-comb-simplify
          • Prune
          • Rewrite!
          • M-assumption-n-output-comb-transform->name
          • N-output-comb-transform->name
          • Comb-transform->name
          • N-output-comb-transformlist
          • M-assumption-n-output-comb-transformlist
          • Comb-transformlist
          • Apply-comb-transform
        • Aignet-m-assumption-n-output-transforms
        • Aignet-n-output-comb-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-comb-transforms

Rewrite!

Apply DAG-aware rewriting to the network.

Signature

(rewrite! aignet config) → new-aignet

Arguments

aignet — Input aignet -- overwritten.

config — Guard (rewrite-config-p config).

Note: This implementation is heavily based on the one in ABC, developed and maintained at Berkeley by Alan Mishchenko.

Settings for the transform can be tweaked using the config input, which is a rewrite-config object.

Definitions and Theorems

Function: rewrite!

(defun rewrite! (aignet config)
 (declare (xargs :stobjs (aignet)))
 (declare (xargs :guard (rewrite-config-p config)))
 (let ((__function__ 'rewrite!))
   (declare (ignorable __function__))
   (b*
    (((local-stobjs aignet-tmp)
      (mv aignet aignet-tmp))
     (aignet-tmp (rewrite-core aignet aignet-tmp config))
     (aignet (aignet-prune-comb aignet-tmp aignet
                                (rewrite-config->gatesimp config))))
    (mv aignet aignet-tmp))))

Theorem: stype-counts-of-rewrite!

(defthm stype-counts-of-rewrite!
  (b* ((?new-aignet (rewrite! aignet config)))
    (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)
                (stype-count :po aignet)))))

Theorem: rewrite!-correct

(defthm rewrite!-correct
  (b* ((?new-aignet (rewrite! aignet config)))
    (comb-equiv new-aignet aignet)))

Theorem: rewrite!-of-node-list-fix-aignet

(defthm rewrite!-of-node-list-fix-aignet
  (equal (rewrite! (node-list-fix aignet) config)
         (rewrite! aignet config)))

Theorem: rewrite!-node-list-equiv-congruence-on-aignet

(defthm rewrite!-node-list-equiv-congruence-on-aignet
  (implies (node-list-equiv aignet aignet-equiv)
           (equal (rewrite! aignet config)
                  (rewrite! aignet-equiv config)))
  :rule-classes :congruence)

Theorem: rewrite!-of-rewrite-config-fix-config

(defthm rewrite!-of-rewrite-config-fix-config
  (equal (rewrite! aignet (rewrite-config-fix config))
         (rewrite! aignet config)))

Theorem: rewrite!-rewrite-config-equiv-congruence-on-config

(defthm rewrite!-rewrite-config-equiv-congruence-on-config
  (implies (rewrite-config-equiv config config-equiv)
           (equal (rewrite! aignet config)
                  (rewrite! aignet config-equiv)))
  :rule-classes :congruence)