f241cc832b
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.
53 lines
1.4 KiB
Text
53 lines
1.4 KiB
Text
import Std.Tactic.BVDecide.Bitblast
|
|
|
|
open Std.Sat
|
|
open Std.Tactic.BVDecide
|
|
|
|
def mkFalseCollapsible (n : Nat) : BVLogicalExpr :=
|
|
match n with
|
|
| 0 => .const false
|
|
| n + 1 =>
|
|
let tree := mkFalseCollapsible n
|
|
.gate .and tree tree
|
|
|
|
/-- info: #[Std.Sat.AIG.Decl.const false] -/
|
|
#guard_msgs in
|
|
#eval BVLogicalExpr.bitblast (mkFalseCollapsible 1) |>.aig.decls
|
|
|
|
/-- info: #[Std.Sat.AIG.Decl.const false] -/
|
|
#guard_msgs in
|
|
#eval BVLogicalExpr.bitblast (mkFalseCollapsible 16) |>.aig.decls
|
|
|
|
def mkTrueCollapsible (n : Nat) : BVLogicalExpr :=
|
|
match n with
|
|
| 0 => .const true
|
|
| n + 1 =>
|
|
let tree := mkTrueCollapsible n
|
|
.gate .and tree tree
|
|
|
|
/-- info: #[Std.Sat.AIG.Decl.const true] -/
|
|
#guard_msgs in
|
|
#eval BVLogicalExpr.bitblast (mkTrueCollapsible 1) |>.aig.decls
|
|
|
|
/-- info: #[Std.Sat.AIG.Decl.const true] -/
|
|
#guard_msgs in
|
|
#eval BVLogicalExpr.bitblast (mkTrueCollapsible 16) |>.aig.decls
|
|
|
|
def mkConstantCollapsible (n : Nat) : BVLogicalExpr :=
|
|
match n with
|
|
| 0 => .const false
|
|
| n + 1 =>
|
|
let tree := mkTrueCollapsible n
|
|
.gate .and (.gate .and tree tree) (.const false)
|
|
|
|
/-- info: (2, Std.Sat.AIG.Decl.const false) -/
|
|
#guard_msgs in
|
|
#eval
|
|
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 := BVLogicalExpr.bitblast (mkConstantCollapsible 16)
|
|
(entry.aig.decls.size, entry.aig.decls[entry.ref.gate]!)
|