		Search-engine friendly clone of the ACL2 documentation.

Aignet-ipasir

Aignet-lits-ipasir-sat-check

Performs a single SAT check to determine whether the input AIGNET literal can have the value 1.

Signature
(aignet-lits-ipasir-sat-check x invals regvals vals aignet state) → (mv status sat-invals sat-regvals eval-vals new-state)
Arguments: x — Literals (conjoined) to check for satisfiability.
Guard (lit-listp x).; invals — Bit array, overwritten with the input values of the satisfying assignment.; regvals — Bit array, overwritten with the register values of the satisfying assignment.; vals — Bit array, overwritten with the values of the satisfying assignment for all aignet nodes.; aignet — AIG network.; state — ACL2 state, used to initialize the incremental solver and generate random numbers.
Returns: status — Status of the satisfiability check.
Type (or (equal status :failed) (equal status :unsat) (equal status :sat)) .; sat-invals — If satisfiable, input values of the satisfying assignment.
Type (equal (len sat-invals) (num-ins aignet)).; sat-regvals — If satisfiable, register values of the satisfying assignment.
Type (equal (len sat-regvals) (num-regs aignet)).; eval-vals — If satisfiable, values for all aignet nodes of the satisfying assignment.
Type (implies (equal status :sat) (equal eval-vals (aignet-record-vals vals sat-invals sat-regvals aignet))) .; new-state — Updated ACL2 state.

This uses the ipasir incremental solver interface to perform a SAT check on the given literal. This isn't really the intended use of an incremental solver, but it at least illustrates how to use it.

Definitions and Theorems

Function: aignet-lits-ipasir-sat-check

