		Search-engine friendly clone of the ACL2 documentation.

Fraig

Print-fraig-stats-noninitial

Signature
(print-fraig-stats-noninitial classes ipasir fraig-stats mark &key (start-node '0)) → *
Arguments: start-node — Guard (natp start-node).

Definitions and Theorems

Function: print-fraig-stats-noninitial-fn

(defun print-fraig-stats-noninitial-fn
       (classes ipasir fraig-stats mark start-node)
 (declare (xargs :stobjs (classes ipasir fraig-stats mark)))
 (declare (xargs :guard (natp start-node)))
 (declare
  (xargs :guard
         (and (non-exec (not (eq (ipasir$a->status ipasir) :undef)))
              (<= start-node (classes-size classes))
              (<= (classes-size classes)
                  (bits-length mark)))))
 (let ((__function__ 'print-fraig-stats-noninitial))
  (declare (ignorable __function__))
  (b*
    (((mv nclasses nconst-lits nclass-lits)
      (classes-counts-with-mark classes mark
                                :start-node start-node))
     (norig-lits (+ (fraig-initial-nconst-lits fraig-stats)
                    (fraig-initial-nclass-lits fraig-stats)))
     ((when (eql norig-lits 0)) nil)
     (nremaining-lits (+ nconst-lits nclass-lits))
     (percent-times-100 (let ((div (floor (* 20000 nremaining-lits)
                                          norig-lits)))
                          (+ (ash div -1) (logand 1 div))))
     (percent-msg (msg "~x0.~x1~x2%"
                       (floor percent-times-100 100)
                       (mod (floor percent-times-100 10) 10)
                       (mod percent-times-100 10))))
   (cw!
    "~@1 (~x0) of lits remaining. Classes: ~x2 Const lits: ~x3 Class lits: ~x4~%"
    (+ nconst-lits nclass-lits)
    percent-msg
    nclasses nconst-lits nclass-lits)
   (cw!
    "      ~x0 gates processed, ~x1 built, ~x2 coincident, ~x3 proved~%"
    (fraig-gates-processed fraig-stats)
    (- (fraig-gates-processed fraig-stats)
       (+ (fraig-coincident-nodes fraig-stats)
          (fraig-unsat-checks fraig-stats)))
    (fraig-coincident-nodes fraig-stats)
    (fraig-unsat-checks fraig-stats))
   (cw! "       SAT checks: ~x0  unsat: ~x1 sat: ~x2 failed: ~x3~%"
        (+ (fraig-unsat-checks fraig-stats)
           (fraig-sat-checks fraig-stats)
           (fraig-failed-checks fraig-stats))
        (fraig-unsat-checks fraig-stats)
        (fraig-sat-checks fraig-stats)
        (fraig-failed-checks fraig-stats))
   (cw! "                     recycles: ~x0 callbacks: ~x1~%"
        (fraig-ipasir-recycles fraig-stats)
        (+ (ipasir-callback-count ipasir)
           (fraig-ipasir-prev-callbacks fraig-stats))))))

Theorem: print-fraig-stats-noninitial-fn-of-nfix-start-node

(defthm print-fraig-stats-noninitial-fn-of-nfix-start-node
  (equal (print-fraig-stats-noninitial-fn
              classes ipasir
              fraig-stats mark (nfix start-node))
         (print-fraig-stats-noninitial-fn
              classes
              ipasir fraig-stats mark start-node)))

Theorem: print-fraig-stats-noninitial-fn-nat-equiv-congruence-on-start-node

(defthm
 print-fraig-stats-noninitial-fn-nat-equiv-congruence-on-start-node
 (implies (nat-equiv start-node start-node-equiv)
          (equal (print-fraig-stats-noninitial-fn
                      classes
                      ipasir fraig-stats mark start-node)
                 (print-fraig-stats-noninitial-fn
                      classes ipasir
                      fraig-stats mark start-node-equiv)))
 :rule-classes :congruence)