• 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
        • Aignet-m-assumption-n-output-transforms
          • M-assumption-n-output-comb-transform
          • Apply-m-assumption-n-output-transform
            • Apply-m-assumption-n-output-transforms
            • Apply-m-assumption-n-output-transform!
            • Apply-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
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Apply-m-assumption-n-output-transform

Apply-m-assumption-n-output-transforms

Signature

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

Arguments

m — Guard (natp m).

n — Guard (natp n).

Definitions and Theorems

Function: apply-m-assumption-n-output-transforms

(defun
 apply-m-assumption-n-output-transforms
 (m n aignet aignet2 transforms 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-transforms))
  (declare (ignorable __function__))
  (prog2$
   (print-aignet-stats "Input" aignet)
   (time$
       (b* (((unless (consp transforms))
             (b* ((aignet2 (aignet-raw-copy aignet aignet2)))
                 (mv aignet2 state))))
           (mbe :logic (non-exec (apply-m-assumption-n-output-transforms!-core
                                      m n aignet transforms state))
                :exec (b* (((mv aignet2 state)
                            (apply-m-assumption-n-output-transform
                                 m n aignet aignet2 (car transforms)
                                 state))
                           ((local-stobjs aignet3)
                            (mv aignet2 aignet3 state)))
                          (apply-m-assumption-n-output-transforms-in-place
                               m n aignet2 aignet3 (cdr transforms)
                               state))))
       :msg "All transforms: ~st seconds, ~sa bytes.~%"))))

Theorem: normalize-inputs-of-apply-m-assumption-n-output-transforms

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

Theorem: num-ins-of-apply-m-assumption-n-output-transforms

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

Theorem: num-regs-of-apply-m-assumption-n-output-transforms

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

Theorem: num-outs-of-apply-m-assumption-n-output-transforms

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

Theorem: apply-m-assumption-n-output-transforms-correct

(defthm
 apply-m-assumption-n-output-transforms-correct
 (b*
  (((mv ?new-aignet2 ?new-state)
    (apply-m-assumption-n-output-transforms
         m n aignet aignet2 transforms state)))
  (and
   (implies (< (nfix i) (nfix m))
            (equal (output-eval i invals regvals new-aignet2)
                   (output-eval i invals regvals aignet)))
   (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-transforms

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

Theorem: list-of-outputs-of-apply-m-assumption-n-output-transforms

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