• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
      • Aignet-copy-init
      • Aignet-simplify-with-tracking
      • Aignet-simplify-marked-with-tracking
      • Aignet-cnf
        • Aignet-lit->cnf
        • Aignet-ipasir
          • Aignet-vals-sat-care-masks-rec
          • Aignet-vals-sat-care-masks-lits
          • Aignet-lits-ipasir-sat-minimize
          • Aignet-lit-ipasir-sat-minimize
          • Aignet-lits-ipasir-sat-check
          • Aignet-get-ipasir-ctrex-regvals
          • Aignet-get-ipasir-ctrex-invals
          • Aignet-lit->ipasir
      • Aignet-simplify-marked
      • Aignet-complete-copy
      • Aignet-transforms
      • Aignet-eval
      • Semantics
      • Aignet-read-aiger
      • Aignet-write-aiger
      • Aignet-abc-interface
      • Utilities
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Aignet-ipasir

Aignet-lit-ipasir-sat-minimize

Check satisfiability of a literal, and minimize the satisfying assignment if satisfiable.

Signature

(aignet-lit-ipasir-sat-minimize 
     x invals 
     regvals inmasks regmasks aignet state) 
 
  → 
(mv status sat-invals sat-regvals 
    sat-inmasks sat-regmasks new-state) 

Arguments

x — Literal to check for satisfiability.
    Guard (litp 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.

inmasks — Bit array, overwritten with the input care set of the satisfying assignment.

regmasks — Bit array, overwritten with the register care set of the satisfying assignment.

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)).

sat-inmasks — If satisfiable, input care set of the satisfying assignment.
    Type (equal (len sat-inmasks) (num-ins aignet)).

sat-regmasks — If satisfiable, register care set of the satisfying assignment.
    Type (equal (len sat-regmasks) (num-regs aignet)).

new-state — Updated ACL2 state.

Definitions and Theorems

Function: aignet-lit-ipasir-sat-minimize

