perf: bv_decide don't drop the expression level cache (#7636)
This PR makes sure that the expression level cache in bv_decide is maintained across the entire bitblaster instead of just locally per BitVec expression. The PR was split off from the first one (#7606) as this mostly entails pulling the invariant through and is thus much more mechanical.
This commit is contained in:
Henrik Böving
GitHub
parent
e663eb1b7a
commit
f241cc832b
12 changed files with 500 additions and 345 deletions
|
|
@ -4,23 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Henrik Böving
|
||||
-/
|
||||
prelude
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
|
||||
import Std.Tactic.BVDecide.Bitblast.BoolExpr.Circuit
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
|
||||
|
||||
/-!
|
||||
This module contains the implementation of a bitblaster for general `BitVec` problems with boolean
|
||||
substructure (`BVLogicalExpr`). It is the main entrypoint into the bitblasting framework.
|
||||
-/
|
||||
|
||||
namespace Std.Tactic.BVDecide
|
||||
|
||||
open Std.Sat
|
||||
|
||||
namespace BVLogicalExpr
|
||||
|
||||
def bitblast (expr : BVLogicalExpr) : AIG.Entrypoint BVBit :=
|
||||
ofBoolExprCached expr BVPred.bitblast
|
||||
|
||||
end BVLogicalExpr
|
||||
|
||||
end Std.Tactic.BVDecide
|
||||
|
|
|
|||
|
|
@ -93,13 +93,18 @@ def Cache.cast (cache : Cache aig1) (h : aig1.decls.size ≤ aig2.decls.size) :
|
|||
· exact h
|
||||
⟨map, this⟩
|
||||
|
||||
structure WithCache (α : Type u) (aig : AIG BVBit) where
|
||||
val : α
|
||||
cache : Cache aig
|
||||
|
||||
structure Return (aig : AIG BVBit) (w : Nat) where
|
||||
result : AIG.ExtendingRefVecEntry aig w
|
||||
cache : Cache result.val.aig
|
||||
|
||||
set_option maxHeartbeats 400000 in
|
||||
def bitblast (aig : AIG BVBit) (expr : BVExpr w) : AIG.RefVecEntry BVBit w :=
|
||||
goCache aig expr .empty |>.result.val
|
||||
def bitblast (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) : Return aig w :=
|
||||
let ⟨expr, cache⟩ := input
|
||||
goCache aig expr cache
|
||||
where
|
||||
goCache {w : Nat} (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : Return aig w :=
|
||||
match cache.get? expr with
|
||||
|
|
@ -370,15 +375,22 @@ end
|
|||
|
||||
end bitblast
|
||||
|
||||
instance : AIG.LawfulVecOperator BVBit (fun _ w => BVExpr w) bitblast where
|
||||
le_size := by
|
||||
intro _ aig expr
|
||||
unfold bitblast
|
||||
exact (bitblast.goCache aig expr _).result.property
|
||||
decl_eq := by
|
||||
intros
|
||||
unfold bitblast
|
||||
apply bitblast.goCache_decl_eq
|
||||
theorem bitblast_decl_eq (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) :
|
||||
∀ (idx : Nat) (h1) (h2), (bitblast aig input).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
|
||||
intros
|
||||
unfold bitblast
|
||||
apply bitblast.goCache_decl_eq
|
||||
|
||||
theorem bitblast_le_size (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) :
|
||||
aig.decls.size ≤ (bitblast aig input).result.val.aig.decls.size := by
|
||||
exact (bitblast aig input).result.property
|
||||
|
||||
theorem bitblast_lt_size_of_lt_aig_size (aig : AIG BVBit) (input : WithCache (BVExpr w) aig)
|
||||
(h : x < aig.decls.size) :
|
||||
x < (bitblast aig input).result.val.aig.decls.size := by
|
||||
apply Nat.lt_of_lt_of_le
|
||||
· exact h
|
||||
· exact bitblast_le_size aig input
|
||||
|
||||
end BVExpr
|
||||
|
||||
|
|
|
|||
|
|
@ -18,81 +18,89 @@ namespace Std.Tactic.BVDecide
|
|||
|
||||
open Std.Sat
|
||||
|
||||
structure Return (aig : AIG BVBit) where
|
||||
result : AIG.ExtendingEntrypoint aig
|
||||
cache : BVExpr.Cache result.val.aig
|
||||
|
||||
namespace BVPred
|
||||
|
||||
def bitblast (aig : AIG BVBit) (pred : BVPred) : AIG.Entrypoint BVBit :=
|
||||
def bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : Return aig :=
|
||||
let ⟨pred, cache⟩ := input
|
||||
match pred with
|
||||
| .bin lhs op rhs =>
|
||||
let res := lhs.bitblast aig
|
||||
let aig := res.aig
|
||||
let lhsRefs := res.vec
|
||||
let res := rhs.bitblast aig
|
||||
let aig := res.aig
|
||||
let rhsRefs := res.vec
|
||||
let lhsRefs := lhsRefs.cast <| AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast) ..
|
||||
let ⟨⟨⟨aig, lhsRefs⟩, hlhs⟩, cache⟩ := BVExpr.bitblast aig ⟨lhs, cache⟩
|
||||
let ⟨⟨⟨aig, rhsRefs⟩, hrhs⟩, cache⟩ := BVExpr.bitblast aig ⟨rhs, cache⟩
|
||||
let lhsRefs := lhsRefs.cast hrhs
|
||||
match op with
|
||||
| .eq => mkEq aig ⟨lhsRefs, rhsRefs⟩
|
||||
| .ult => mkUlt aig ⟨lhsRefs, rhsRefs⟩
|
||||
| .eq =>
|
||||
let res := mkEq aig ⟨lhsRefs, rhsRefs⟩
|
||||
let cache := cache.cast (AIG.LawfulOperator.le_size (f := mkEq) ..)
|
||||
have := by
|
||||
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkEq)
|
||||
dsimp only at hlhs hrhs
|
||||
omega
|
||||
⟨⟨res, this⟩, cache⟩
|
||||
| .ult =>
|
||||
let res := mkUlt aig ⟨lhsRefs, rhsRefs⟩
|
||||
have := AIG.LawfulOperator.le_size (f := mkUlt) ..
|
||||
let cache := cache.cast this
|
||||
have := by
|
||||
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
|
||||
dsimp only at hlhs hrhs
|
||||
omega
|
||||
⟨⟨res, this⟩, cache⟩
|
||||
| .getLsbD expr idx =>
|
||||
/-
|
||||
Note: This blasts the entire expression up to `w` despite only needing it up to `idx`.
|
||||
However the vast majority of operations are interested in all bits so the API is currently
|
||||
not designed to support this use case.
|
||||
-/
|
||||
let res := expr.bitblast aig
|
||||
let aig := res.aig
|
||||
let refs := res.vec
|
||||
blastGetLsbD aig ⟨refs, idx⟩
|
||||
|
||||
instance : AIG.LawfulOperator BVBit (fun _ => BVPred) bitblast where
|
||||
le_size := by
|
||||
intro aig pred
|
||||
unfold bitblast
|
||||
cases pred with
|
||||
| bin lhs op rhs =>
|
||||
cases op with
|
||||
| eq =>
|
||||
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkEq)
|
||||
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
|
||||
apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast)
|
||||
| ult =>
|
||||
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
|
||||
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
|
||||
apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast)
|
||||
| getLsbD expr idx =>
|
||||
let ⟨⟨⟨aig, refs⟩, hrefs⟩, cache⟩ := BVExpr.bitblast aig ⟨expr, cache⟩
|
||||
let res := blastGetLsbD aig ⟨refs, idx⟩
|
||||
let cache := cache.cast (AIG.LawfulOperator.le_size (f := blastGetLsbD) ..)
|
||||
have := by
|
||||
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsbD)
|
||||
apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast)
|
||||
decl_eq := by
|
||||
intro aig pred idx h1 h2
|
||||
cases pred with
|
||||
| bin lhs op rhs =>
|
||||
cases op with
|
||||
| eq =>
|
||||
simp only [bitblast]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkEq)]
|
||||
rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast)]
|
||||
rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast)]
|
||||
· apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
|
||||
assumption
|
||||
· apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
|
||||
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
|
||||
assumption
|
||||
| ult =>
|
||||
simp only [bitblast]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkUlt)]
|
||||
rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast)]
|
||||
rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast)]
|
||||
· apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
|
||||
assumption
|
||||
· apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
|
||||
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
|
||||
assumption
|
||||
| getLsbD expr idx =>
|
||||
exact hrefs
|
||||
⟨⟨res, this⟩, cache⟩
|
||||
|
||||
theorem bitblast_decl_eq (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) :
|
||||
∀ (idx : Nat) (h1) (h2), (bitblast aig input).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
|
||||
intro idx h1 h2
|
||||
rcases input with ⟨pred, cache⟩
|
||||
unfold BVPred.bitblast
|
||||
cases pred with
|
||||
| bin lhs op rhs =>
|
||||
cases op with
|
||||
| eq =>
|
||||
dsimp only
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkEq)]
|
||||
rw [BVExpr.bitblast_decl_eq]
|
||||
rw [BVExpr.bitblast_decl_eq]
|
||||
· apply BVExpr.bitblast_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
· apply BVExpr.bitblast_lt_size_of_lt_aig_size
|
||||
apply BVExpr.bitblast_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
| ult =>
|
||||
simp only [bitblast]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := blastGetLsbD)]
|
||||
rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast)]
|
||||
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
|
||||
assumption
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkUlt)]
|
||||
rw [BVExpr.bitblast_decl_eq]
|
||||
rw [BVExpr.bitblast_decl_eq]
|
||||
· apply BVExpr.bitblast_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
· apply BVExpr.bitblast_lt_size_of_lt_aig_size
|
||||
apply BVExpr.bitblast_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
| getLsbD expr idx =>
|
||||
simp only [bitblast]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := blastGetLsbD)]
|
||||
rw [BVExpr.bitblast_decl_eq]
|
||||
apply BVExpr.bitblast_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
|
||||
theorem bitblast_le_size (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) :
|
||||
aig.decls.size ≤ (bitblast aig input).result.val.aig.decls.size := by
|
||||
exact (bitblast aig input).result.property
|
||||
|
||||
end BVPred
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,203 @@
|
|||
/-
|
||||
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Henrik Böving
|
||||
-/
|
||||
prelude
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
|
||||
|
||||
/-!
|
||||
This module contains the logic to turn a `BVLogicalExpr` into an `AIG` with maximum subterm sharing,
|
||||
through the use of a cache that re-uses sub-circuits if possible. Additionally a term level cache
|
||||
is used to prevent rerunning bitblasting on commong bitvector subexpressions.
|
||||
-/
|
||||
|
||||
namespace Std.Tactic.BVDecide
|
||||
|
||||
open Std.Sat Std.Sat.AIG
|
||||
|
||||
namespace BVLogicalExpr
|
||||
|
||||
/--
|
||||
Turn a `BoolExpr` into an `Entrypoint`.
|
||||
-/
|
||||
def bitblast (expr : BVLogicalExpr) : Entrypoint BVBit :=
|
||||
go AIG.empty expr .empty |>.result.val
|
||||
where
|
||||
go (aig : AIG BVBit) (expr : BVLogicalExpr) (cache : BVExpr.Cache aig) : Return aig :=
|
||||
match expr with
|
||||
| .literal var => BVPred.bitblast aig ⟨var, cache⟩
|
||||
| .const val =>
|
||||
have := LawfulOperator.le_size (f := mkConstCached) ..
|
||||
⟨⟨aig.mkConstCached val, this⟩, cache.cast this⟩
|
||||
| .not expr =>
|
||||
let ⟨⟨⟨aig, exprRef⟩, hexpr⟩, cache⟩ := go aig expr cache
|
||||
let ret := aig.mkNotCached exprRef
|
||||
have := LawfulOperator.le_size (f := mkNotCached) ..
|
||||
let cache := cache.cast this
|
||||
have := by
|
||||
apply LawfulOperator.le_size_of_le_aig_size (f := mkNotCached)
|
||||
exact hexpr
|
||||
⟨⟨ret, this⟩, cache⟩
|
||||
| .ite discr lhs rhs =>
|
||||
let ⟨⟨⟨aig, discrRef⟩, dextend⟩, cache⟩ := go aig discr cache
|
||||
let ⟨⟨⟨aig, lhsRef⟩, lextend⟩, cache⟩ := go aig lhs cache
|
||||
let ⟨⟨⟨aig, rhsRef⟩, rextend⟩, cache⟩ := go aig rhs cache
|
||||
let discrRef := discrRef.cast <| by
|
||||
dsimp only at lextend rextend ⊢
|
||||
omega
|
||||
let lhsRef := lhsRef.cast <| by
|
||||
dsimp only at rextend ⊢
|
||||
omega
|
||||
|
||||
let input := ⟨discrRef, lhsRef, rhsRef⟩
|
||||
let ret := aig.mkIfCached input
|
||||
have := LawfulOperator.le_size (f := mkIfCached) ..
|
||||
let cache := cache.cast this
|
||||
have := by
|
||||
apply LawfulOperator.le_size_of_le_aig_size (f := mkIfCached)
|
||||
dsimp only at dextend lextend rextend
|
||||
omega
|
||||
⟨⟨ret, this⟩, cache⟩
|
||||
| .gate g lhs rhs =>
|
||||
let ⟨⟨⟨aig, lhsRef⟩, lextend⟩, cache⟩ := go aig lhs cache
|
||||
let ⟨⟨⟨aig, rhsRef⟩, rextend⟩, cache⟩ := go aig rhs cache
|
||||
let lhsRef := lhsRef.cast <| by
|
||||
dsimp only at rextend ⊢
|
||||
omega
|
||||
let input := ⟨lhsRef, rhsRef⟩
|
||||
match g with
|
||||
| .and =>
|
||||
let ret := aig.mkAndCached input
|
||||
have := LawfulOperator.le_size (f := mkAndCached) ..
|
||||
let cache := cache.cast this
|
||||
have := by
|
||||
apply LawfulOperator.le_size_of_le_aig_size (f := mkAndCached)
|
||||
dsimp only at lextend rextend
|
||||
omega
|
||||
⟨⟨ret, this⟩, cache⟩
|
||||
| .xor =>
|
||||
let ret := aig.mkXorCached input
|
||||
have := LawfulOperator.le_size (f := mkXorCached) ..
|
||||
let cache := cache.cast this
|
||||
have := by
|
||||
apply LawfulOperator.le_size_of_le_aig_size (f := mkXorCached)
|
||||
dsimp only at lextend rextend
|
||||
omega
|
||||
⟨⟨ret, this⟩, cache⟩
|
||||
| .beq =>
|
||||
let ret := aig.mkBEqCached input
|
||||
have := LawfulOperator.le_size (f := mkBEqCached) ..
|
||||
let cache := cache.cast this
|
||||
have := by
|
||||
apply LawfulOperator.le_size_of_le_aig_size (f := mkBEqCached)
|
||||
dsimp only at lextend rextend
|
||||
omega
|
||||
⟨⟨ret, this⟩, cache⟩
|
||||
| .or =>
|
||||
let ret := aig.mkOrCached input
|
||||
have := LawfulOperator.le_size (f := mkOrCached) ..
|
||||
let cache := cache.cast this
|
||||
have := by
|
||||
apply LawfulOperator.le_size_of_le_aig_size (f := mkOrCached)
|
||||
dsimp only at lextend rextend
|
||||
omega
|
||||
⟨⟨ret, this⟩, cache⟩
|
||||
|
||||
namespace bitblast
|
||||
|
||||
theorem go_le_size (aig : AIG BVBit) (expr : BVLogicalExpr) (cache : BVExpr.Cache aig) :
|
||||
aig.decls.size ≤ (go aig expr cache).result.val.aig.decls.size :=
|
||||
(go aig expr cache).result.property
|
||||
|
||||
theorem go_lt_size_of_lt_aig_size (aig : AIG BVBit) (expr : BVLogicalExpr)
|
||||
(cache : BVExpr.Cache aig) (h : x < aig.decls.size) :
|
||||
x < (go aig expr cache).result.val.aig.decls.size := by
|
||||
apply Nat.lt_of_lt_of_le
|
||||
· exact h
|
||||
· apply go_le_size
|
||||
|
||||
theorem go_decl_eq (idx) (aig : AIG BVBit) (cache : BVExpr.Cache aig) (h : idx < aig.decls.size) (hbounds) :
|
||||
(go aig expr cache).result.val.aig.decls[idx]'hbounds = aig.decls[idx] := by
|
||||
induction expr generalizing aig with
|
||||
| const =>
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
|
||||
| literal =>
|
||||
simp only [go]
|
||||
rw [BVPred.bitblast_decl_eq]
|
||||
| not expr ih =>
|
||||
simp only [go]
|
||||
have := go_le_size aig expr cache
|
||||
specialize ih aig cache (by omega) (by omega)
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)]
|
||||
assumption
|
||||
| ite discr lhs rhs dih lih rih =>
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkIfCached), rih, lih, dih]
|
||||
· apply go_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
· apply go_lt_size_of_lt_aig_size
|
||||
apply go_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
· apply go_lt_size_of_lt_aig_size
|
||||
apply go_lt_size_of_lt_aig_size
|
||||
apply go_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
| gate g lhs rhs lih rih =>
|
||||
cases g with
|
||||
| and =>
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkAndCached), rih, lih]
|
||||
· apply go_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
· apply go_lt_size_of_lt_aig_size
|
||||
apply go_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
| xor =>
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkXorCached), rih, lih]
|
||||
· apply go_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
· apply go_lt_size_of_lt_aig_size
|
||||
apply go_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
| beq =>
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih]
|
||||
· apply go_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
· apply go_lt_size_of_lt_aig_size
|
||||
apply go_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
| or =>
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), rih, lih]
|
||||
· apply go_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
· apply go_lt_size_of_lt_aig_size
|
||||
apply go_lt_size_of_lt_aig_size
|
||||
assumption
|
||||
|
||||
theorem go_isPrefix_aig {aig : AIG BVBit} (cache : BVExpr.Cache aig) :
|
||||
IsPrefix aig.decls (go aig expr cache).result.val.aig.decls := by
|
||||
apply IsPrefix.of
|
||||
· intro idx h
|
||||
apply go_decl_eq
|
||||
· apply go_le_size
|
||||
|
||||
theorem go_denote_mem_prefix (aig : AIG BVBit) (cache : BVExpr.Cache aig) (hstart) :
|
||||
⟦
|
||||
(go aig expr cache).result.val.aig,
|
||||
⟨start, inv, go_lt_size_of_lt_aig_size (h := hstart) ..⟩,
|
||||
assign
|
||||
⟧
|
||||
=
|
||||
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
|
||||
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
|
||||
apply go_isPrefix_aig
|
||||
|
||||
end bitblast
|
||||
end BVLogicalExpr
|
||||
|
||||
end Std.Tactic.BVDecide
|
||||
|
|
@ -20,25 +20,99 @@ open Std.Sat.AIG
|
|||
|
||||
namespace BVLogicalExpr
|
||||
|
||||
theorem bitblast.go_eval_eq_eval (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment) :
|
||||
⟦ofBoolExprCached.go aig expr BVPred.bitblast, assign.toAIGAssignment⟧ = expr.eval assign := by
|
||||
namespace bitblast
|
||||
|
||||
mutual
|
||||
|
||||
theorem go_Inv_of_Inv (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment)
|
||||
(cache : BVExpr.Cache aig) (hinv : BVExpr.Cache.Inv assign aig cache) :
|
||||
BVExpr.Cache.Inv assign (go aig expr cache).result.val.aig (go aig expr cache).cache := by
|
||||
induction expr generalizing aig with
|
||||
| const => simp [ofBoolExprCached.go]
|
||||
| literal => simp [ofBoolExprCached.go]
|
||||
| not expr ih => simp [ofBoolExprCached.go, ih]
|
||||
| gate g lhs rhs lih rih => cases g <;> simp [ofBoolExprCached.go, Gate.eval, lih, rih]
|
||||
| const =>
|
||||
simp only [go]
|
||||
apply BVExpr.Cache.Inv_cast
|
||||
apply LawfulOperator.isPrefix_aig (f := mkConstCached)
|
||||
exact hinv
|
||||
| literal =>
|
||||
simp only [go]
|
||||
apply BVPred.bitblast_Inv_of_Inv
|
||||
exact hinv
|
||||
| not expr ih =>
|
||||
simp only [go]
|
||||
apply BVExpr.Cache.Inv_cast
|
||||
· apply LawfulOperator.isPrefix_aig (f := mkNotCached)
|
||||
· apply ih
|
||||
exact hinv
|
||||
| gate g lhs rhs lih rih =>
|
||||
cases g
|
||||
all_goals
|
||||
simp [go, Gate.eval]
|
||||
apply BVExpr.Cache.Inv_cast
|
||||
· apply LawfulOperator.isPrefix_aig
|
||||
· apply rih
|
||||
apply lih
|
||||
exact hinv
|
||||
| ite discr lhs rhs dih lih rih =>
|
||||
simp only [ofBoolExprCached.go, Ref.cast_eq, denote_mkIfCached,
|
||||
ofBoolExprCached.go_denote_entry, eval_ite]
|
||||
rw [ofBoolExprCached.go_denote_mem_prefix, ofBoolExprCached.go_denote_mem_prefix]
|
||||
· simp [dih, lih, rih]
|
||||
· simp [Ref.hgate]
|
||||
simp only [go]
|
||||
apply BVExpr.Cache.Inv_cast
|
||||
· apply LawfulOperator.isPrefix_aig (f := mkIfCached)
|
||||
· apply rih
|
||||
apply lih
|
||||
apply dih
|
||||
exact hinv
|
||||
|
||||
theorem go_eval_eq_eval (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment)
|
||||
(cache : BVExpr.Cache aig) (hinv : BVExpr.Cache.Inv assign aig cache) :
|
||||
⟦(go aig expr cache).result, assign.toAIGAssignment⟧ = expr.eval assign := by
|
||||
induction expr generalizing aig with
|
||||
| const => simp [go]
|
||||
| literal =>
|
||||
simp only [go, eval_literal]
|
||||
rw [BVPred.denote_bitblast]
|
||||
exact hinv
|
||||
| not expr ih =>
|
||||
specialize ih _ _ hinv
|
||||
simp [go, ih]
|
||||
| gate g lhs rhs lih rih =>
|
||||
cases g
|
||||
all_goals
|
||||
simp [go, Gate.eval]
|
||||
congr 1
|
||||
· rw [go_denote_mem_prefix]
|
||||
apply lih
|
||||
exact hinv
|
||||
· apply rih
|
||||
apply go_Inv_of_Inv
|
||||
exact hinv
|
||||
| ite discr lhs rhs dih lih rih =>
|
||||
simp only [go, Ref.cast_eq, denote_mkIfCached, denote_projected_entry,
|
||||
eval_ite, Bool.ite_eq_cond_iff]
|
||||
apply ite_congr
|
||||
· rw [go_denote_mem_prefix]
|
||||
rw [go_denote_mem_prefix]
|
||||
· specialize dih _ _ hinv
|
||||
simp [dih]
|
||||
· simp [Ref.hgate]
|
||||
· intro h
|
||||
rw [go_denote_mem_prefix]
|
||||
apply lih
|
||||
apply go_Inv_of_Inv
|
||||
exact hinv
|
||||
· intro h
|
||||
apply rih
|
||||
apply go_Inv_of_Inv
|
||||
apply go_Inv_of_Inv
|
||||
exact hinv
|
||||
|
||||
end
|
||||
|
||||
end bitblast
|
||||
|
||||
theorem denote_bitblast (expr : BVLogicalExpr) (assign : BVExpr.Assignment) :
|
||||
⟦bitblast expr, assign.toAIGAssignment⟧ = expr.eval assign := by
|
||||
unfold bitblast
|
||||
unfold ofBoolExprCached
|
||||
rw [bitblast.go_eval_eq_eval]
|
||||
apply BVExpr.Cache.Inv_empty
|
||||
|
||||
theorem unsat_of_bitblast (expr : BVLogicalExpr) : expr.bitblast.Unsat → expr.Unsat := by
|
||||
intro h assign
|
||||
|
|
|
|||
|
|
@ -121,8 +121,8 @@ end Cache
|
|||
|
||||
namespace bitblast
|
||||
|
||||
theorem goCache_val_eq_bitblast (aig : AIG BVBit) (expr : BVExpr w) :
|
||||
(goCache aig expr .empty).result.val = bitblast aig expr := by
|
||||
theorem goCache_val_eq_bitblast (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
|
||||
goCache aig expr cache = bitblast aig ⟨expr, cache⟩ := by
|
||||
rfl
|
||||
|
||||
theorem go_denote_mem_prefix (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment)
|
||||
|
|
@ -478,20 +478,46 @@ termination_by idx => (sizeOf expr, 0, idx)
|
|||
|
||||
end
|
||||
|
||||
|
||||
end bitblast
|
||||
|
||||
@[simp]
|
||||
theorem denote_bitblast (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
|
||||
theorem bitblast_aig_IsPrefix (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) :
|
||||
IsPrefix aig.decls (bitblast aig input).result.val.aig.decls := by
|
||||
apply IsPrefix.of
|
||||
· intros
|
||||
apply bitblast_decl_eq
|
||||
· intros
|
||||
apply (bitblast aig input).result.property
|
||||
|
||||
theorem bitblast_denote_mem_prefix (aig : AIG BVBit) (input : WithCache (BVExpr w) aig)
|
||||
(assign : Assignment) (start : Nat) (hstart) :
|
||||
⟦
|
||||
(bitblast aig input).result.val.aig,
|
||||
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply (bitblast aig input).result.property⟩,
|
||||
assign.toAIGAssignment
|
||||
⟧
|
||||
=
|
||||
⟦aig, ⟨start, inv, hstart⟩, assign.toAIGAssignment⟧ := by
|
||||
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
|
||||
apply bitblast_aig_IsPrefix
|
||||
|
||||
theorem bitblast_Inv_of_Inv (input : WithCache (BVExpr w) aig)
|
||||
(hinv : Cache.Inv assign aig input.cache) :
|
||||
Cache.Inv assign (bitblast aig input).result.val.aig (bitblast aig input).cache := by
|
||||
unfold bitblast
|
||||
apply bitblast.goCache_Inv_of_Inv
|
||||
exact hinv
|
||||
|
||||
theorem denote_bitblast (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) (assign : Assignment)
|
||||
(hinv : Cache.Inv assign aig input.cache) :
|
||||
∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦(bitblast aig expr).aig, (bitblast aig expr).vec.get idx hidx, assign.toAIGAssignment⟧
|
||||
⟦(bitblast aig input).result.val.aig, (bitblast aig input).result.val.vec.get idx hidx, assign.toAIGAssignment⟧
|
||||
=
|
||||
(expr.eval assign).getLsbD idx
|
||||
(input.val.eval assign).getLsbD idx
|
||||
:= by
|
||||
intros
|
||||
rw [← bitblast.goCache_val_eq_bitblast]
|
||||
rw [bitblast.goCache_denote_eq]
|
||||
apply Cache.Inv_empty
|
||||
exact hinv
|
||||
|
||||
end BVExpr
|
||||
|
||||
|
|
|
|||
|
|
@ -35,8 +35,7 @@ theorem denote_getD_eq_getLsbD (aig : AIG α) (assign : α → Bool) (x : BitVec
|
|||
omega
|
||||
|
||||
@[simp]
|
||||
theorem denote_blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig)
|
||||
(assign : α → Bool) :
|
||||
theorem denote_blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig) (assign : α → Bool) :
|
||||
⟦blastGetLsbD aig target, assign⟧
|
||||
=
|
||||
if h : target.idx < target.w then
|
||||
|
|
|
|||
|
|
@ -22,9 +22,58 @@ open Std.Sat.AIG
|
|||
|
||||
namespace BVPred
|
||||
|
||||
@[simp]
|
||||
theorem denote_bitblast (aig : AIG BVBit) (pred : BVPred) (assign : BVExpr.Assignment) :
|
||||
⟦bitblast aig pred, assign.toAIGAssignment⟧ = pred.eval assign := by
|
||||
theorem bitblast_aig_IsPrefix (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) :
|
||||
IsPrefix aig.decls (bitblast aig input).result.val.aig.decls := by
|
||||
apply IsPrefix.of
|
||||
· intros
|
||||
apply bitblast_decl_eq
|
||||
· intros
|
||||
apply (bitblast aig input).result.property
|
||||
|
||||
theorem bitblast_denote_mem_prefix (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig)
|
||||
(assign : BVExpr.Assignment) (start : Nat) (hstart) :
|
||||
⟦
|
||||
(bitblast aig input).result.val.aig,
|
||||
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply (bitblast aig input).result.property⟩,
|
||||
assign.toAIGAssignment
|
||||
⟧
|
||||
=
|
||||
⟦aig, ⟨start, inv, hstart⟩, assign.toAIGAssignment⟧ := by
|
||||
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
|
||||
apply bitblast_aig_IsPrefix
|
||||
|
||||
theorem bitblast_Inv_of_Inv (input : BVExpr.WithCache BVPred aig)
|
||||
(hinv : BVExpr.Cache.Inv assign aig input.cache) :
|
||||
BVExpr.Cache.Inv assign (bitblast aig input).result.val.aig (bitblast aig input).cache := by
|
||||
unfold bitblast
|
||||
dsimp only
|
||||
split
|
||||
· next op _ _ =>
|
||||
cases op
|
||||
· dsimp only
|
||||
apply BVExpr.Cache.Inv_cast
|
||||
· apply AIG.LawfulOperator.isPrefix_aig (f := mkEq)
|
||||
· apply BVExpr.bitblast_Inv_of_Inv
|
||||
apply BVExpr.bitblast_Inv_of_Inv
|
||||
exact hinv
|
||||
· dsimp only
|
||||
apply BVExpr.Cache.Inv_cast
|
||||
· apply AIG.LawfulOperator.isPrefix_aig (f := mkUlt)
|
||||
· apply BVExpr.bitblast_Inv_of_Inv
|
||||
apply BVExpr.bitblast_Inv_of_Inv
|
||||
exact hinv
|
||||
· dsimp only
|
||||
apply BVExpr.Cache.Inv_cast
|
||||
· apply AIG.LawfulOperator.isPrefix_aig (f := blastGetLsbD)
|
||||
· apply BVExpr.bitblast_Inv_of_Inv
|
||||
exact hinv
|
||||
|
||||
theorem denote_bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig)
|
||||
(assign : BVExpr.Assignment) (hinv : BVExpr.Cache.Inv assign aig input.cache ) :
|
||||
⟦(bitblast aig input).result.val.aig, (bitblast aig input).result.val.ref, assign.toAIGAssignment⟧
|
||||
=
|
||||
input.val.eval assign := by
|
||||
rcases input with ⟨pred, cache⟩
|
||||
cases pred with
|
||||
| bin lhs op rhs =>
|
||||
cases op with
|
||||
|
|
@ -32,26 +81,36 @@ theorem denote_bitblast (aig : AIG BVBit) (pred : BVPred) (assign : BVExpr.Assig
|
|||
simp only [bitblast, eval_bin, BVBinPred.eval_eq]
|
||||
rw [mkEq_denote_eq]
|
||||
· intros
|
||||
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast)]
|
||||
· simp
|
||||
rw [BVExpr.bitblast_denote_mem_prefix]
|
||||
· simp only [RefVec.get_cast, Ref.cast_eq]
|
||||
rw [BVExpr.denote_bitblast]
|
||||
exact hinv
|
||||
· simp [Ref.hgate]
|
||||
· intros
|
||||
simp
|
||||
rw [BVExpr.denote_bitblast]
|
||||
apply BVExpr.bitblast_Inv_of_Inv
|
||||
exact hinv
|
||||
| ult =>
|
||||
simp only [bitblast, eval_bin, BVBinPred.eval_ult]
|
||||
rw [mkUlt_denote_eq]
|
||||
· intros
|
||||
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast)]
|
||||
· simp
|
||||
rw [BVExpr.bitblast_denote_mem_prefix]
|
||||
· simp only [RefVec.get_cast, Ref.cast_eq]
|
||||
rw [BVExpr.denote_bitblast]
|
||||
exact hinv
|
||||
· simp [Ref.hgate]
|
||||
· intros
|
||||
simp
|
||||
rw [BVExpr.denote_bitblast]
|
||||
apply BVExpr.bitblast_Inv_of_Inv
|
||||
exact hinv
|
||||
| getLsbD expr idx =>
|
||||
simp only [bitblast, denote_blastGetLsbD, BVExpr.denote_bitblast, dite_eq_ite,
|
||||
Bool.if_false_right, eval_getLsbD, Bool.and_iff_right_iff_imp, decide_eq_true_eq]
|
||||
apply BitVec.lt_of_getLsbD
|
||||
simp only [bitblast, denote_projected_entry, denote_blastGetLsbD, eval_getLsbD]
|
||||
split
|
||||
· rw [BVExpr.denote_bitblast]
|
||||
exact hinv
|
||||
· symm
|
||||
apply BitVec.getLsbD_ge
|
||||
omega
|
||||
|
||||
end BVPred
|
||||
|
||||
|
|
|
|||
|
|
@ -5,9 +5,7 @@ Authors: Henrik Böving
|
|||
-/
|
||||
prelude
|
||||
import Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
|
||||
import Std.Tactic.BVDecide.Bitblast.BoolExpr.Circuit
|
||||
|
||||
/-!
|
||||
This directory contains the definition and bitblaster of generic boolean substructures for
|
||||
SMT-like problems.
|
||||
This directory contains the definition of generic boolean substructures for SMT-like problems.
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -1,162 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Henrik Böving
|
||||
-/
|
||||
prelude
|
||||
import Std.Sat.AIG.CachedGates
|
||||
import Std.Sat.AIG.CachedGatesLemmas
|
||||
import Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
|
||||
import Std.Sat.AIG.If
|
||||
|
||||
/-!
|
||||
This module contains the logic to turn a `BoolExpr Nat` into an `AIG` with maximum subterm sharing,
|
||||
through the use of a cache that re-uses sub-circuits if possible.
|
||||
-/
|
||||
|
||||
namespace Std.Tactic.BVDecide
|
||||
|
||||
open Std.Sat Std.Sat.AIG
|
||||
|
||||
variable {β : Type} [Hashable β] [DecidableEq β]
|
||||
|
||||
/--
|
||||
Turn a `BoolExpr` into an `Entrypoint`.
|
||||
-/
|
||||
@[specialize]
|
||||
def ofBoolExprCached (expr : BoolExpr α) (atomHandler : AIG β → α → Entrypoint β)
|
||||
[LawfulOperator β (fun _ => α) atomHandler] : Entrypoint β :=
|
||||
go AIG.empty expr atomHandler |>.val
|
||||
where
|
||||
@[specialize]
|
||||
go (aig : AIG β) (expr : BoolExpr α) (atomHandler : AIG β → α → Entrypoint β)
|
||||
[LawfulOperator β (fun _ => α) atomHandler] :
|
||||
ExtendingEntrypoint aig :=
|
||||
match expr with
|
||||
| .literal var => ⟨atomHandler aig var, by apply LawfulOperator.le_size⟩
|
||||
| .const val => ⟨aig.mkConstCached val, (by apply LawfulOperator.le_size)⟩
|
||||
| .not expr =>
|
||||
let ⟨⟨aig, exprRef⟩, _⟩ := go aig expr atomHandler
|
||||
let ret := aig.mkNotCached exprRef
|
||||
have := LawfulOperator.le_size (f := mkNotCached) aig exprRef
|
||||
⟨ret, by dsimp only [ret] at *; omega⟩
|
||||
| .ite discr lhs rhs =>
|
||||
let ⟨⟨aig, discrRef⟩, dextend⟩ := go aig discr atomHandler
|
||||
let ⟨⟨aig, lhsRef⟩, lextend⟩ := go aig lhs atomHandler
|
||||
let ⟨⟨aig, rhsRef⟩, rextend⟩ := go aig rhs atomHandler
|
||||
let discrRef := discrRef.cast <| by
|
||||
dsimp only at lextend rextend ⊢
|
||||
omega
|
||||
let lhsRef := lhsRef.cast <| by
|
||||
dsimp only at rextend ⊢
|
||||
omega
|
||||
|
||||
let input := ⟨discrRef, lhsRef, rhsRef⟩
|
||||
let ret := aig.mkIfCached input
|
||||
have := LawfulOperator.le_size (f := mkIfCached) aig input
|
||||
⟨ret, by dsimp only [ret] at lextend rextend dextend ⊢; omega⟩
|
||||
| .gate g lhs rhs =>
|
||||
let ⟨⟨aig, lhsRef⟩, lextend⟩ := go aig lhs atomHandler
|
||||
let ⟨⟨aig, rhsRef⟩, rextend⟩ := go aig rhs atomHandler
|
||||
let lhsRef := lhsRef.cast <| by
|
||||
dsimp only at rextend ⊢
|
||||
omega
|
||||
let input := ⟨lhsRef, rhsRef⟩
|
||||
match g with
|
||||
| .and =>
|
||||
let ret := aig.mkAndCached input
|
||||
have := LawfulOperator.le_size (f := mkAndCached) aig input
|
||||
⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
|
||||
| .xor =>
|
||||
let ret := aig.mkXorCached input
|
||||
have := LawfulOperator.le_size (f := mkXorCached) aig input
|
||||
⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
|
||||
| .beq =>
|
||||
let ret := aig.mkBEqCached input
|
||||
have := LawfulOperator.le_size (f := mkBEqCached) aig input
|
||||
⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
|
||||
| .or =>
|
||||
let ret := aig.mkOrCached input
|
||||
have := LawfulOperator.le_size (f := mkOrCached) aig input
|
||||
⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
|
||||
|
||||
namespace ofBoolExprCached
|
||||
|
||||
variable (atomHandler : AIG β → α → Entrypoint β) [LawfulOperator β (fun _ => α) atomHandler]
|
||||
|
||||
theorem go_le_size (expr : BoolExpr α) (aig : AIG β) :
|
||||
aig.decls.size ≤ (ofBoolExprCached.go aig expr atomHandler).val.aig.decls.size :=
|
||||
(ofBoolExprCached.go aig expr atomHandler).property
|
||||
|
||||
theorem go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.size) (hbounds) :
|
||||
(ofBoolExprCached.go aig expr atomHandler).val.aig.decls[idx]'hbounds = aig.decls[idx] := by
|
||||
induction expr generalizing aig with
|
||||
| const =>
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
|
||||
| literal =>
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := atomHandler)]
|
||||
| not expr ih =>
|
||||
simp only [go]
|
||||
have := go_le_size atomHandler expr aig
|
||||
specialize ih aig (by omega) (by omega)
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)]
|
||||
assumption
|
||||
| ite discr lhs rhs dih lih rih =>
|
||||
have := go_le_size atomHandler discr aig
|
||||
have := go_le_size atomHandler lhs (go aig discr atomHandler).val.aig
|
||||
have := go_le_size atomHandler rhs (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig
|
||||
specialize dih aig (by omega) (by omega)
|
||||
specialize lih (go aig discr atomHandler).val.aig (by omega) (by omega)
|
||||
specialize rih (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig (by omega) (by omega)
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkIfCached), rih, lih, dih]
|
||||
| gate g lhs rhs lih rih =>
|
||||
have := go_le_size atomHandler lhs aig
|
||||
have := go_le_size atomHandler rhs (go aig lhs atomHandler).val.aig
|
||||
specialize lih aig (by omega) (by omega)
|
||||
specialize rih (go aig lhs atomHandler).val.aig (by omega) (by omega)
|
||||
cases g with
|
||||
| and =>
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkAndCached), rih, lih]
|
||||
| xor =>
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkXorCached), rih, lih]
|
||||
| beq =>
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih]
|
||||
| or =>
|
||||
simp only [go]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), rih, lih]
|
||||
|
||||
theorem go_isPrefix_aig {aig : AIG β} :
|
||||
IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls := by
|
||||
apply IsPrefix.of
|
||||
· intro idx h
|
||||
apply ofBoolExprCached.go_decl_eq
|
||||
· apply go_le_size
|
||||
|
||||
theorem go_denote_mem_prefix :
|
||||
⟦
|
||||
(go aig expr atomHandler).val.aig,
|
||||
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
|
||||
assign
|
||||
⟧
|
||||
=
|
||||
⟦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, entry.ref.invert, h⟩, assign⟧
|
||||
=
|
||||
⟦entry, assign⟧ := by
|
||||
apply denote.eq_of_isPrefix
|
||||
apply ofBoolExprCached.go_isPrefix_aig
|
||||
|
||||
end ofBoolExprCached
|
||||
|
||||
end Std.Tactic.BVDecide
|
||||
|
|
@ -1,9 +1,9 @@
|
|||
import Std.Tactic.BVDecide.Bitblast.BoolExpr
|
||||
import Std.Tactic.BVDecide.Bitblast
|
||||
|
||||
open Std.Sat
|
||||
open Std.Tactic.BVDecide
|
||||
|
||||
def mkFalseCollapsible (n : Nat) : BoolExpr Nat :=
|
||||
def mkFalseCollapsible (n : Nat) : BVLogicalExpr :=
|
||||
match n with
|
||||
| 0 => .const false
|
||||
| n + 1 =>
|
||||
|
|
@ -12,13 +12,13 @@ def mkFalseCollapsible (n : Nat) : BoolExpr Nat :=
|
|||
|
||||
/-- info: #[Std.Sat.AIG.Decl.const false] -/
|
||||
#guard_msgs in
|
||||
#eval ofBoolExprCached (mkFalseCollapsible 1) AIG.mkAtomCached |>.aig.decls
|
||||
#eval BVLogicalExpr.bitblast (mkFalseCollapsible 1) |>.aig.decls
|
||||
|
||||
/-- info: #[Std.Sat.AIG.Decl.const false] -/
|
||||
#guard_msgs in
|
||||
#eval ofBoolExprCached (mkFalseCollapsible 16) AIG.mkAtomCached |>.aig.decls
|
||||
#eval BVLogicalExpr.bitblast (mkFalseCollapsible 16) |>.aig.decls
|
||||
|
||||
def mkTrueCollapsible (n : Nat) : BoolExpr Nat :=
|
||||
def mkTrueCollapsible (n : Nat) : BVLogicalExpr :=
|
||||
match n with
|
||||
| 0 => .const true
|
||||
| n + 1 =>
|
||||
|
|
@ -27,13 +27,13 @@ def mkTrueCollapsible (n : Nat) : BoolExpr Nat :=
|
|||
|
||||
/-- info: #[Std.Sat.AIG.Decl.const true] -/
|
||||
#guard_msgs in
|
||||
#eval ofBoolExprCached (mkTrueCollapsible 1) AIG.mkAtomCached |>.aig.decls
|
||||
#eval BVLogicalExpr.bitblast (mkTrueCollapsible 1) |>.aig.decls
|
||||
|
||||
/-- info: #[Std.Sat.AIG.Decl.const true] -/
|
||||
#guard_msgs in
|
||||
#eval ofBoolExprCached (mkTrueCollapsible 16) AIG.mkAtomCached |>.aig.decls
|
||||
#eval BVLogicalExpr.bitblast (mkTrueCollapsible 16) |>.aig.decls
|
||||
|
||||
def mkConstantCollapsible (n : Nat) : BoolExpr Nat :=
|
||||
def mkConstantCollapsible (n : Nat) : BVLogicalExpr :=
|
||||
match n with
|
||||
| 0 => .const false
|
||||
| n + 1 =>
|
||||
|
|
@ -43,11 +43,11 @@ def mkConstantCollapsible (n : Nat) : BoolExpr Nat :=
|
|||
/-- info: (2, Std.Sat.AIG.Decl.const false) -/
|
||||
#guard_msgs in
|
||||
#eval
|
||||
let entry := ofBoolExprCached (mkConstantCollapsible 1) AIG.mkAtomCached
|
||||
let entry := BVLogicalExpr.bitblast (mkConstantCollapsible 1)
|
||||
(entry.aig.decls.size, entry.aig.decls[entry.ref.gate]!)
|
||||
|
||||
/-- info: (2, Std.Sat.AIG.Decl.const false) -/
|
||||
#guard_msgs in
|
||||
#eval
|
||||
let entry := ofBoolExprCached (mkConstantCollapsible 16) AIG.mkAtomCached
|
||||
let entry := BVLogicalExpr.bitblast (mkConstantCollapsible 16)
|
||||
(entry.aig.decls.size, entry.aig.decls[entry.ref.gate]!)
|
||||
|
|
|
|||
|
|
@ -1,48 +0,0 @@
|
|||
import Std.Tactic.BVDecide.Bitblast.BoolExpr
|
||||
|
||||
open Std.Sat
|
||||
open Std.Tactic.BVDecide
|
||||
|
||||
def mkSharedTree (n : Nat) : BoolExpr Nat :=
|
||||
match n with
|
||||
| 0 => .literal 0
|
||||
| n + 1 =>
|
||||
let tree := mkSharedTree n
|
||||
.gate .xor tree tree
|
||||
|
||||
/--
|
||||
info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true]
|
||||
-/
|
||||
#guard_msgs in
|
||||
#eval ofBoolExprCached (mkSharedTree 1) AIG.mkAtomCached |>.aig.decls
|
||||
|
||||
/--
|
||||
info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true,
|
||||
Std.Sat.AIG.Decl.gate 2 2 true true, Std.Sat.AIG.Decl.gate 2 3 true true]
|
||||
-/
|
||||
#guard_msgs in
|
||||
#eval ofBoolExprCached (mkSharedTree 2) AIG.mkAtomCached |>.aig.decls
|
||||
|
||||
/--
|
||||
info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true,
|
||||
Std.Sat.AIG.Decl.gate 2 2 true true, Std.Sat.AIG.Decl.gate 2 3 true true, Std.Sat.AIG.Decl.gate 4 4 true true,
|
||||
Std.Sat.AIG.Decl.gate 4 5 true true, Std.Sat.AIG.Decl.gate 6 6 true true, Std.Sat.AIG.Decl.gate 6 7 true true]
|
||||
-/
|
||||
#guard_msgs in
|
||||
#eval ofBoolExprCached (mkSharedTree 4) AIG.mkAtomCached |>.aig.decls
|
||||
|
||||
/--
|
||||
info: #[Std.Sat.AIG.Decl.atom 0, Std.Sat.AIG.Decl.gate 0 0 true true, Std.Sat.AIG.Decl.gate 0 1 true true,
|
||||
Std.Sat.AIG.Decl.gate 2 2 true true, Std.Sat.AIG.Decl.gate 2 3 true true, Std.Sat.AIG.Decl.gate 4 4 true true,
|
||||
Std.Sat.AIG.Decl.gate 4 5 true true, Std.Sat.AIG.Decl.gate 6 6 true true, Std.Sat.AIG.Decl.gate 6 7 true true,
|
||||
Std.Sat.AIG.Decl.gate 8 8 true true, Std.Sat.AIG.Decl.gate 8 9 true true, Std.Sat.AIG.Decl.gate 10 10 true true,
|
||||
Std.Sat.AIG.Decl.gate 10 11 true true, Std.Sat.AIG.Decl.gate 12 12 true true, Std.Sat.AIG.Decl.gate 12 13 true true,
|
||||
Std.Sat.AIG.Decl.gate 14 14 true true, Std.Sat.AIG.Decl.gate 14 15 true true, Std.Sat.AIG.Decl.gate 16 16 true true,
|
||||
Std.Sat.AIG.Decl.gate 16 17 true true, Std.Sat.AIG.Decl.gate 18 18 true true, Std.Sat.AIG.Decl.gate 18 19 true true,
|
||||
Std.Sat.AIG.Decl.gate 20 20 true true, Std.Sat.AIG.Decl.gate 20 21 true true, Std.Sat.AIG.Decl.gate 22 22 true true,
|
||||
Std.Sat.AIG.Decl.gate 22 23 true true, Std.Sat.AIG.Decl.gate 24 24 true true, Std.Sat.AIG.Decl.gate 24 25 true true,
|
||||
Std.Sat.AIG.Decl.gate 26 26 true true, Std.Sat.AIG.Decl.gate 26 27 true true, Std.Sat.AIG.Decl.gate 28 28 true true,
|
||||
Std.Sat.AIG.Decl.gate 28 29 true true, Std.Sat.AIG.Decl.gate 30 30 true true, Std.Sat.AIG.Decl.gate 30 31 true true]
|
||||
-/
|
||||
#guard_msgs in
|
||||
#eval ofBoolExprCached (mkSharedTree 16) AIG.mkAtomCached |>.aig.decls
|
||||
Loading…
Add table
Reference in a new issue