• 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
            • Apply-comb-transforms
            • Apply-comb-transform!
            • Apply-comb-transforms!
        • 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

• Apply-comb-transform

Apply-comb-transforms

Signature

(apply-comb-transforms aignet 
                       aignet2 transforms output-ranges state) 
 
  → 
(mv new-aignet2 new-output-ranges new-state)

Arguments

output-ranges — Guard (aignet-output-range-map-p output-ranges).

Returns

new-output-ranges — Type (aignet-output-range-map-p new-output-ranges).

Definitions and Theorems

Function: apply-comb-transforms

(defun apply-comb-transforms
       (aignet aignet2 transforms output-ranges state)
 (declare (xargs :stobjs (aignet aignet2 state)))
 (declare (xargs :guard (aignet-output-range-map-p output-ranges)))
 (declare (xargs :guard t))
 (let ((__function__ 'apply-comb-transforms))
  (declare (ignorable __function__))
  (prog2$
   (print-aignet-stats "Input" aignet)
   (time$
    (b* (((unless (consp transforms))
          (b* ((aignet2 (aignet-raw-copy aignet aignet2)))
            (mv aignet2
                (aignet-output-range-map-fix output-ranges)
                state))))
     (mbe
         :logic
         (non-exec (apply-comb-transforms!-core
                        aignet transforms output-ranges state))
         :exec
         (b* (((mv aignet2 output-ranges state)
               (apply-comb-transform aignet aignet2 (car transforms)
                                     output-ranges state))
              ((local-stobjs aignet3)
               (mv aignet2 aignet3 output-ranges state)))
           (apply-comb-transforms-in-place
                aignet2 aignet3 (cdr transforms)
                output-ranges state))))
    :msg "All transforms: ~st seconds, ~sa bytes.~%"))))

Theorem: aignet-output-range-map-p-of-apply-comb-transforms.new-output-ranges

(defthm
 aignet-output-range-map-p-of-apply-comb-transforms.new-output-ranges
 (b* (((mv ?new-aignet2
           ?new-output-ranges ?new-state)
       (apply-comb-transforms aignet aignet2
                              transforms output-ranges state)))
   (aignet-output-range-map-p new-output-ranges))
 :rule-classes :rewrite)

Theorem: normalize-inputs-of-apply-comb-transforms

(defthm normalize-inputs-of-apply-comb-transforms
 (b* nil
  (implies
   (syntaxp (not (equal aignet2 ''nil)))
   (equal
      (apply-comb-transforms aignet
                             aignet2 transforms output-ranges state)
      (let ((aignet2 nil))
        (apply-comb-transforms aignet aignet2
                               transforms output-ranges state))))))

Theorem: num-ins-of-apply-comb-transforms

(defthm num-ins-of-apply-comb-transforms
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (apply-comb-transforms aignet aignet2
                               transforms output-ranges state)))
    (equal (stype-count :pi new-aignet2)
           (stype-count :pi aignet))))

Theorem: num-outs-lower-bound-of-apply-comb-transforms

(defthm num-outs-lower-bound-of-apply-comb-transforms
 (b* (((mv ?new-aignet2
           ?new-output-ranges ?new-state)
       (apply-comb-transforms aignet aignet2
                              transforms output-ranges state)))
   (implies (<= (aignet-output-range-map-length output-ranges)
                (stype-count :po aignet))
            (<= (aignet-output-range-map-length new-output-ranges)
                (stype-count :po new-aignet2))))
 :rule-classes
 ((:linear
   :trigger-terms
   ((stype-count
       :po
       (mv-nth
            0
            (apply-comb-transforms aignet aignet2
                                   transforms output-ranges state)))
    (aignet-output-range-map-length
     (mv-nth
        1
        (apply-comb-transforms aignet aignet2
                               transforms output-ranges state)))))))

Theorem: apply-comb-transforms-comb-equiv

(defthm apply-comb-transforms-comb-equiv
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (apply-comb-transforms aignet aignet2
                               transforms output-ranges state)))
    (comb-equiv new-aignet2 aignet)))

Theorem: num-regs-of-apply-comb-transforms

(defthm num-regs-of-apply-comb-transforms
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (apply-comb-transforms aignet aignet2
                               transforms output-ranges state)))
    (equal (stype-count :reg new-aignet2)
           (stype-count :reg aignet))))

Theorem: num-outs-of-apply-comb-transforms

(defthm num-outs-of-apply-comb-transforms
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (apply-comb-transforms aignet aignet2
                               transforms output-ranges state)))
    (equal (stype-count :po new-aignet2)
           (stype-count :po aignet))))

Theorem: w-state-of-apply-comb-transforms

(defthm w-state-of-apply-comb-transforms
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (apply-comb-transforms aignet aignet2
                               transforms output-ranges state)))
    (equal (w new-state) (w state))))

Theorem: list-of-outputs-of-apply-comb-transforms

(defthm list-of-outputs-of-apply-comb-transforms
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (apply-comb-transforms aignet aignet2
                               transforms output-ranges state)))
    (equal (list new-aignet2 new-output-ranges new-state)
           (apply-comb-transforms aignet aignet2
                                  transforms output-ranges state))))