(defun aignet-lit-ipasir-sat-minimize
       (x invals
          regvals inmasks regmasks aignet state)
 (declare
     (xargs :stobjs (invals regvals inmasks regmasks aignet state)))
 (declare (xargs :guard (litp x)))
 (declare (xargs :guard (fanin-litp x aignet)))
 (let ((__function__ 'aignet-lit-ipasir-sat-minimize))
   (declare (ignorable __function__))
   (aignet-lits-ipasir-sat-minimize
        (list x)
        invals
        regvals inmasks regmasks aignet state)))

Theorem: return-type-of-aignet-lit-ipasir-sat-minimize.status

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

Theorem: return-type-of-aignet-lit-ipasir-sat-minimize.sat-invals

(defthm return-type-of-aignet-lit-ipasir-sat-minimize.sat-invals
  (b* (((mv ?status ?sat-invals ?sat-regvals
            ?sat-inmasks ?sat-regmasks ?new-state)
        (aignet-lit-ipasir-sat-minimize
             x invals
             regvals inmasks regmasks aignet state)))
    (equal (len sat-invals)
           (num-ins aignet)))
  :rule-classes :rewrite)

Theorem: return-type-of-aignet-lit-ipasir-sat-minimize.sat-regvals

(defthm return-type-of-aignet-lit-ipasir-sat-minimize.sat-regvals
  (b* (((mv ?status ?sat-invals ?sat-regvals
            ?sat-inmasks ?sat-regmasks ?new-state)
        (aignet-lit-ipasir-sat-minimize
             x invals
             regvals inmasks regmasks aignet state)))
    (equal (len sat-regvals)
           (num-regs aignet)))
  :rule-classes :rewrite)

Theorem: return-type-of-aignet-lit-ipasir-sat-minimize.sat-inmasks

(defthm return-type-of-aignet-lit-ipasir-sat-minimize.sat-inmasks
  (b* (((mv ?status ?sat-invals ?sat-regvals
            ?sat-inmasks ?sat-regmasks ?new-state)
        (aignet-lit-ipasir-sat-minimize
             x invals
             regvals inmasks regmasks aignet state)))
    (equal (len sat-inmasks)
           (num-ins aignet)))
  :rule-classes :rewrite)

Theorem: return-type-of-aignet-lit-ipasir-sat-minimize.sat-regmasks

(defthm return-type-of-aignet-lit-ipasir-sat-minimize.sat-regmasks
  (b* (((mv ?status ?sat-invals ?sat-regvals
            ?sat-inmasks ?sat-regmasks ?new-state)
        (aignet-lit-ipasir-sat-minimize
             x invals
             regvals inmasks regmasks aignet state)))
    (equal (len sat-regmasks)
           (num-regs aignet)))
  :rule-classes :rewrite)

Theorem: satisfying-assign-of-aignet-lit-ipasir-sat-minimize

(defthm satisfying-assign-of-aignet-lit-ipasir-sat-minimize
 (b* (((mv ?status ?sat-invals ?sat-regvals
           ?sat-inmasks ?sat-regmasks ?new-state)
       (aignet-lit-ipasir-sat-minimize
            x invals
            regvals inmasks regmasks aignet state)))
  (implies
    (and (equal status :sat)
         (aignet-litp x aignet)
         (vals-equiv-under-masks sat-inmasks sat-invals invals1)
         (vals-equiv-under-masks sat-regmasks sat-regvals regvals1))
    (equal (lit-eval x invals1 regvals1 aignet)
           1))))

Theorem: satisfying-assign-of-aignet-lit-ipasir-sat-minimize-basic

(defthm satisfying-assign-of-aignet-lit-ipasir-sat-minimize-basic
  (b* (((mv ?status ?sat-invals ?sat-regvals
            ?sat-inmasks ?sat-regmasks ?new-state)
        (aignet-lit-ipasir-sat-minimize
             x invals
             regvals inmasks regmasks aignet state)))
    (implies (and (equal status :sat)
                  (aignet-litp x aignet))
             (equal (lit-eval x sat-invals sat-regvals aignet)
                    1))))

Theorem: aignet-lit-ipasir-sat-minimize-not-unsat-when-sat

(defthm aignet-lit-ipasir-sat-minimize-not-unsat-when-sat
 (b* (((mv ?status ?sat-invals ?sat-regvals
           ?sat-inmasks ?sat-regmasks ?new-state)
       (aignet-lit-ipasir-sat-minimize
            x invals
            regvals inmasks regmasks aignet state)))
   (implies (and (equal (lit-eval x some-invals some-regvals aignet)
                        1)
                 (aignet-litp x aignet))
            (not (equal status :unsat)))))

Theorem: w-state-of-aignet-lit-ipasir-sat-minimize

(defthm w-state-of-aignet-lit-ipasir-sat-minimize
  (b* (((mv ?status ?sat-invals ?sat-regvals
            ?sat-inmasks ?sat-regmasks ?new-state)
        (aignet-lit-ipasir-sat-minimize
             x invals
             regvals inmasks regmasks aignet state)))
    (equal (w new-state) (w state))))

Theorem: aignet-lit-ipasir-sat-minimize-of-lit-fix-x

(defthm aignet-lit-ipasir-sat-minimize-of-lit-fix-x
  (equal (aignet-lit-ipasir-sat-minimize
              (lit-fix x)
              invals
              regvals inmasks regmasks aignet state)
         (aignet-lit-ipasir-sat-minimize
              x invals
              regvals inmasks regmasks aignet state)))

Theorem: aignet-lit-ipasir-sat-minimize-lit-equiv-congruence-on-x

(defthm aignet-lit-ipasir-sat-minimize-lit-equiv-congruence-on-x
  (implies (lit-equiv x x-equiv)
           (equal (aignet-lit-ipasir-sat-minimize
                       x invals
                       regvals inmasks regmasks aignet state)
                  (aignet-lit-ipasir-sat-minimize
                       x-equiv invals
                       regvals inmasks regmasks aignet state)))
  :rule-classes :congruence)

Theorem: aignet-lit-ipasir-sat-minimize-of-node-list-fix-aignet

(defthm aignet-lit-ipasir-sat-minimize-of-node-list-fix-aignet
  (equal (aignet-lit-ipasir-sat-minimize
              x invals regvals
              inmasks regmasks (node-list-fix aignet)
              state)
         (aignet-lit-ipasir-sat-minimize
              x invals
              regvals inmasks regmasks aignet state)))

Theorem: aignet-lit-ipasir-sat-minimize-node-list-equiv-congruence-on-aignet

(defthm
 aignet-lit-ipasir-sat-minimize-node-list-equiv-congruence-on-aignet
 (implies (node-list-equiv aignet aignet-equiv)
          (equal (aignet-lit-ipasir-sat-minimize
                      x invals
                      regvals inmasks regmasks aignet state)
                 (aignet-lit-ipasir-sat-minimize
                      x invals regvals
                      inmasks regmasks aignet-equiv state)))
 :rule-classes :congruence)