• 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-comb-transforms
          • Fraig
          • Observability-fix
          • Constprop
          • Balance
          • Apply-m-assumption-n-output-output-transform-default
          • Obs-constprop
          • Apply-n-output-comb-transform-default
          • Rewrite
          • Comb-transform
          • Abc-comb-simplify
          • Apply-comb-transform-default
          • 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-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-comb-transforms

Apply-m-assumption-n-output-output-transform-default

Signature

(apply-m-assumption-n-output-output-transform-default 
     m n aignet aignet2 transform state) 
 
  → 
(mv new-aignet2 new-state)

Arguments

m — Guard (natp m).

n — Guard (natp n).

Definitions and Theorems

Function: apply-m-assumption-n-output-output-transform-default

(defun apply-m-assumption-n-output-output-transform-default
       (m n aignet aignet2 transform state)
 (declare (xargs :stobjs (aignet aignet2 state)))
 (declare (xargs :guard (and (natp m) (natp n))))
 (declare (xargs :guard (<= (+ m n) (num-outs aignet))))
 (let ((__function__
            'apply-m-assumption-n-output-output-transform-default))
  (declare (ignorable __function__))
  (b*
   (((unless (m-assumption-n-output-comb-transform-p transform))
     (raise "Bad transform config object; should satisfy ~x1: ~x0~%"
            transform
            'm-assumption-n-output-comb-transform-p)
     (b* ((aignet2 (aignet-raw-copy aignet aignet2)))
       (mv aignet2 state)))
    (name (m-assumption-n-output-comb-transform->name transform)))
   (time$
    (b*
     (((mv aignet2 state)
       (case (tag transform)
        (:balance-config
             (b* ((aignet2 (balance aignet aignet2 transform)))
               (mv aignet2 state)))
        (:fraig-config (fraig aignet aignet2 transform state))
        (:rewrite-config
             (b* ((aignet2 (rewrite aignet aignet2 transform)))
               (mv aignet2 state)))
        (:obs-constprop-config
             (obs-constprop aignet aignet2 transform state))
        (:observability-config
             (observability-fix aignet aignet2 transform state))
        (:constprop-config
             (b* ((aignet2 (constprop aignet aignet2 transform)))
               (mv aignet2 state)))
        (:snapshot-config
             (b* ((state (aignet-write-aiger
                              (snapshot-config->filename transform)
                              aignet state))
                  (aignet2 (aignet-raw-copy aignet aignet2)))
               (mv aignet2 state)))
        (:prune-config
             (b* ((aignet2 (prune aignet aignet2 transform)))
               (mv aignet2 state)))
        (:unreachability-config
           (b* ((aignet2 (unreachability aignet aignet2 transform)))
             (mv aignet2 state)))
        (:dom-supergates-sweep-config
         (b* ((aignet2
                   (dom-supergates-sweep aignet aignet2 transform)))
           (mv aignet2 state)))
        (:n-outputs-unreachability-config
         (b*
          ((aignet2
               (n-outputs-unreachability (+ (lnfix m) (lnfix n))
                                         aignet aignet2 transform)))
          (mv aignet2 state)))
        (:n-outputs-dom-supergates-sweep-config
             (b* ((aignet2 (n-outputs-dom-supergates-sweep
                                (+ (lnfix m) (lnfix n))
                                aignet aignet2 transform)))
               (mv aignet2 state)))
        (:m-assum-n-output-observability-config
             (m-assum-n-output-observability
                  m n aignet aignet2 transform state))
        (otherwise
             (abc-comb-simplify aignet aignet2 transform state))))
      (- (print-aignet-stats name aignet2)))
     (mv aignet2 state))
    :msg "~s0 transform: ~st seconds, ~sa bytes.~%"
    :args (list name)))))

Theorem: normalize-inputs-of-apply-m-assumption-n-output-output-transform-default

(defthm
 normalize-inputs-of-apply-m-assumption-n-output-output-transform-default
 (b* nil
   (implies (syntaxp (not (equal aignet2 ''nil)))
            (equal (apply-m-assumption-n-output-output-transform-default
                        m n aignet aignet2 transform state)
                   (let ((aignet2 nil))
                     (apply-m-assumption-n-output-output-transform-default
                          m n aignet aignet2 transform state))))))

Theorem: num-ins-of-apply-m-assumption-n-output-output-transform-default

(defthm
    num-ins-of-apply-m-assumption-n-output-output-transform-default
  (b* (((mv ?new-aignet2 ?new-state)
        (apply-m-assumption-n-output-output-transform-default
             m n aignet aignet2 transform state)))
    (equal (stype-count :pi new-aignet2)
           (stype-count :pi aignet))))

Theorem: num-regs-of-apply-m-assumption-n-output-output-transform-default

(defthm
   num-regs-of-apply-m-assumption-n-output-output-transform-default
  (b* (((mv ?new-aignet2 ?new-state)
        (apply-m-assumption-n-output-output-transform-default
             m n aignet aignet2 transform state)))
    (equal (stype-count :reg new-aignet2)
           (stype-count :reg aignet))))

Theorem: num-outs-of-apply-m-assumption-n-output-output-transform-default

(defthm
   num-outs-of-apply-m-assumption-n-output-output-transform-default
  (b* (((mv ?new-aignet2 ?new-state)
        (apply-m-assumption-n-output-output-transform-default
             m n aignet aignet2 transform state)))
    (equal (stype-count :po new-aignet2)
           (stype-count :po aignet))))

Theorem: apply-m-assumption-n-output-output-transform-default-eval-assumptions

(defthm
 apply-m-assumption-n-output-output-transform-default-eval-assumptions
 (b* (((mv ?new-aignet2 ?new-state)
       (apply-m-assumption-n-output-output-transform-default
            m n aignet aignet2 transform state)))
   (implies (< (nfix i) (nfix m))
            (equal (output-eval i invals regvals new-aignet2)
                   (output-eval i invals regvals aignet)))))

Theorem: apply-m-assumption-n-output-output-transform-default-eval-conclusion

(defthm
 apply-m-assumption-n-output-output-transform-default-eval-conclusion
 (b* (((mv ?new-aignet2 ?new-state)
       (apply-m-assumption-n-output-output-transform-default
            m n aignet aignet2 transform state)))
   (implies
        (and (< (nfix i) (+ (nfix m) (nfix n)))
             (equal (conjoin-output-range 0 m invals regvals aignet)
                    1))
        (equal (output-eval i invals regvals new-aignet2)
               (output-eval i invals regvals aignet)))))

Theorem: w-state-of-apply-m-assumption-n-output-output-transform-default

(defthm
    w-state-of-apply-m-assumption-n-output-output-transform-default
  (b* (((mv ?new-aignet2 ?new-state)
        (apply-m-assumption-n-output-output-transform-default
             m n aignet aignet2 transform state)))
    (equal (w new-state) (w state))))

Theorem: list-of-outputs-of-apply-m-assumption-n-output-output-transform-default

(defthm
 list-of-outputs-of-apply-m-assumption-n-output-output-transform-default
 (b* (((mv ?new-aignet2 ?new-state)
       (apply-m-assumption-n-output-output-transform-default
            m n aignet aignet2 transform state)))
   (equal (list new-aignet2 new-state)
          (apply-m-assumption-n-output-output-transform-default
               m n aignet aignet2 transform state))))