		Search-engine friendly clone of the ACL2 documentation.

Fraig

Ipasir-maybe-recycle

Signature
(ipasir-maybe-recycle config sat-lits ipasir fraig-stats) → (mv new-sat-lits new-ipasir new-fraig-stats)
Arguments: config — Guard (fraig-config-p config).

Definitions and Theorems

Function: ipasir-maybe-recycle

(defun ipasir-maybe-recycle (config sat-lits ipasir fraig-stats)
 (declare (xargs :stobjs (sat-lits ipasir fraig-stats)))
 (declare (xargs :guard (fraig-config-p config)))
 (declare
  (xargs
   :guard (non-exec (and (not (eq (ipasir$a->status ipasir) :undef))
                         (not (ipasir$a->new-clause ipasir))
                         (not (ipasir$a->assumption ipasir))))))
 (let ((__function__ 'ipasir-maybe-recycle))
   (declare (ignorable __function__))
   (b*
    (((fraig-config config))
     ((unless (and config.ipasir-recycle-count
                   (<= config.ipasir-recycle-count
                       (ipasir-callback-count ipasir))))
      (b* ((ipasir (ipasir-cancel-new-clause ipasir))
           (ipasir (ipasir-cancel-assumption ipasir))
           (ipasir (ipasir-input ipasir)))
        (mv sat-lits ipasir fraig-stats)))
     (fraig-stats (update-fraig-ipasir-recycles
                       (+ 1 (fraig-ipasir-recycles fraig-stats))
                       fraig-stats))
     (fraig-stats (update-fraig-ipasir-prev-callbacks
                       (+ (ipasir-callback-count ipasir)
                          (fraig-ipasir-prev-callbacks fraig-stats))
                       fraig-stats))
     (ipasir (ipasir-release ipasir))
     (ipasir (ipasir-reinit ipasir))
     (ipasir (ipasir-set-limit ipasir config.ipasir-limit))
     (sat-lits (sat-lits-empty (aignet->sat-length sat-lits)
                               sat-lits)))
    (mv sat-lits ipasir fraig-stats))))

Theorem: sat-lits-wfp-of-ipasir-maybe-recycle

(defthm sat-lits-wfp-of-ipasir-maybe-recycle
  (b* (((mv ?new-sat-lits
            ?new-ipasir ?new-fraig-stats)
        (ipasir-maybe-recycle config sat-lits ipasir fraig-stats)))
    (implies (sat-lits-wfp sat-lits aignet)
             (sat-lits-wfp new-sat-lits aignet))))

Theorem: ipasir-new-clause-of-ipasir-maybe-recycle

(defthm ipasir-new-clause-of-ipasir-maybe-recycle
  (b* (((mv ?new-sat-lits
            ?new-ipasir ?new-fraig-stats)
        (ipasir-maybe-recycle config sat-lits ipasir fraig-stats)))
    (equal (ipasir$a->new-clause new-ipasir)
           nil)))

Theorem: ipasir-assumption-of-ipasir-maybe-recycle

(defthm ipasir-assumption-of-ipasir-maybe-recycle
  (b* (((mv ?new-sat-lits
            ?new-ipasir ?new-fraig-stats)
        (ipasir-maybe-recycle config sat-lits ipasir fraig-stats)))
    (equal (ipasir$a->assumption new-ipasir)
           nil)))

Theorem: ipasir-status-of-ipasir-maybe-recycle

(defthm ipasir-status-of-ipasir-maybe-recycle
  (b* (((mv ?new-sat-lits
            ?new-ipasir ?new-fraig-stats)
        (ipasir-maybe-recycle config sat-lits ipasir fraig-stats)))
    (equal (ipasir$a->status new-ipasir)
           :input)))

Theorem: ipasir-formula-wfp-of-ipasir-maybe-recycle

(defthm ipasir-formula-wfp-of-ipasir-maybe-recycle
  (b* (((mv ?new-sat-lits
            ?new-ipasir ?new-fraig-stats)
        (ipasir-maybe-recycle config sat-lits ipasir fraig-stats)))
    (implies (sat-lit-list-listp (ipasir$a->formula ipasir)
                                 sat-lits)
             (sat-lit-list-listp (ipasir$a->formula new-ipasir)
                                 new-sat-lits))))

Theorem: cnf-for-aignet-of-ipasir-maybe-recycle

(defthm cnf-for-aignet-of-ipasir-maybe-recycle
  (b* (((mv ?new-sat-lits
            ?new-ipasir ?new-fraig-stats)
        (ipasir-maybe-recycle config sat-lits ipasir fraig-stats)))
    (implies (cnf-for-aignet aignet (ipasir$a->formula ipasir)
                             sat-lits)
             (cnf-for-aignet aignet (ipasir$a->formula new-ipasir)
                             new-sat-lits))))

Theorem: ipasir-maybe-recycle-of-fraig-config-fix-config

(defthm ipasir-maybe-recycle-of-fraig-config-fix-config
  (equal (ipasir-maybe-recycle (fraig-config-fix config)
                               sat-lits ipasir fraig-stats)
         (ipasir-maybe-recycle config sat-lits ipasir fraig-stats)))

Theorem: ipasir-maybe-recycle-fraig-config-equiv-congruence-on-config

(defthm ipasir-maybe-recycle-fraig-config-equiv-congruence-on-config
 (implies
    (fraig-config-equiv config config-equiv)
    (equal (ipasir-maybe-recycle config sat-lits ipasir fraig-stats)
           (ipasir-maybe-recycle config-equiv
                                 sat-lits ipasir fraig-stats)))
 :rule-classes :congruence)