mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
54 lines
1.4 KiB
Lean4
54 lines
1.4 KiB
Lean4
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.false] -/
|
|
#guard_msgs in
|
|
#eval BVLogicalExpr.bitblast (mkFalseCollapsible 1) |>.aig.decls
|
|
|
|
/-- info: #[Std.Sat.AIG.Decl.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.false] -/
|
|
#guard_msgs in
|
|
#eval BVLogicalExpr.bitblast (mkTrueCollapsible 1) |>.aig.decls
|
|
|
|
/-- info: #[Std.Sat.AIG.Decl.false] -/
|
|
#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: (1, Std.Sat.AIG.Decl.false) -/
|
|
#guard_msgs in
|
|
#eval
|
|
let entry := BVLogicalExpr.bitblast (mkConstantCollapsible 1)
|
|
(entry.aig.decls.size, entry.aig.decls[entry.ref.gate]!)
|
|
|
|
/-- info: (1, Std.Sat.AIG.Decl.false) -/
|
|
#guard_msgs in
|
|
#eval
|
|
let entry := BVLogicalExpr.bitblast (mkConstantCollapsible 16)
|
|
(entry.aig.decls.size, entry.aig.decls[entry.ref.gate]!)
|