max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: the AIG framework to track negations in a more efficient way (#7381)

Browse source 
This PR refactors the AIG datastructures that underly bv_decide in order
to allow a better tracking of negations in the circuit. This refactor
has two effects, for one adding full constant folding to the AIG
framework and secondly enabling us to add further simplifications from
the Brummayer Biere paper in the future which was previously
architecturally impossible.
This commit is contained in:
Henrik Böving 2025-03-17 18:33:49 +01:00 • committed by GitHub
parent 5e0648fe98
commit 5a5e83c26c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
29 changed files with 359 additions and 484 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
View file

@ -111,10 +111,10 @@ builtin_simproc [bv_normalize] bv_udiv_of_two_pow (((_ : BitVec _) / (BitVec.ofN
}
builtin_simproc [bv_normalize] bv_equal_const_not (~~~(_ : BitVec _) == (BitVec.ofNat _ _)) := fun e => do
let_expr BEq.beq α inst outerLhs rhs := e | return .continue
let_expr BEq.beq _ _ outerLhs rhs := e | return .continue
let some ⟨w, rhsVal⟩ ← getBitVecValue? rhs | return .continue
let_expr Complement.complement _ _ lhs := outerLhs | return .continue
let expr := mkApp4 (mkConst ``BEq.beq [0]) α inst lhs (toExpr (~~~rhsVal))
let expr ← mkAppM ``BEq.beq #[lhs, toExpr (~~~rhsVal)]
let proof :=
mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm)
(toExpr w)
@ -123,10 +123,10 @@ builtin_simproc [bv_normalize] bv_equal_const_not (~~~(_ : BitVec _) == (BitVec.
return .visit { expr := expr, proof? := some proof }
builtin_simproc [bv_normalize] bv_equal_const_not' ((BitVec.ofNat _ _) == ~~~(_ : BitVec _)) := fun e => do
let_expr BEq.beq α inst lhs outerRhs := e | return .continue
let_expr BEq.beq _ _ lhs outerRhs := e | return .continue
let some ⟨w, lhsVal⟩ ← getBitVecValue? lhs | return .continue
let_expr Complement.complement _ _ rhs := outerRhs | return .continue
let expr := mkApp4 (mkConst ``BEq.beq [0]) α inst rhs (toExpr (~~~lhsVal))
let expr ← mkAppM ``BEq.beq #[rhs, toExpr (~~~lhsVal)]
let proof :=
mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm')
(toExpr w)
@ -135,12 +135,12 @@ builtin_simproc [bv_normalize] bv_equal_const_not' ((BitVec.ofNat _ _) == ~~~(_
return .visit { expr := expr, proof? := some proof }
builtin_simproc [bv_normalize] bv_and_eq_allOnes ((_ : BitVec _) &&& (_ : BitVec _) == (BitVec.ofNat _ _)) := fun e => do
let_expr BEq.beq α instBEq outerLhs rhs := e | return .continue
let_expr BEq.beq _ _ outerLhs rhs := e | return .continue
let some ⟨w, rhsVal⟩ ← getBitVecValue? rhs | return .continue
if -1#w != rhsVal then return .continue
let_expr HAnd.hAnd _ _ _ _ llhs lrhs := outerLhs | return .continue
let newLhs := mkApp4 (mkConst ``BEq.beq [0]) α instBEq llhs rhs
let newRhs := mkApp4 (mkConst ``BEq.beq [0]) α instBEq lrhs rhs
let newLhs ← mkAppM ``BEq.beq #[llhs, rhs]
let newRhs ← mkAppM ``BEq.beq #[lrhs, rhs]
let expr := mkApp2 (mkConst ``Bool.and) newLhs newRhs
let proof :=
mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.and_eq_allOnes)
@ -150,12 +150,12 @@ builtin_simproc [bv_normalize] bv_and_eq_allOnes ((_ : BitVec _) &&& (_ : BitVec
return .visit { expr := expr, proof? := some proof }
builtin_simproc [bv_normalize] bv_allOnes_eq_and ((BitVec.ofNat _ _) == (_ : BitVec _) &&& (_ : BitVec _)) := fun e => do
let_expr BEq.beq α instBEq lhs outerRhs := e | return .continue
let_expr BEq.beq _ _ lhs outerRhs := e | return .continue
let some ⟨w, lhsVal⟩ ← getBitVecValue? lhs | return .continue
if -1#w != lhsVal then return .continue
let_expr HAnd.hAnd _ _ _ _ rlhs rrhs := outerRhs | return .continue
let newLhs := mkApp4 (mkConst ``BEq.beq [0]) α instBEq rlhs lhs
let newRhs := mkApp4 (mkConst ``BEq.beq [0]) α instBEq rrhs lhs
let newLhs ← mkAppM ``BEq.beq #[rlhs, lhs]
let newRhs ← mkAppM ``BEq.beq #[rrhs, lhs]
let expr := mkApp2 (mkConst ``Bool.and) newLhs newRhs
let proof :=
mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.allOnes_eq_and)

103
src/Std/Sat/AIG/Basic.lean
View file

@ -224,21 +224,36 @@ instance : Membership α (AIG α) where
mem := Mem
/--
A reference to a node within an AIG. This is the `AIG` analog of `Bool`.
A reference to a node within an AIG.
-/
structure Ref (aig : AIG α) where
gate : Nat
invert : Bool
hgate : gate < aig.decls.size
/--
A `Ref` into `aig1` is also valid for `aig2` if `aig1` is smaller than `aig2`.
-/
@[inline]
def Ref.cast {aig1 aig2 : AIG α} (ref : Ref aig1)
(h : aig1.decls.size ≤ aig2.decls.size) :
def Ref.cast {aig1 aig2 : AIG α} (ref : Ref aig1) (h : aig1.decls.size ≤ aig2.decls.size) :
Ref aig2 :=
{ ref with hgate := by have := ref.hgate; omega }
/--
Flip the polarity of `Ref` if `inv` is set.
-/
@[inline]
def Ref.flip {aig : AIG α} (ref : Ref aig) (inv : Bool) : Ref aig :=
{ ref with invert := inv ^^ ref.invert }
/--
Flip the polarity of `Ref`.
-/
@[inline]
def Ref.not {aig : AIG α} (ref : Ref aig) : Ref aig :=
ref.flip true
/--
A pair of `Ref`s, useful for `LawfulOperator`s that act on two `Ref`s at a time.
-/
@ -255,6 +270,14 @@ def BinaryInput.cast {aig1 aig2 : AIG α} (input : BinaryInput aig1)
BinaryInput aig2 :=
{ input with lhs := input.lhs.cast h, rhs := input.rhs.cast h }
/--
Flip the current inverter settings of the `BinaryInput` if `linv` or `rinv` is set respectively.
-/
@[inline]
def BinaryInput.invert {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) :
BinaryInput aig :=
{ input with lhs := input.lhs.flip linv, rhs := input.rhs.flip rinv }
/--
A collection of 3 of `Ref`s, useful for `LawfulOperator`s that act on three `Ref`s at a time,
in particular multiplexer style functions.
@ -292,14 +315,14 @@ Transform an `Entrypoint` into a graphviz string. Useful for debugging purposes.
-/
def toGraphviz {α : Type} [DecidableEq α] [ToString α] [Hashable α] (entry : Entrypoint α) :
String :=
let ⟨⟨decls, _, hinv⟩, ⟨idx, h⟩⟩ := entry
let ⟨⟨decls, _, hinv⟩, ⟨idx, invert, h⟩⟩ := entry
let (dag, s) := go "" decls hinv idx h |>.run ∅
let nodes := s.fold (fun x y ↦ x ++ toGraphvizString decls y) ""
"Digraph AIG {" ++ nodes ++ dag ++ "}"
where
go {α : Type} [DecidableEq α] [ToString α] [Hashable α] (acc : String) (decls : Array (Decl α))
(hinv : IsDAG α decls) (idx : Nat) (hidx : idx < decls.size)
: StateM (HashSet (Fin decls.size)) String := do
(hinv : IsDAG α decls) (idx : Nat) (hidx : idx < decls.size) :
StateM (HashSet (Fin decls.size)) String := do
let fidx : Fin decls.size := Fin.mk idx hidx
if (← get).contains fidx then
return acc
@ -325,9 +348,9 @@ where
A vector of references into `aig`. This is the `AIG` analog of `BitVec`.
-/
structure RefVec (aig : AIG α) (w : Nat) where
refs : Array Nat
refs : Array (Nat × Bool)
hlen : refs.size = w
hrefs : ∀ (h : i < w), refs[i] < aig.decls.size
hrefs : ∀ (h : i < w), refs[i].1 < aig.decls.size
/--
A sequence of references bundled with their AIG.
@ -362,7 +385,7 @@ structure ExtendTarget (aig : AIG α) (newWidth : Nat) where
Evaluate an `AIG.Entrypoint` using some assignment for atoms.
-/
def denote (assign : α → Bool) (entry : Entrypoint α) : Bool :=
go entry.ref.gate entry.aig.decls assign entry.ref.hgate entry.aig.invariant
go entry.ref.gate entry.aig.decls assign entry.ref.hgate entry.aig.invariant ^^ entry.ref.invert
where
go (x : Nat) (decls : Array (Decl α)) (assign : α → Bool) (h1 : x < decls.size)
(h2 : IsDAG α decls) :
@ -400,61 +423,23 @@ def unexpandDenote : Lean.PrettyPrinter.Unexpander
/--
The denotation of the sub-DAG in the `aig` at node `start` is false for all assignments.
-/
def UnsatAt (aig : AIG α) (start : Nat) (h : start < aig.decls.size) : Prop :=
∀ assign, ⟦aig, ⟨start, h⟩, assign⟧ = false
def UnsatAt (aig : AIG α) (start : Nat) (invert : Bool) (h : start < aig.decls.size) : Prop :=
∀ assign, ⟦aig, ⟨start, invert, h⟩, assign⟧ = false
/--
The denotation of the `Entrypoint` is false for all assignments.
-/
def Entrypoint.Unsat (entry : Entrypoint α) : Prop :=
entry.aig.UnsatAt entry.ref.gate entry.ref.hgate
/--
An input to an AIG gate.
-/
structure Fanin (aig : AIG α) where
/--
The node we are referring to.
-/
ref : Ref aig
/--
Whether the node is inverted
-/
inv : Bool
/--
The `Ref.cast` equivalent for `Fanin`.
-/
@[inline]
def Fanin.cast {aig1 aig2 : AIG α} (fanin : Fanin aig1)
(h : aig1.decls.size ≤ aig2.decls.size) :
Fanin aig2 :=
{ fanin with ref := fanin.ref.cast h }
/--
The input type for creating AIG and gates.
-/
structure GateInput (aig : AIG α) where
lhs : Fanin aig
rhs : Fanin aig
/--
The `Ref.cast` equivalent for `GateInput`.
-/
@[inline]
def GateInput.cast {aig1 aig2 : AIG α} (input : GateInput aig1)
(h : aig1.decls.size ≤ aig2.decls.size) :
GateInput aig2 :=
{ input with lhs := input.lhs.cast h, rhs := input.rhs.cast h }
entry.aig.UnsatAt entry.ref.gate entry.ref.invert entry.ref.hgate
/--
Add a new and inverter gate to the AIG in `aig`. Note that this version is only meant for proving,
for production purposes use `AIG.mkGateCached` and equality theorems to this one.
-/
def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
def mkGate (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
let g := aig.decls.size
let decls :=
aig.decls.push <| .gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
aig.decls.push <| .gate input.lhs.gate input.rhs.gate input.lhs.invert input.rhs.invert
let cache := aig.cache.noUpdate
have invariant := by
intro i lhs' rhs' linv' rinv' h1 h2
@ -462,10 +447,10 @@ def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
split at h2
· apply aig.invariant <;> assumption
· injections
have := input.lhs.ref.hgate
have := input.rhs.ref.hgate
have := input.lhs.hgate
have := input.rhs.hgate
omega
⟨{ aig with decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩
⟨{ aig with decls, invariant, cache }, ⟨g, false, by simp [g, decls]⟩⟩
/--
Add a new input node to the AIG in `aig`. Note that this version is only meant for proving,
@ -481,7 +466,7 @@ def mkAtom (aig : AIG α) (n : α) : Entrypoint α :=
split at h2
· apply aig.invariant <;> assumption
· contradiction
⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩
⟨{ decls, invariant, cache }, ⟨g, false, by simp [g, decls]⟩⟩
/--
Add a new constant node to `aig`. Note that this version is only meant for proving,
@ -497,17 +482,17 @@ def mkConst (aig : AIG α) (val : Bool) : Entrypoint α :=
split at h2
· apply aig.invariant <;> assumption
· contradiction
⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩
⟨{ decls, invariant, cache }, ⟨g, false, by simp [g, decls]⟩⟩
/--
Determine whether `ref` is a `Decl.const` with value `b`.
-/
def isConstant (aig : AIG α) (ref : Ref aig) (b : Bool) : Bool :=
let ⟨gate, hgate⟩ := ref
let ⟨gate, invert, hgate⟩ := ref
let decl := aig.decls[gate]'hgate
match decl with
| .const val => b = val
| .const val => (invert ^^ b) = val
| _ => false
end AIG

41
src/Std/Sat/AIG/CNF.lean
View file

@ -121,7 +121,7 @@ Tseitin transformation. This is done by combining the atom assignment with an as
auxiliary variables, that just evaluates the AIG at the corresponding node.
-/
def cnfSatAssignment (aig : AIG Nat) (assign1 : Nat → Bool) : CNFVar aig → Bool :=
mixAssigns assign1 (fun idx => ⟦aig, ⟨idx.val, idx.isLt⟩, assign1⟧)
mixAssigns assign1 (fun idx => ⟦aig, ⟨idx.val, false, idx.isLt⟩, assign1⟧)
@[simp]
theorem satAssignment_inl : (cnfSatAssignment aig assign1) (.inl x) = assign1 x := by
@ -129,7 +129,7 @@ theorem satAssignment_inl : (cnfSatAssignment aig assign1) (.inl x) = assign1 x
@[simp]
theorem satAssignment_inr :
(cnfSatAssignment aig assign1) (.inr x) = ⟦aig, ⟨x.val, x.isLt⟩, assign1⟧ := by
(cnfSatAssignment aig assign1) (.inr x) = ⟦aig, ⟨x.val, false, x.isLt⟩, assign1⟧ := by
simp [cnfSatAssignment, mixAssigns]
/--
@ -156,7 +156,7 @@ structure Cache.Inv (cnf : CNF (CNFVar aig)) (marks : Array Bool) (hmarks : mark
-/
heval : ∀ (assign : CNFVar aig → Bool) (_heval : cnf.eval assign = true) (idx : Nat)
(hbound : idx < aig.decls.size) (_hmark : marks[idx]'(by omega) = true),
⟦aig, ⟨idx, hbound⟩, projectLeftAssign assign⟧ = (projectRightAssign assign) idx hbound
⟦aig, ⟨idx, false, hbound⟩, projectLeftAssign assign⟧ = (projectRightAssign assign) idx hbound
/--
@ -287,7 +287,7 @@ def Cache.addConst (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size
· next heq =>
simp only [heq, CNF.eval_append, Decl.constToCNF_eval, Bool.and_eq_true, beq_iff_eq]
at htip heval
simp only [denote_idx_const htip, projectRightAssign_property, heval]
simp [denote_idx_const htip, projectRightAssign_property, heval]
· next heq =>
simp only [CNF.eval_append, Decl.constToCNF_eval, Bool.and_eq_true, beq_iff_eq] at heval
have := cache.inv.heval assign heval.right idx hbound hmarked
@ -376,7 +376,7 @@ def Cache.addGate (cache : Cache aig cnf) {hlb} {hrb} (idx : Nat) (h : idx < aig
at htip heval
have hleval := cache.inv.heval assign heval.right lhs (by omega) hl
have hreval := cache.inv.heval assign heval.right rhs (by omega) hr
simp only [denote_idx_gate htip, hleval, projectRightAssign_property, hreval, heval]
cases linv <;> cases rinv <;> simp [denote_idx_gate htip, hleval, projectRightAssign_property, hreval, heval]
· next heq =>
simp only [CNF.eval_append, Decl.gateToCNF_eval, Bool.and_eq_true, beq_iff_eq] at heval
have := cache.inv.heval assign heval.right idx hbound hmarked
@ -439,7 +439,7 @@ theorem State.Inv_gateToCNF {aig : AIG Nat} {h}
rinv)
:= by
intro assign1
simp [CNF.sat_def, denote_idx_gate heq]
cases linv <;> cases rinv <;> simp [CNF.sat_def, denote_idx_gate heq]
/--
The state to accumulate CNF clauses as we run our Tseitin transformation on the AIG.
@ -566,10 +566,12 @@ theorem State.unsat_def (state : State aig) :
rfl
@[simp]
theorem State.eval_eq : State.eval assign state = state.cnf.eval assign := by simp [State.eval]
theorem State.eval_eq : State.eval assign state = state.cnf.eval assign := by
simp [State.eval]
@[simp]
theorem State.sat_iff : State.Sat assign state ↔ state.cnf.Sat assign := by simp [State.sat_def]
theorem State.sat_iff : State.Sat assign state ↔ state.cnf.Sat assign := by
simp [State.sat_def]
@[simp]
theorem State.unsat_iff : State.Unsat state ↔ state.cnf.Unsat := by simp [State.unsat_def]
@ -581,7 +583,7 @@ Convert an AIG into CNF, starting at some entry node.
-/
def toCNF (entry : Entrypoint Nat) : CNF Nat :=
let ⟨state, _⟩ := go entry.aig entry.ref.gate entry.ref.hgate (toCNF.State.empty entry.aig)
let cnf : CNF (CNFVar entry.aig) := [(.inr ⟨entry.ref.gate, entry.ref.hgate⟩, true)] :: state.cnf
let cnf : CNF (CNFVar entry.aig) := [(.inr ⟨entry.ref.gate, entry.ref.hgate⟩, !entry.ref.invert)] :: state.cnf
cnf.relabel inj
where
inj {aig : AIG Nat} (var : CNFVar aig) : Nat :=
@ -664,8 +666,8 @@ theorem toCNF.go_sat (aig : AIG Nat) (start : Nat) (h1 : start < aig.decls.size)
rw [State.sat_iff]
simp [this]
theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (h1) (assign1) :
⟦aig, ⟨start, h1⟩, assign1⟧ → (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1) := by
theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (inv) (h1) (assign1) :
⟦aig, ⟨start, inv, h1⟩, assign1⟧ → (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1) := by
have := go_sat aig start h1 assign1 (.empty aig)
simp only [State.Sat, CNF.sat_def] at this
simp [this]
@ -674,26 +676,25 @@ theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (h1) (assign1) :
Connect SAT results about the CNF to SAT results about the AIG.
-/
theorem toCNF.go_as_denote (aig : AIG Nat) (start) (h1) (assign1) :
((⟦aig, ⟨start, h1⟩, assign1⟧ && (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1)) = sat?)
((⟦aig, ⟨start, inv, h1⟩, assign1⟧ && (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1)) = sat?)
→
(⟦aig, ⟨start, h1⟩, assign1⟧ = sat?) := by
have := go_as_denote' aig start h1 assign1
(⟦aig, ⟨start, inv, h1⟩, assign1⟧ = sat?) := by
have := go_as_denote' aig start inv h1 assign1
by_cases CNF.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val.cnf <;> simp_all
/--
Connect SAT results about the AIG to SAT results about the CNF.
-/
theorem toCNF.denote_as_go {assign : AIG.CNFVar aig → Bool}:
(⟦aig, ⟨start, h1⟩, projectLeftAssign assign⟧ = false)
theorem toCNF.denote_as_go {assign : AIG.CNFVar aig → Bool} :
(⟦aig, ⟨start, inv, h1⟩, projectLeftAssign assign⟧ = false)
→
CNF.eval assign (([(.inr ⟨start, h1⟩, true)] :: (go aig start h1 (.empty aig)).val.cnf)) = false := by
CNF.eval assign (([(.inr ⟨start, h1⟩, !inv)] :: (go aig start h1 (.empty aig)).val.cnf)) = false := by
intro h
match heval1:(go aig start h1 (State.empty aig)).val.cnf.eval assign with
| true =>
have heval2 := (go aig start h1 (.empty aig)).val.cache.inv.heval
specialize heval2 assign heval1 start h1 go_marks
simp only [h, projectRightAssign_property, Bool.false_eq] at heval2
simp [heval2]
cases inv <;> simp_all
| false =>
simp [heval1]
@ -707,7 +708,7 @@ theorem toCNF_equisat (entry : Entrypoint Nat) : (toCNF entry).Unsat ↔ entry.U
· intro h assign1
apply toCNF.go_as_denote
specialize h (toCNF.cnfSatAssignment entry.aig assign1)
simpa using h
rcases entry with ⟨_, ⟨_, _ | _, _⟩⟩ <;> simpa using h
· intro h assign
apply toCNF.denote_as_go
specialize h (toCNF.projectLeftAssign assign)

42
src/Std/Sat/AIG/Cached.lean
View file

@ -29,7 +29,7 @@ def mkAtomCached (aig : AIG α) (n : α) : Entrypoint α :=
let decl := .atom n
match cache.get? decl with
| some hit =>
⟨⟨decls, cache, inv⟩ , hit.idx, hit.hbound⟩
⟨⟨decls, cache, inv⟩ , hit.idx, false, hit.hbound⟩
| none =>
let g := decls.size
let cache := cache.insert decls decl
@ -40,7 +40,7 @@ def mkAtomCached (aig : AIG α) (n : α) : Entrypoint α :=
split at h2
· apply inv <;> assumption
· contradiction
⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩
⟨⟨decls, cache, inv⟩, ⟨g, false, by simp [g, decls]⟩⟩
/--
A version of `AIG.mkConst` that uses the subterm cache in `AIG`. This version is meant for
@ -51,7 +51,7 @@ def mkConstCached (aig : AIG α) (val : Bool) : Entrypoint α :=
let decl := .const val
match cache.get? decl with
| some hit =>
⟨⟨decls, cache, inv⟩, hit.idx, hit.hbound⟩
⟨⟨decls, cache, inv⟩, hit.idx, false, hit.hbound⟩
| none =>
let g := decls.size
let cache := cache.insert decls decl
@ -62,7 +62,7 @@ def mkConstCached (aig : AIG α) (val : Bool) : Entrypoint α :=
split at h2
· apply inv <;> assumption
· contradiction
⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩
⟨⟨decls, cache, inv⟩, ⟨g, false, by simp [g, decls]⟩⟩
/--
A version of `AIG.mkGate` that uses the subterm cache in `AIG`. This version is meant for
@ -70,26 +70,26 @@ programming, for proving purposes use `AIG.mkGate` and equality theorems to this
Beyond caching this function also implements a subset of the optimizations presented in:
-/
def mkGateCached (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
let lhs := input.lhs.ref.gate
let rhs := input.rhs.ref.gate
def mkGateCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
let lhs := input.lhs.gate
let rhs := input.rhs.gate
if lhs < rhs then
go aig ⟨input.lhs, input.rhs⟩
else
go aig ⟨input.rhs, input.lhs⟩
where
go (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
go (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
let ⟨decls, cache, inv⟩ := aig
let lhs := input.lhs.ref.gate
let rhs := input.rhs.ref.gate
let linv := input.lhs.inv
let rinv := input.rhs.inv
have := input.lhs.ref.hgate
have := input.rhs.ref.hgate
let lhs := input.lhs.gate
let rhs := input.rhs.gate
let linv := input.lhs.invert
let rinv := input.rhs.invert
have := input.lhs.hgate
have := input.rhs.hgate
let decl := .gate lhs rhs linv rinv
match cache.get? decl with
| some hit =>
⟨⟨decls, cache, inv⟩, ⟨hit.idx, hit.hbound⟩⟩
⟨⟨decls, cache, inv⟩, ⟨hit.idx, false, hit.hbound⟩⟩
| none =>
/-
Here we implement the constant propagating subset of:
@ -102,15 +102,15 @@ where
| _, .const true, _, true | _, .const false, _, false =>
mkConstCached ⟨decls, cache, inv⟩ false
-- Left Neutrality
| .const true, _, false, false | .const false, _, true, false =>
⟨⟨decls, cache, inv⟩, rhs, (by assumption)⟩
| .const true, _, false, _ | .const false, _, true, _ =>
⟨⟨decls, cache, inv⟩, rhs, rinv, by assumption⟩
-- Right Neutrality
| _, .const true, false, false | _, .const false, false, true =>
⟨⟨decls, cache, inv⟩, lhs, (by assumption)⟩
| _, .const true, _, false | _, .const false, _, true =>
⟨⟨decls, cache, inv⟩, lhs, linv, by assumption⟩
| _, _, _, _ =>
if lhs == rhs && linv == false && rinv == false then
-- Idempotency rule
⟨⟨decls, cache, inv⟩, lhs, (by assumption)⟩
⟨⟨decls, cache, inv⟩, lhs, false, by assumption⟩
else if lhs == rhs && linv == !rinv then
-- Contradiction rule
mkConstCached ⟨decls, cache, inv⟩ false
@ -125,7 +125,7 @@ where
split at h2
· apply inv <;> assumption
· injections; omega
⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩
⟨⟨decls, cache, inv⟩, ⟨g, false, by simp [g, decls]⟩⟩
end AIG

125
src/Std/Sat/AIG/CachedGates.lean
View file

@ -22,94 +22,43 @@ variable {α : Type} [Hashable α] [DecidableEq α]
/--
Create a not gate in the input AIG. This uses the builtin cache to enable automated subterm sharing.
-/
def mkNotCached (aig : AIG α) (gate : Ref aig) : Entrypoint α :=
-- ¬x = true && invert x
let res := aig.mkConstCached true
let aig := res.aig
let constRef := res.ref
aig.mkGateCached {
lhs := {
ref := constRef
inv := false
}
rhs := {
ref := gate.cast <| by
intros
apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
omega
inv := true
}
}
@[inline]
def BinaryInput.asGateInput {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) :
GateInput aig :=
{ lhs := { ref := input.lhs, inv := linv }, rhs := { ref := input.rhs, inv := rinv } }
def mkNotCached (aig : AIG α) (gate : Ref aig) : Entrypoint α :=
⟨aig, gate.not⟩
/--
Create an and gate in the input AIG. This uses the builtin cache to enable automated subterm
sharing.
-/
@[inline]
def mkAndCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
aig.mkGateCached <| input.asGateInput false false
aig.mkGateCached input
/--
Create an or gate in the input AIG. This uses the builtin cache to enable automated subterm sharing.
-/
def mkOrCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
-- x or y = true && (invert (invert x && invert y))
let res := aig.mkGateCached <| input.asGateInput true true
-- x or y = invert (invert x && invert y)
let res := aig.mkGateCached <| input.invert true true
let aig := res.aig
let auxRef := res.ref
let res := aig.mkConstCached true
let aig := res.aig
let constRef := res.ref
aig.mkGateCached {
lhs := {
ref := constRef
inv := false
},
rhs := {
ref := auxRef.cast <| by
intros
simp +zetaDelta only
apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
omega
inv := true
}
}
⟨aig, auxRef.not⟩
/--
Create an xor gate in the input AIG. This uses the builtin cache to enable automated subterm
sharing.
-/
def mkXorCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
-- x xor y = (invert (invert (x && y))) && (invert ((invert x) && (invert y)))
let res := aig.mkGateCached <| input.asGateInput false false
-- x xor y = (invert (x && y)) && (invert ((invert x) && (invert y)))
let res := aig.mkGateCached input
let aig := res.aig
let aux1Ref := res.ref
let rinput :=
(input.asGateInput true true).cast
(by
intros
apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached)
omega)
let res := aig.mkGateCached rinput
let input := input.cast <| by apply LawfulOperator.le_size (f := mkGateCached)
let res := aig.mkGateCached (input.invert true true)
let aig := res.aig
let aux2Ref := res.ref
aig.mkGateCached {
lhs := {
ref := aux1Ref.cast <| by
simp +zetaDelta only
apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached)
omega
inv := true
},
rhs := {
ref := aux2Ref
inv := true
}
}
let aux1Ref := aux1Ref.cast <| by apply LawfulOperator.le_size (f := mkGateCached)
aig.mkGateCached ⟨aux1Ref.not, aux2Ref.not⟩
/--
Create an equality gate in the input AIG. This uses the builtin cache to enable automated subterm
@ -117,58 +66,26 @@ sharing.
-/
def mkBEqCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
-- a == b = (invert (a && (invert b))) && (invert ((invert a) && b))
let res := aig.mkGateCached <| input.asGateInput false true
let res := aig.mkGateCached <| input.invert false true
let aig := res.aig
let aux1Ref := res.ref
let rinput :=
(input.asGateInput true false).cast
(by
intros
apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached)
omega)
let res := aig.mkGateCached rinput
let input := input.cast <| by apply LawfulOperator.le_size (f := mkGateCached)
let res := aig.mkGateCached (input.invert true false)
let aig := res.aig
let aux2Ref := res.ref
aig.mkGateCached {
lhs := {
ref := aux1Ref.cast <| by
simp +zetaDelta only
apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached)
omega
inv := true
},
rhs := {
ref := aux2Ref
inv := true
}
}
let aux1Ref := aux1Ref.cast <| by apply LawfulOperator.le_size (f := mkGateCached)
aig.mkGateCached ⟨aux1Ref.not, aux2Ref.not⟩
/--
Create an implication gate in the input AIG. This uses the builtin cache to enable automated subterm
sharing.
-/
def mkImpCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
-- a -> b = true && (invert (a and (invert b)))
let res := aig.mkGateCached <| input.asGateInput false true
-- a -> b = (invert (a and (invert b)))
let res := aig.mkGateCached <| input.invert false true
let aig := res.aig
let auxRef := res.ref
let res := aig.mkConstCached true
let aig := res.aig
let constRef := res.ref
aig.mkGateCached {
lhs := {
ref := constRef
inv := false
},
rhs := {
ref := auxRef.cast <| by
intros
simp +zetaDelta only
apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
omega
inv := true
}
}
⟨aig, auxRef.not⟩
end AIG

88
src/Std/Sat/AIG/CachedGatesLemmas.lean
View file

@ -18,12 +18,6 @@ namespace Sat
namespace AIG
/--
Encoding of not as boolean expression in AIG form.
-/
private theorem not_as_aig : ∀ (b : Bool), (true && !b) = !b := by
decide
/--
Encoding of or as boolean expression in AIG form.
-/
@ -50,27 +44,13 @@ private theorem imp_as_aig : ∀ (a b : Bool), (!(a && !b)) = (!a || b) := by
variable {α : Type} [Hashable α] [DecidableEq α]
@[simp]
theorem BinaryInput_asGateInput_lhs {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) :
(input.asGateInput linv rinv).lhs = ⟨input.lhs, linv⟩ := rfl
@[simp]
theorem BinaryInput_asGateInput_rhs {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) :
(input.asGateInput linv rinv).rhs = ⟨input.rhs, rinv⟩ := rfl
theorem mkNotCached_le_size (aig : AIG α) (gate : Ref aig) :
aig.decls.size ≤ (aig.mkNotCached gate).aig.decls.size := by
simp only [mkNotCached]
apply LawfulOperator.le_size_of_le_aig_size
apply mkConstCached_le_size
simp [mkNotCached]
theorem mkNotCached_decl_eq idx (aig : AIG α) (gate : Ref aig) {h : idx < aig.decls.size} {h2} :
(aig.mkNotCached gate).aig.decls[idx]'h2 = aig.decls[idx] := by
simp only [mkNotCached]
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
assumption
(aig.mkNotCached gate).aig.decls[idx]'h2 = aig.decls[idx]'h := by
simp [mkNotCached]
instance : LawfulOperator α Ref mkNotCached where
le_size := mkNotCached_le_size
@ -80,10 +60,7 @@ instance : LawfulOperator α Ref mkNotCached where
@[simp]
theorem denote_mkNotCached {aig : AIG α} {gate : Ref aig} :
⟦aig.mkNotCached gate, assign⟧
=
!⟦aig, ⟨gate.gate, gate.hgate⟩, assign⟧ := by
rw [← not_as_aig]
⟦aig.mkNotCached gate, assign⟧ = !⟦aig, gate, assign⟧ := by
simp [mkNotCached, LawfulOperator.denote_mem_prefix (f := mkConstCached) gate.hgate]
theorem mkAndCached_le_size (aig : AIG α) (input : BinaryInput aig) :
@ -104,33 +81,19 @@ instance : LawfulOperator α BinaryInput mkAndCached where
@[simp]
theorem denote_mkAndCached {aig : AIG α} {input : BinaryInput aig} :
⟦aig.mkAndCached input, assign⟧
=
(⟦aig, input.lhs, assign⟧
&&
⟦aig, input.rhs, assign⟧) := by
⟦aig.mkAndCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧) := by
simp [mkAndCached]
theorem mkOrCached_le_size (aig : AIG α) (input : BinaryInput aig) :
aig.decls.size ≤ (aig.mkOrCached input).aig.decls.size := by
simp only [mkOrCached]
apply LawfulOperator.le_size_of_le_aig_size
apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
apply LawfulOperator.le_size_of_le_aig_size
omega
apply LawfulOperator.le_size
theorem mkOrCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size}
{h2} :
(aig.mkOrCached input).aig.decls[idx]'h2 = aig.decls[idx] := by
simp only [mkOrCached]
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
· rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
apply LawfulOperator.lt_size_of_lt_aig_size
assumption
· apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
apply LawfulOperator.lt_size_of_lt_aig_size
assumption
instance : LawfulOperator α BinaryInput mkOrCached where
le_size := mkOrCached_le_size
@ -138,11 +101,7 @@ instance : LawfulOperator α BinaryInput mkOrCached where
@[simp]
theorem denote_mkOrCached {aig : AIG α} {input : BinaryInput aig} :
⟦aig.mkOrCached input, assign⟧
=
(⟦aig, input.lhs, assign⟧
||
⟦aig, input.rhs, assign⟧) := by
⟦aig.mkOrCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ || ⟦aig, input.rhs, assign⟧) := by
rw [← or_as_aig]
simp [mkOrCached, LawfulOperator.denote_input_entry (f := mkConstCached)]
@ -174,12 +133,7 @@ instance : LawfulOperator α BinaryInput mkXorCached where
@[simp]
theorem denote_mkXorCached {aig : AIG α} {input : BinaryInput aig} :
⟦aig.mkXorCached input, assign⟧
=
xor
⟦aig, input.lhs, assign⟧
⟦aig, input.rhs, assign⟧
:= by
⟦aig.mkXorCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ ^^ ⟦aig, input.rhs, assign⟧) := by
rw [← xor_as_aig]
simp [
mkXorCached,
@ -214,11 +168,7 @@ instance : LawfulOperator α BinaryInput mkBEqCached where
@[simp]
theorem denote_mkBEqCached {aig : AIG α} {input : BinaryInput aig} :
⟦aig.mkBEqCached input, assign⟧
=
(⟦aig, input.lhs, assign⟧
==
⟦aig, input.rhs, assign⟧) := by
⟦aig.mkBEqCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ == ⟦aig, input.rhs, assign⟧) := by
rw [← beq_as_aig]
simp [
mkBEqCached,
@ -229,23 +179,13 @@ theorem denote_mkBEqCached {aig : AIG α} {input : BinaryInput aig} :
theorem mkImpCached_le_size (aig : AIG α) (input : BinaryInput aig) :
aig.decls.size ≤ (aig.mkImpCached input).aig.decls.size := by
simp only [mkImpCached]
apply LawfulOperator.le_size_of_le_aig_size
apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
apply LawfulOperator.le_size_of_le_aig_size
omega
apply LawfulOperator.le_size
theorem mkImpCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size}
{h2} :
(aig.mkImpCached input).aig.decls[idx]'h2 = aig.decls[idx] := by
simp only [mkImpCached]
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
· rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
apply LawfulOperator.lt_size_of_lt_aig_size
assumption
· apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
apply LawfulOperator.lt_size_of_lt_aig_size
assumption
instance : LawfulOperator α BinaryInput mkImpCached where
le_size := mkImpCached_le_size
@ -253,13 +193,7 @@ instance : LawfulOperator α BinaryInput mkImpCached where
@[simp]
theorem denote_mkImpCached {aig : AIG α} {input : BinaryInput aig} :
⟦aig.mkImpCached input, assign⟧
=
(
!⟦aig, ⟨input.lhs.gate, input.lhs.hgate⟩, assign⟧
||
⟦aig, ⟨input.rhs.gate, input.rhs.hgate⟩, assign⟧
) := by
⟦aig.mkImpCached input, assign⟧ = ( !⟦aig, input.lhs, assign⟧ || ⟦aig, input.rhs, assign⟧) := by
rw [← imp_as_aig]
simp [mkImpCached, LawfulOperator.denote_input_entry (f := mkConstCached)]

47
src/Std/Sat/AIG/CachedLemmas.lean
View file

@ -25,7 +25,7 @@ If we find a cached atom declaration in the AIG, denoting it is equivalent to de
theorem denote_mkAtom_cached {aig : AIG α} {hit} :
aig.cache.get? (.atom v) = some hit
→
⟦aig, ⟨hit.idx, hit.hbound⟩, assign⟧ = ⟦aig.mkAtom v, assign⟧ := by
⟦aig, ⟨hit.idx, false, hit.hbound⟩, assign⟧ = ⟦aig.mkAtom v, assign⟧ := by
have := hit.hvalid
simp only [denote_mkAtom]
unfold denote denote.go
@ -98,7 +98,7 @@ If we find a cached const declaration in the AIG, denoting it is equivalent to d
theorem denote_mkConst_cached {aig : AIG α} {hit} :
aig.cache.get? (.const b) = some hit
→
⟦aig, ⟨hit.idx, hit.hbound⟩, assign⟧ = ⟦aig.mkConst b, assign⟧ := by
⟦aig, ⟨hit.idx, false, hit.hbound⟩, assign⟧ = ⟦aig.mkConst b, assign⟧ := by
have := hit.hvalid
simp only [denote_mkConst]
unfold denote denote.go
@ -171,9 +171,9 @@ theorem mkConstCached_eval_eq_mkConst_eval {aig : AIG α} :
If we find a cached gate declaration in the AIG, denoting it is equivalent to denoting `AIG.mkGate`.
-/
theorem denote_mkGate_cached {aig : AIG α} {input} {hit} :
aig.cache.get? (.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
aig.cache.get? (.gate input.lhs.gate input.rhs.gate input.lhs.invert input.rhs.invert) = some hit
→
⟦⟨aig, hit.idx, hit.hbound⟩, assign⟧
⟦⟨aig, hit.idx, false, hit.hbound⟩, assign⟧
=
⟦aig.mkGate input, assign⟧ := by
intros
@ -184,27 +184,29 @@ theorem denote_mkGate_cached {aig : AIG α} {input} {hit} :
unfold denote denote.go
split <;> simp_all[denote]
theorem mkGateCached.go_le_size (aig : AIG α) (input : GateInput aig) :
theorem mkGateCached.go_le_size (aig : AIG α) (input : BinaryInput aig) :
aig.decls.size ≤ (go aig input).aig.decls.size := by
dsimp only [go]
split
· simp
· split <;> try simp +arith [mkConstCached_le_size]
· split <;> try simp [mkConstCached_le_size]
split
· simp +arith
· split <;> simp +arith [mkConstCached_le_size]
· simp
· split
· simp [mkConstCached_le_size]
· simp
/--
`AIG.mkGateCached` never shrinks the underlying AIG.
-/
theorem mkGateCached_le_size (aig : AIG α) (input : GateInput aig)
theorem mkGateCached_le_size (aig : AIG α) (input : BinaryInput aig)
: aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size := by
dsimp only [mkGateCached]
split
· apply mkGateCached.go_le_size
· apply mkGateCached.go_le_size
theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) :
theorem mkGateCached.go_decl_eq (aig : AIG α) (input : BinaryInput aig) :
∀ (idx : Nat) (h1) (h2), (go aig input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
generalize hres : go aig input = res
unfold go at hres
@ -256,7 +258,7 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) :
The AIG produced by `AIG.mkGateCached` agrees with the input AIG on all indices that are valid for
both.
-/
theorem mkGateCached_decl_eq (aig : AIG α) (input : GateInput aig) :
theorem mkGateCached_decl_eq (aig : AIG α) (input : BinaryInput aig) :
∀ (idx : Nat) (h1) (h2), (aig.mkGateCached input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
generalize hres : mkGateCached aig input = res
unfold mkGateCached at hres
@ -267,13 +269,13 @@ theorem mkGateCached_decl_eq (aig : AIG α) (input : GateInput aig) :
intros
rw [mkGateCached.go_decl_eq]
instance : LawfulOperator α GateInput mkGateCached where
instance : LawfulOperator α BinaryInput mkGateCached where
le_size := mkGateCached_le_size
decl_eq := by
intros
apply mkGateCached_decl_eq
theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput aig} :
theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : BinaryInput aig} :
⟦go aig input, assign⟧ = ⟦aig.mkGate input, assign⟧ := by
simp only [go]
split
@ -289,28 +291,27 @@ theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput ai
· next heq _ _ _ =>
simp_all [denote_idx_const heq]
· next heq _ _ _ =>
rcases input with ⟨_, ⟨rhs, rinv, hrgate⟩⟩
simp_all [denote_idx_const heq]
· next heq _ _ _ =>
rcases input with ⟨_, ⟨rhs, rinv, hrgate⟩⟩
simp_all [denote_idx_const heq]
· next heq _ _ _ _ =>
· next heq _ _ _ _ _ =>
rcases input with ⟨⟨lhs, linv, hlgate⟩, _⟩
simp_all [denote_idx_const heq]
· next heq _ _ _ =>
· next heq _ _ _ _ _ =>
rcases input with ⟨⟨lhs, linv, hlgate⟩, _⟩
simp_all [denote_idx_const heq]
· split
· rcases input with ⟨⟨lhs, linv, hlgate⟩, ⟨rhs, rinv, hrgate⟩⟩
split
· next hif =>
simp only [beq_false, Bool.and_eq_true, beq_iff_eq, Bool.not_eq_true'] at hif
rcases hif with ⟨⟨hifeq, hlinv⟩, hrinv⟩
replace hifeq : input.lhs.ref = input.rhs.ref := by
rcases input with ⟨⟨⟨_, _⟩, _⟩, ⟨⟨_, _⟩, _⟩⟩
simpa using hifeq
simp [hlinv, hrinv, hifeq]
· split
· next hif =>
simp only [Bool.and_eq_true, beq_iff_eq] at hif
rcases hif with ⟨hifeq, hinv⟩
replace hifeq : input.lhs.ref = input.rhs.ref := by
rcases input with ⟨⟨⟨_, _⟩, _⟩, ⟨⟨_, _⟩, _⟩⟩
simpa using hifeq
simp [hifeq, hinv]
· simp [mkGate, denote]
@ -318,7 +319,7 @@ theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput ai
The central equality theorem between `mkGateCached` and `mkGate`.
-/
@[simp]
theorem mkGateCached_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput aig} :
theorem mkGateCached_eval_eq_mkGate_eval {aig : AIG α} {input : BinaryInput aig} :
⟦aig.mkGateCached input, assign⟧ = ⟦aig.mkGate input, assign⟧ := by
simp only [mkGateCached]
split

6
src/Std/Sat/AIG/If.lean
View file

@ -221,12 +221,12 @@ theorem go_denote_mem_prefix {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr
(discr : Ref aig) (lhs rhs : RefVec aig w) (s : RefVec aig curr) (start : Nat) (hstart) :
⟦
(go aig curr hcurr discr lhs rhs s).aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply go_decl_eq

18
src/Std/Sat/AIG/LawfulOperator.lean
View file

@ -30,6 +30,13 @@ structure IsPrefix (decls1 decls2 : Array (Decl α)) : Prop where
-/
idx_eq : ∀ idx (h : idx < decls1.size), decls2[idx]'(by omega) = decls1[idx]'h
@[simp]
theorem IsPrefix_push {decls : Array (Decl α)} : IsPrefix decls (decls.push decl) := by
apply IsPrefix.of
· intro idx hidx
simp [hidx, Array.getElem_push]
· simp
/--
If `decls1` is a prefix of `decls2` and we start evaluating `decls2` at an
index in bounds of `decls1` we can evaluate at `decls1`.
@ -69,11 +76,12 @@ variable {α : Type} [Hashable α] [DecidableEq α]
@[inherit_doc denote.go_eq_of_isPrefix]
theorem denote.eq_of_isPrefix (entry : Entrypoint α) (newAIG : AIG α)
(hprefix : IsPrefix entry.aig.decls newAIG.decls) :
⟦newAIG, ⟨entry.ref.gate, (by have := entry.ref.hgate; have := hprefix.size_le; omega)⟩, assign⟧
⟦newAIG, ⟨entry.ref.gate, entry.ref.invert, (by have := entry.ref.hgate; have := hprefix.size_le; omega)⟩, assign⟧
=
⟦entry, assign⟧
:= by
unfold denote
rw [Bool.bne_left_inj]
apply denote.go_eq_of_isPrefix
assumption
@ -129,7 +137,7 @@ theorem le_size_of_le_aig_size (aig : AIG α) (input : β aig) (h : x ≤ aig.de
@[simp]
theorem denote_input_entry (entry : Entrypoint α) {input} {h} :
⟦(f entry.aig input).aig, ⟨entry.ref.gate, h⟩, assign⟧
⟦(f entry.aig input).aig, ⟨entry.ref.gate, entry.ref.invert, h⟩, assign⟧
=
⟦entry, assign⟧ := by
apply denote.eq_of_isPrefix
@ -143,10 +151,10 @@ theorem denote_cast_entry (entry : Entrypoint α) {input} {h} :
simp [Ref.cast]
theorem denote_mem_prefix {aig : AIG α} {input} (h) :
⟦(f aig input).aig, ⟨start, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧
⟦(f aig input).aig, ⟨start, invert, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧
=
⟦aig, ⟨start, h⟩, assign⟧ := by
rw [denote_input_entry ⟨aig, start, h⟩]
⟦aig, ⟨start, invert, h⟩, assign⟧ := by
rw [denote_input_entry ⟨aig, start, invert, h⟩]
end LawfulOperator

8
src/Std/Sat/AIG/LawfulVecOperator.lean
View file

@ -54,7 +54,7 @@ theorem le_size_of_le_aig_size (aig : AIG α) (input : β aig len) (h : x ≤ ai
@[simp]
theorem denote_input_entry (entry : Entrypoint α) {input : β entry.aig len} {h} :
⟦(f entry.aig input).aig, ⟨entry.ref.gate, h⟩, assign ⟧
⟦(f entry.aig input).aig, ⟨entry.ref.gate, entry.ref.invert, h⟩, assign ⟧
=
⟦entry, assign⟧ := by
apply denote.eq_of_isPrefix
@ -68,10 +68,10 @@ theorem denote_cast_entry (entry : Entrypoint α) {input : β entry.aig len} {h}
simp [Ref.cast]
theorem denote_mem_prefix {aig : AIG α} {input : β aig len} (h) :
⟦(f aig input).aig, ⟨start, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧
⟦(f aig input).aig, ⟨start, inv, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧
=
⟦aig, ⟨start, h⟩, assign⟧ := by
rw [denote_input_entry ⟨aig, start, h⟩]
⟦aig, ⟨start, inv, h⟩, assign⟧ := by
rw [denote_input_entry ⟨aig, start, inv, h⟩]
@[simp]
theorem denote_input_vec (s : RefVecEntry α len) {input : β s.aig len} {hcast} :

125
src/Std/Sat/AIG/Lemmas.lean
View file

@ -27,25 +27,15 @@ theorem Ref.gate_cast {aig1 aig2 : AIG α} (ref : Ref aig1)
@[simp]
theorem Ref.cast_eq {aig1 aig2 : AIG α} (ref : Ref aig1)
(h : aig1.decls.size ≤ aig2.decls.size) :
(ref.cast h) = ⟨ref.gate, by have := ref.hgate; omega⟩ := rfl
(ref.cast h) = ⟨ref.gate, ref.invert, by have := ref.hgate; omega⟩ := rfl
@[simp]
theorem Fanin.ref_cast {aig1 aig2 : AIG α} (fanin : Fanin aig1)
(h : aig1.decls.size ≤ aig2.decls.size) :
(fanin.cast h).ref = fanin.ref.cast h := rfl
@[simp]
theorem Fanin.inv_cast {aig1 aig2 : AIG α} (fanin : Fanin aig1)
(h : aig1.decls.size ≤ aig2.decls.size) :
(fanin.cast h).inv = fanin.inv := rfl
@[simp]
theorem GateInput.lhs_cast {aig1 aig2 : AIG α} (input : GateInput aig1)
theorem BinaryInput.lhs_cast {aig1 aig2 : AIG α} (input : BinaryInput aig1)
(h : aig1.decls.size ≤ aig2.decls.size) :
(input.cast h).lhs = input.lhs.cast h := rfl
@[simp]
theorem GateInput.rhs_cast {aig1 aig2 : AIG α} (input : GateInput aig1)
theorem BinaryInput.rhs_cast {aig1 aig2 : AIG α} (input : BinaryInput aig1)
(h : aig1.decls.size ≤ aig2.decls.size) :
(input.cast h).rhs = input.rhs.cast h := rfl
@ -55,6 +45,16 @@ theorem BinaryInput.each_cast {aig1 aig2 : AIG α} (lhs rhs : Ref aig1)
BinaryInput.mk (lhs.cast h1) (rhs.cast h2) = (BinaryInput.mk lhs rhs).cast h2 := by
simp [BinaryInput.cast]
@[simp]
theorem BinaryInput_invert_lhs {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) :
(input.invert linv rinv).lhs = ⟨input.lhs.gate, linv ^^ input.lhs.invert, input.lhs.hgate⟩ := by
simp [BinaryInput.invert, Ref.flip]
@[simp]
theorem BinaryInput_invert_rhs {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) :
(input.invert linv rinv).rhs = ⟨input.rhs.gate, rinv ^^ input.rhs.invert, input.rhs.hgate⟩ := by
simp [BinaryInput.invert, Ref.flip]
@[simp]
theorem denote_projected_entry {entry : Entrypoint α} :
⟦entry.aig, entry.ref, assign⟧ = ⟦entry, assign⟧ := by
@ -62,20 +62,43 @@ theorem denote_projected_entry {entry : Entrypoint α} :
@[simp]
theorem denote_projected_entry' {entry : Entrypoint α} :
⟦entry.aig, ⟨entry.ref.gate, entry.ref.hgate⟩, assign⟧ = ⟦entry, assign⟧ := by
⟦entry.aig, ⟨entry.ref.gate, entry.ref.invert, entry.ref.hgate⟩, assign⟧ = ⟦entry, assign⟧ := by
cases entry; simp
@[simp]
theorem Ref.denote_flip {aig : AIG α} {ref : Ref aig} {inv : Bool} :
⟦aig, ref.flip inv, assign⟧ = (⟦aig, ref, assign⟧ ^^ inv) := by
unfold denote
cases ref <;> cases inv <;> simp [Ref.flip]
@[simp]
theorem Ref.denote_not {aig : AIG α} {ref : Ref aig} :
⟦aig, ref.not, assign⟧ = !⟦aig, ref, assign⟧ := by
simp [Ref.not]
@[simp]
theorem denote_not_invert {aig : AIG α} {gate} {inv} {hgate} :
⟦aig, ⟨gate, !inv, hgate⟩, assign⟧ = !⟦aig, ⟨gate, inv, hgate⟩, assign⟧ := by
unfold denote
simp
@[simp]
theorem denote_invert_true {aig : AIG α} {gate} {hgate} :
⟦aig, ⟨gate, true, hgate⟩, assign⟧ = !⟦aig, ⟨gate, false, hgate⟩, assign⟧ := by
unfold denote
simp
/--
`AIG.mkGate` never shrinks the underlying AIG.
-/
theorem mkGate_le_size (aig : AIG α) (input : GateInput aig) :
theorem mkGate_le_size (aig : AIG α) (input : BinaryInput aig) :
aig.decls.size ≤ (aig.mkGate input).aig.decls.size := by
simp +arith [mkGate]
simp [mkGate]
/--
The AIG produced by `AIG.mkGate` agrees with the input AIG on all indices that are valid for both.
-/
theorem mkGate_decl_eq idx (aig : AIG α) (input : GateInput aig) {h : idx < aig.decls.size} :
theorem mkGate_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size} :
have := mkGate_le_size aig input
(aig.mkGate input).aig.decls[idx]'(by omega) = aig.decls[idx] := by
simp only [mkGate, Array.getElem_push]
@ -83,17 +106,17 @@ theorem mkGate_decl_eq idx (aig : AIG α) (input : GateInput aig) {h : idx < aig
· rfl
· contradiction
instance : LawfulOperator α GateInput mkGate where
instance : LawfulOperator α BinaryInput mkGate where
le_size := mkGate_le_size
decl_eq := by
intros
apply mkGate_decl_eq
@[simp]
theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
theorem denote_mkGate {aig : AIG α} {input : BinaryInput aig} :
⟦aig.mkGate input, assign⟧
=
((⟦aig, input.lhs.ref, assign⟧ ^^ input.lhs.inv) && (⟦aig, input.rhs.ref, assign⟧ ^^ input.rhs.inv)) := by
(⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧) := by
conv =>
lhs
unfold denote denote.go
@ -107,18 +130,12 @@ theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
· next heq =>
rw [mkGate, Array.getElem_push_eq] at heq
injection heq with heq1 heq2 heq3 heq4
dsimp only
simp only [← heq1, mkGate, ← heq3, ← heq2, ← heq4, Bool.bne_false, denote]
congr 2
· unfold denote
simp only [heq1]
apply denote.go_eq_of_isPrefix
apply LawfulOperator.isPrefix_aig
· simp [heq3]
· unfold denote
simp only [heq2]
apply denote.go_eq_of_isPrefix
apply LawfulOperator.isPrefix_aig
· simp [heq4]
· apply denote.go_eq_of_isPrefix
simp
· apply denote.go_eq_of_isPrefix
simp
/--
`AIG.mkAtom` never shrinks the underlying AIG.
@ -154,7 +171,7 @@ theorem denote_mkAtom {aig : AIG α} :
· next heq =>
rw [mkAtom, Array.getElem_push_eq] at heq
injection heq with heq
rw [heq]
simp [heq, mkAtom]
· next heq =>
rw [mkAtom, Array.getElem_push_eq] at heq
contradiction
@ -190,7 +207,7 @@ theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val :=
· next heq =>
rw [mkConst, Array.getElem_push_eq] at heq
injection heq with heq
rw [heq]
simp [heq, mkConst]
· next heq =>
rw [mkConst, Array.getElem_push_eq] at heq
contradiction
@ -202,7 +219,7 @@ theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val :=
If an index contains a `Decl.const` we know how to denote it.
-/
theorem denote_idx_const {aig : AIG α} {hstart} (h : aig.decls[start]'hstart = .const b) :
⟦aig, ⟨start, hstart⟩, assign⟧ = b := by
⟦aig, ⟨start, invert, hstart⟩, assign⟧ = (b ^^ invert) := by
unfold denote denote.go
split <;> simp_all
@ -210,7 +227,7 @@ theorem denote_idx_const {aig : AIG α} {hstart} (h : aig.decls[start]'hstart =
If an index contains a `Decl.atom` we know how to denote it.
-/
theorem denote_idx_atom {aig : AIG α} {hstart} (h : aig.decls[start] = .atom a) :
⟦aig, ⟨start, hstart⟩, assign⟧ = assign a := by
⟦aig, ⟨start, invert, hstart⟩, assign⟧ = (assign a ^^ invert) := by
unfold denote denote.go
split <;> simp_all
@ -218,13 +235,13 @@ theorem denote_idx_atom {aig : AIG α} {hstart} (h : aig.decls[start] = .atom a)
If an index contains a `Decl.gate` we know how to denote it.
-/
theorem denote_idx_gate {aig : AIG α} {hstart} (h : aig.decls[start] = .gate lhs rhs linv rinv) :
⟦aig, ⟨start, hstart⟩, assign⟧
⟦aig, ⟨start, invert, hstart⟩, assign⟧
=
(
(⟦aig, ⟨lhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ linv)
((
(⟦aig, ⟨lhs, linv, by have := aig.invariant hstart h; omega⟩, assign⟧)
&&
(⟦aig, ⟨rhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ rinv)
) := by
(⟦aig, ⟨rhs, rinv, by have := aig.invariant hstart h; omega⟩, assign⟧)
) ^^ invert) := by
unfold denote
conv =>
lhs
@ -247,15 +264,15 @@ theorem idx_trichotomy (aig : AIG α) (hstart : start < aig.decls.size) {prop :
| .gate lhs rhs linv rinv => apply hgate; assumption
theorem denote_idx_trichotomy {aig : AIG α} {hstart : start < aig.decls.size}
(hconst : ∀ b, aig.decls[start]'hstart = .const b → ⟦aig, ⟨start, hstart⟩, assign⟧ = res)
(hatom : ∀ a, aig.decls[start]'hstart = .atom a → ⟦aig, ⟨start, hstart⟩, assign⟧ = res)
(hconst : ∀ b, aig.decls[start]'hstart = .const b → ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = res)
(hatom : ∀ a, aig.decls[start]'hstart = .atom a → ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = res)
(hgate :
∀ lhs rhs linv rinv,
aig.decls[start]'hstart = .gate lhs rhs linv rinv
→
⟦aig, ⟨start, hstart⟩, assign⟧ = res
⟦aig, ⟨start, invert, hstart⟩, assign⟧ = res
) :
⟦aig, ⟨start, hstart⟩, assign⟧ = res := by
⟦aig, ⟨start, invert, hstart⟩, assign⟧ = res := by
apply idx_trichotomy aig hstart
· exact hconst
· exact hatom
@ -264,32 +281,32 @@ theorem denote_idx_trichotomy {aig : AIG α} {hstart : start < aig.decls.size}
theorem mem_def {aig : AIG α} {a : α} : (a ∈ aig) ↔ ((.atom a) ∈ aig.decls) := by
simp [Membership.mem, Mem]
theorem denote_congr (assign1 assign2 : α → Bool) (aig : AIG α) (idx : Nat)
theorem denote_congr (assign1 assign2 : α → Bool) (aig : AIG α) (idx : Nat) (invert : Bool)
(hidx : idx < aig.decls.size) (h : ∀ a, a ∈ aig → assign1 a = assign2 a) :
⟦aig, ⟨idx, hidx⟩, assign1⟧ = ⟦aig, ⟨idx, hidx⟩, assign2⟧ := by
⟦aig, ⟨idx, invert, hidx⟩, assign1⟧ = ⟦aig, ⟨idx, invert, hidx⟩, assign2⟧ := by
apply denote_idx_trichotomy
· intro b heq
simp [denote_idx_const heq]
· intro a heq
simp only [denote_idx_atom heq]
simp only [denote_idx_atom heq, Bool.bne_left_inj]
apply h
rw [mem_def, ← heq, Array.mem_def]
apply Array.getElem_mem_toList
simp [mem_def, ← heq]
· intro lhs rhs linv rinv heq
simp only [denote_idx_gate heq]
have := aig.invariant hidx heq
rw [denote_congr assign1 assign2 aig lhs (by omega) h]
rw [denote_congr assign1 assign2 aig rhs (by omega) h]
rw [denote_congr assign1 assign2 aig lhs _ (by omega) h]
rw [denote_congr assign1 assign2 aig rhs _ (by omega) h]
theorem of_isConstant {aig : AIG α} {assign : α → Bool} {ref : Ref aig} {b : Bool} :
aig.isConstant ref b → ⟦aig, ref, assign⟧ = b := by
rcases ref with ⟨gate, hgate⟩
rcases ref with ⟨gate, invert, hgate⟩
intro h
unfold isConstant at h
dsimp only at h
split at h
· rw [denote_idx_const]
simp_all
· next heq =>
rw [denote_idx_const (h := heq)]
cases invert <;> simp_all
· contradiction
end AIG

20
src/Std/Sat/AIG/RefVec.lean
View file

@ -33,8 +33,8 @@ theorem emptyWithCapacity_eq : emptyWithCapacity (aig := aig) c = empty := by
@[inline]
def cast' {aig1 aig2 : AIG α} (s : RefVec aig1 len)
(h :
(∀ {i : Nat} (h : i < len), s.refs[i]'(by have := s.hlen; omega) < aig1.decls.size)
→ ∀ {i : Nat} (h : i < len), s.refs[i]'(by have := s.hlen; omega) < aig2.decls.size) :
(∀ {i : Nat} (h : i < len), (s.refs[i]'(by have := s.hlen; omega)).1 < aig1.decls.size)
→ ∀ {i : Nat} (h : i < len), (s.refs[i]'(by have := s.hlen; omega)).1 < aig2.decls.size) :
RefVec aig2 len :=
{ s with
hrefs := by
@ -58,13 +58,13 @@ def cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (h : aig1.decls.size ≤ aig
def get (s : RefVec aig len) (idx : Nat) (hidx : idx < len) : Ref aig :=
let ⟨refs, hlen, hrefs⟩ := s
let ref := refs[idx]'(by rw [hlen]; assumption)
⟨ref, by apply hrefs; assumption⟩
⟨ref.1, ref.2, by apply hrefs; assumption⟩
@[inline]
def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) :=
let ⟨refs, hlen, hrefs⟩ := s
⟨
refs.push ref.gate,
refs.push (ref.gate, ref.invert),
by simp [hlen],
by
intro i hi
@ -75,6 +75,11 @@ def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) :=
· apply AIG.Ref.hgate
⟩
@[simp]
theorem cast_cast {aig1 aig2 aig3 : AIG α} (s : RefVec aig1 len)
(h1 : aig1.decls.size ≤ aig2.decls.size) (h2 : aig2.decls.size ≤ aig3.decls.size) :
(s.cast h1).cast h2 = s.cast (Nat.le_trans h1 h2) := by rfl
@[simp]
theorem get_push_ref_eq (s : RefVec aig len) (ref : AIG.Ref aig) :
(s.push ref).get len (by omega) = ref := by
@ -95,6 +100,8 @@ theorem get_push_ref_lt (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat)
cases ref
simp only [Ref.mk.injEq]
rw [Array.getElem_push_lt]
· simp
· simp [hlen, hidx]
@[simp]
theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx : idx < len)
@ -135,6 +142,9 @@ theorem get_append (lhs : RefVec aig lw) (rhs : RefVec aig rw) (idx : Nat)
split
· simp [Ref.mk.injEq]
rw [Array.getElem_append_left]
· simp
· rw [lhs.hlen]
assumption
· simp only [Ref.mk.injEq]
rw [Array.getElem_append_right]
· simp [lhs.hlen]
@ -162,7 +172,7 @@ theorem get_out_bound (s : RefVec aig len) (idx : Nat) (alt : Ref aig) (hidx : l
def countKnown [Inhabited α] (aig : AIG α) (s : RefVec aig len) : Nat := Id.run do
let folder acc ref :=
let decl := aig.decls[ref]!
let decl := aig.decls[ref.1]!
match decl with
| .const .. => acc + 1
| _ => acc

10
src/Std/Sat/AIG/RefVecOperator/Map.lean
View file

@ -36,7 +36,7 @@ theorem denote_prefix_cast_ref {aig : AIG α} {input1 input2 : Ref aig}
instance : LawfulMapOperator α mkNotCached where
chainable := by
intros
simp only [Ref.gate_cast, denote_mkNotCached]
simp only [Ref.cast_eq, denote_mkNotCached, Bool.not_eq_eq_eq_not, Bool.not_not]
rw [LawfulOperator.denote_mem_prefix (f := mkNotCached)]
end LawfulMapOperator
@ -156,7 +156,7 @@ theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVe
simp only [Nat.le_refl, get, Ref.cast_eq, Ref.mk.injEq, true_implies]
have : curr = len := by omega
subst this
rfl
simp
termination_by len - curr
theorem go_get {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr)
@ -175,12 +175,12 @@ theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len)
(start : Nat) (hstart) :
⟦
(go aig curr hcurr s input f).aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply go_decl_eq

6
src/Std/Sat/AIG/RefVecOperator/Zip.lean
View file

@ -202,12 +202,12 @@ theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len)
[chainable : LawfulZipOperator α f] (start : Nat) (hstart) :
⟦
(go aig curr s hcurr lhs rhs f).aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply go_decl_eq

8
src/Std/Sat/AIG/Relabel.lean
View file

@ -98,9 +98,9 @@ theorem relabel_gate {aig : AIG α} {r : α → β} {hidx : idx < (relabel r aig
@[simp]
theorem denote_relabel (aig : AIG α) (r : α → β) (start : Nat) {hidx}
(assign : β → Bool) :
⟦aig.relabel r, ⟨start, hidx⟩, assign⟧
⟦aig.relabel r, ⟨start, invert, hidx⟩, assign⟧
=
⟦aig, ⟨start, by rw [← relabel_size_eq_size (r := r)]; omega⟩, (assign ∘ r)⟧ := by
⟦aig, ⟨start, invert, by rw [← relabel_size_eq_size (r := r)]; omega⟩, (assign ∘ r)⟧ := by
apply denote_idx_trichotomy
· intro b heq1
have heq2 := relabel_const heq1
@ -121,14 +121,14 @@ theorem denote_relabel (aig : AIG α) (r : α → β) (start : Nat) {hidx}
rw [denote_relabel aig r rhs assign]
theorem unsat_relabel {aig : AIG α} (r : α → β) {hidx} :
aig.UnsatAt idx hidx → (aig.relabel r).UnsatAt idx (by simp [hidx]) := by
aig.UnsatAt idx invert hidx → (aig.relabel r).UnsatAt idx invert (by simp [hidx]) := by
intro h assign
specialize h (assign ∘ r)
simp [h]
theorem relabel_unsat_iff [Nonempty α] {aig : AIG α} {r : α → β} {hidx1} {hidx2}
(hinj : ∀ x y, x ∈ aig → y ∈ aig → r x = r y → x = y) :
(aig.relabel r).UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2 := by
(aig.relabel r).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
constructor
· intro h assign
let g : β → α := fun b =>

2
src/Std/Sat/AIG/RelabelNat.lean
View file

@ -329,7 +329,7 @@ theorem relabelNat_size_eq_size {aig : AIG α} : aig.relabelNat.decls.size = aig
`relabelNat` preserves unsatisfiablility.
-/
theorem relabelNat_unsat_iff [Nonempty α] {aig : AIG α} {hidx1} {hidx2} :
(aig.relabelNat).UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2 := by
(aig.relabelNat).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
dsimp only [relabelNat, relabelNat']
rw [relabel_unsat_iff]
intro x y hx hy heq

2
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
View file

@ -197,6 +197,8 @@ theorem go_le_size (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.R
dsimp only
split
· refine Nat.le_trans ?_ (by apply go_le_size)
unfold mkFullAdder
dsimp only
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkFullAdderCarry)
apply AIG.LawfulOperator.le_size (f := mkFullAdderOut)
· simp

6
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
View file

@ -64,12 +64,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (idx : Nat) (hidx)
(s : AIG.RefVec aig idx) (c : BitVec w) (start : Nat) (hstart) :
⟦
(go aig c idx s hidx).aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply go_decl_eq

6
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
View file

@ -42,12 +42,12 @@ theorem go_denote_mem_prefix (aig : AIG BVBit) (expr : BVExpr w) (assign : Assig
(hstart) :
⟦
(go aig expr).val.aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply (go aig expr).property⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply (go aig expr).property⟩,
assign.toAIGAssignment
⟧
=
⟦aig, ⟨start, hstart⟩, assign.toAIGAssignment⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign.toAIGAssignment⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply go_decl_eq

10
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
View file

@ -63,11 +63,11 @@ theorem mkFullAdder_denote_mem_prefix (aig : AIG α) (input : FullAdderInput aig
(hstart) :
⟦
(mkFullAdder aig input).aig,
⟨start, Nat.lt_of_lt_of_le hstart (FullAdderOutput.hle _)⟩,
⟨start, inv, Nat.lt_of_lt_of_le hstart (FullAdderOutput.hle _)⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
unfold mkFullAdder
dsimp only
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
@ -77,12 +77,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (c
(s : AIG.RefVec aig curr) (lhs rhs : AIG.RefVec aig w) (start : Nat) (hstart) :
⟦
(go aig lhs rhs curr hcurr cin s).aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply go_decl_eq

5
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean
View file

@ -39,9 +39,8 @@ theorem denote_blastNeg (aig : AIG α) (value : BitVec w) (target : RefVec aig w
rw [denote_blastAdd]
· intro idx hidx
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_true,
Bool.true_and]
rw [denote_blastNot, htarget]
· simp only [RefVec.get_cast, Ref.cast_eq, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_not]
rw [denote_blastNot, htarget, BitVec.getLsbD_eq_getElem]
· simp [Ref.hgate]
· simp

6
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
View file

@ -69,12 +69,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (distance : Nat) (input : AIG.RefVec
(curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) (start : Nat) (hstart) :
⟦
(go aig input distance curr hcurr s).aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply go_decl_eq

6
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
View file

@ -69,12 +69,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (distance : Nat) (input : AIG.RefVec
(curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) (start : Nat) (hstart) :
⟦
(go aig input distance curr hcurr s).aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply go_decl_eq

100
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
View file

@ -61,12 +61,12 @@ theorem blastDivSubtractShift_denote_mem_prefix (aig : AIG α) (falseRef trueRef
(n d q r : AIG.RefVec aig w) (wn wr : Nat) (start : Nat) (hstart) :
⟦
(blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply blastDivSubtractShift_le_size⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply blastDivSubtractShift_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply blastDivSubtractShift_decl_eq
@ -95,58 +95,60 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh
unfold blastDivSubtractShift BitVec.divSubtractShift
dsimp only
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite)]
. simp only [RefVec.get_cast, Ref.gate_cast]
. simp only [Ref.cast_eq, RefVec.cast_cast, RefVec.get_cast]
rw [AIG.RefVec.denote_ite]
rw [BVPred.mkUlt_denote_eq (lhs := rbv.shiftConcat (lhs.getLsbD (wn - 1))) (rhs := rhs)]
· split
· next hdiscr =>
rw [← Normalize.BitVec.lt_ult] at hdiscr
simp only [Ref.cast_eq, id_eq, Int.reduceNeg, RefVec.get_cast, hdiscr, ↓reduceIte]
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
conv =>
rhs
rw [apply_ite (f := BitVec.DivModState.q)]
rw [apply_ite (f := (BitVec.getLsbD · idx))]
apply ite_congr
· rw [BVPred.mkUlt_denote_eq (assign := assign) (lhs := rbv.shiftConcat (lhs.getLsbD (wn - 1))) (rhs := rhs)]
· simp [Std.Tactic.BVDecide.Normalize.BitVec.lt_ult]
· intro idx hidx
simp only [RefVec.get_cast, Ref.cast_eq]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [denote_blastShiftConcat_eq_shiftConcat]
· intro idx hidx
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [hq]
· simp [Ref.hgate]
· rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [hr]
· rw [BVPred.denote_getD_eq_getLsbD]
· simp [hleft]
· simp [hfalse]
· simp [Ref.hgate]
· next hdiscr =>
rw [← Normalize.BitVec.lt_ult] at hdiscr
simp only [Ref.cast_eq, id_eq, Int.reduceNeg, RefVec.get_cast, hdiscr, ↓reduceIte]
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
· intro idx hidx
simp only [RefVec.get_cast, Ref.cast_eq]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
rw [denote_blastShiftConcat_eq_shiftConcat]
· intro idx hidx
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [hq]
· simp [Ref.hgate]
· rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [htrue]
· simp [Ref.hgate]
· intro idx hidx
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [hright]
· simp [Ref.hgate]
· intro h
simp only [RefVec.get_cast, Ref.cast_eq]
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
. simp only [Ref.cast_eq, id_eq, Int.reduceNeg, RefVec.get_cast]
rw [denote_blastShiftConcat_eq_shiftConcat]
. simp [hr]
. dsimp only
rw [BVPred.denote_getD_eq_getLsbD]
· exact hleft
· exact hfalse
. simp [Ref.hgate]
· intro idx hidx
rw [denote_blastShiftConcat_eq_shiftConcat]
· intro idx hidx
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [hq]
· simp [Ref.hgate]
· rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [hfalse]
· simp [Ref.hgate]
· intro h
simp only [RefVec.get_cast, Ref.cast_eq]
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
. simp [hright]
. simp [Ref.hgate]
rw [denote_blastShiftConcat_eq_shiftConcat]
· intro idx hidx
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [hq]
· simp [Ref.hgate]
· rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [htrue]
· simp [Ref.hgate]
. simp [Ref.hgate]
theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
@ -378,12 +380,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG
(n d q r : AIG.RefVec aig w) (wn wr : Nat) (start : Nat) (hstart) :
⟦
(go aig curr falseRef trueRef n d wn wr q r).aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply go_decl_eq

9
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
View file

@ -26,7 +26,7 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe
(assign : α → Bool)
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
⟦(mkUlt aig input).aig, (mkUlt aig input).ref, assign⟧ = BitVec.ult lhs rhs := by
⟦mkUlt aig input, assign⟧ = BitVec.ult lhs rhs := by
rw [BitVec.ult_eq_not_carry]
unfold mkUlt
simp only [denote_projected_entry, denote_mkNotCached, denote_projected_entry']
@ -42,11 +42,8 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe
· dsimp only
intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_true,
Bool.true_and]
rw [BVExpr.bitblast.denote_blastNot]
congr 1
apply hright
· simp only [RefVec.get_cast, Ref.cast_eq, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_not]
rw [BVExpr.bitblast.denote_blastNot, hright, BitVec.getLsbD_eq_getElem]
· simp [Ref.hgate]
end BVPred

6
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
View file

@ -69,12 +69,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w)
(hcurr : curr ≤ newWidth) (s : AIG.RefVec aig curr) (start : Nat) (hstart) :
⟦
(go aig w input newWidth curr hcurr s).aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply go_decl_eq

6
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
View file

@ -62,12 +62,12 @@ theorem go_denote_mem_prefix (aig : AIG BVBit) (idx : Nat) (hidx) (s : AIG.RefVe
(a : Nat) (start : Nat) (hstart) :
⟦
(go aig w a idx s hidx).aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply go_decl_eq

10
src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
View file

@ -141,17 +141,19 @@ theorem go_isPrefix_aig {aig : AIG β} :
theorem go_denote_mem_prefix :
⟦
(go aig expr atomHandler).val.aig,
⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply go_isPrefix_aig
@[simp]
theorem go_denote_entry (entry : Entrypoint β) {h} :
⟦(go entry.aig expr atomHandler).val.aig, ⟨entry.ref.gate, h⟩, assign⟧ = ⟦entry, assign⟧ := by
⟦(go entry.aig expr atomHandler).val.aig, ⟨entry.ref.gate, entry.ref.invert, h⟩, assign⟧
=
⟦entry, assign⟧ := by
apply denote.eq_of_isPrefix
apply ofBoolExprCached.go_isPrefix_aig

2
tests/lean/run/bv_counterexample.lean
View file

@ -12,7 +12,7 @@ example (x : BitVec 64) : x < x + 1 := by
/--
error: The prover found a counterexample, consider the following assignment:
x = 511#64
x = 0#64
-/
#guard_msgs in
example (x : BitVec 64) (h : x < 512) : x ^^^ x ≠ 0 := by