(defun aignet-lits-ipasir-sat-check
       (x invals regvals vals aignet state)
  (declare (xargs :stobjs (invals regvals vals aignet state)))
  (declare (xargs :guard (lit-listp x)))
  (declare (xargs :guard (aignet-lit-listp x aignet)))
  (let ((__function__ 'aignet-lits-ipasir-sat-check))
    (declare (ignorable __function__))
    (b* (((local-stobjs ipasir sat-lits)
          (mv ipasir sat-lits
              status invals regvals vals state))
         ((mv ipasir sat-lits state)
          (aignet-lits-ipasir-sat-check-aux
               x sat-lits ipasir aignet state))
         ((mv status ipasir)
          (ipasir-solve ipasir))
         (invals (resize-bits (num-ins aignet) invals))
         (regvals (resize-bits (num-regs aignet) regvals))
         ((unless (eq status :sat))
          (b* ((ipasir (ipasir-release ipasir)))
            (mv ipasir sat-lits
                status invals regvals vals state)))
         (invals (aignet-get-ipasir-ctrex-invals
                      0 invals sat-lits aignet ipasir))
         (regvals (aignet-get-ipasir-ctrex-regvals
                       0 regvals sat-lits aignet ipasir))
         (ipasir (ipasir-release ipasir))
         (vals (aignet-record-vals vals invals regvals aignet))
         ((unless (eql (aignet-eval-vals-conjunction x vals)
                       1))
          (raise "Supposed satisfying assignment didn't work!")
          (mv ipasir sat-lits
              :failed invals regvals vals state)))
      (mv ipasir sat-lits
          :sat invals regvals vals state))))

Theorem: return-type-of-aignet-lits-ipasir-sat-check.status

(defthm return-type-of-aignet-lits-ipasir-sat-check.status
  (b* (((mv ?status ?sat-invals
            ?sat-regvals ?eval-vals ?new-state)
        (aignet-lits-ipasir-sat-check
             x invals regvals vals aignet state)))
    (or (equal status :failed)
        (equal status :unsat)
        (equal status :sat)))
  :rule-classes
  ((:forward-chaining
        :trigger-terms
        ((mv-nth 0
                 (aignet-lits-ipasir-sat-check
                      x invals regvals vals aignet state))))))

Theorem: return-type-of-aignet-lits-ipasir-sat-check.sat-invals

(defthm return-type-of-aignet-lits-ipasir-sat-check.sat-invals
  (b* (((mv ?status ?sat-invals
            ?sat-regvals ?eval-vals ?new-state)
        (aignet-lits-ipasir-sat-check
             x invals regvals vals aignet state)))
    (equal (len sat-invals)
           (num-ins aignet)))
  :rule-classes :rewrite)

Theorem: return-type-of-aignet-lits-ipasir-sat-check.sat-regvals

(defthm return-type-of-aignet-lits-ipasir-sat-check.sat-regvals
  (b* (((mv ?status ?sat-invals
            ?sat-regvals ?eval-vals ?new-state)
        (aignet-lits-ipasir-sat-check
             x invals regvals vals aignet state)))
    (equal (len sat-regvals)
           (num-regs aignet)))
  :rule-classes :rewrite)

Theorem: return-type-of-aignet-lits-ipasir-sat-check.eval-vals

(defthm return-type-of-aignet-lits-ipasir-sat-check.eval-vals
 (b* (((mv ?status ?sat-invals
           ?sat-regvals ?eval-vals ?new-state)
       (aignet-lits-ipasir-sat-check
            x invals regvals vals aignet state)))
  (implies
   (equal status :sat)
   (equal eval-vals
          (aignet-record-vals vals sat-invals sat-regvals aignet))))
 :rule-classes :rewrite)

Theorem: satisfying-assign-of-aignet-lits-ipasir-sat-check

(defthm satisfying-assign-of-aignet-lits-ipasir-sat-check
 (b* (((mv ?status ?sat-invals
           ?sat-regvals ?eval-vals ?new-state)
       (aignet-lits-ipasir-sat-check
            x invals regvals vals aignet state)))
  (implies
    (and (equal status :sat)
         (aignet-lit-listp x aignet))
    (equal (aignet-eval-conjunction x sat-invals sat-regvals aignet)
           1))))

Theorem: aignet-lits-ipasir-sat-check-not-unsat-when-sat

(defthm aignet-lits-ipasir-sat-check-not-unsat-when-sat
 (b* (((mv ?status ?sat-invals
           ?sat-regvals ?eval-vals ?new-state)
       (aignet-lits-ipasir-sat-check
            x invals regvals vals aignet state)))
  (implies
   (and
    (equal
         (aignet-eval-conjunction x some-invals some-regvals aignet)
         1)
    (aignet-lit-listp x aignet))
   (not (equal status :unsat)))))

Theorem: w-state-of-aignet-lits-ipasir-sat-check

(defthm w-state-of-aignet-lits-ipasir-sat-check
  (b* (((mv ?status ?sat-invals
            ?sat-regvals ?eval-vals ?new-state)
        (aignet-lits-ipasir-sat-check
             x invals regvals vals aignet state)))
    (equal (w new-state) (w state))))

Theorem: aignet-lits-ipasir-sat-check-of-lit-list-fix-x

(defthm aignet-lits-ipasir-sat-check-of-lit-list-fix-x
 (equal
     (aignet-lits-ipasir-sat-check (lit-list-fix x)
                                   invals regvals vals aignet state)
     (aignet-lits-ipasir-sat-check
          x invals regvals vals aignet state)))

Theorem: aignet-lits-ipasir-sat-check-lit-list-equiv-congruence-on-x

(defthm aignet-lits-ipasir-sat-check-lit-list-equiv-congruence-on-x
 (implies
  (satlink::lit-list-equiv x x-equiv)
  (equal
   (aignet-lits-ipasir-sat-check x invals regvals vals aignet state)
   (aignet-lits-ipasir-sat-check x-equiv
                                 invals regvals vals aignet state)))
 :rule-classes :congruence)

Theorem: aignet-lits-ipasir-sat-check-of-node-list-fix-aignet

(defthm aignet-lits-ipasir-sat-check-of-node-list-fix-aignet
 (equal
   (aignet-lits-ipasir-sat-check x invals
                                 regvals vals (node-list-fix aignet)
                                 state)
   (aignet-lits-ipasir-sat-check
        x invals regvals vals aignet state)))

Theorem: aignet-lits-ipasir-sat-check-node-list-equiv-congruence-on-aignet

(defthm
  aignet-lits-ipasir-sat-check-node-list-equiv-congruence-on-aignet
 (implies
  (node-list-equiv aignet aignet-equiv)
  (equal
   (aignet-lits-ipasir-sat-check x invals regvals vals aignet state)
   (aignet-lits-ipasir-sat-check x invals
                                 regvals vals aignet-equiv state)))
 :rule-classes :congruence)