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.
34 lines
1,011 B
Text
34 lines
1,011 B
Text
import Std.Tactic.BVDecide
|
|
|
|
inductive Bar : Type
|
|
| A : Bar
|
|
| B : Bar
|
|
| C : Bar -- Requires extra variant in enum
|
|
deriving DecidableEq
|
|
structure Foo where
|
|
state : Bar
|
|
num : BitVec 1
|
|
deriving DecidableEq
|
|
def r' (b : Bool)
|
|
: Bool :=
|
|
-- Two inline if-statements
|
|
let a : Foo :=
|
|
if b then { state := .A, num := 0 }
|
|
else { state := .B, num := 0 }
|
|
let x : Foo :=
|
|
if a.state = .A then { state := .A, num := 0}
|
|
else { state := .B, num := 0 }
|
|
x.num.getLsbD 0
|
|
|
|
/--
|
|
error: None of the hypotheses are in the supported BitVec fragment after applying preprocessing.
|
|
There are three potential reasons for this:
|
|
1. If you are using custom BitVec constructs simplify them to built-in ones.
|
|
2. If your problem is using only built-in ones it might currently be out of reach.
|
|
Consider expressing it in terms of different operations that are better supported.
|
|
3. The original goal was reduced to False and is thus invalid.
|
|
-/
|
|
#guard_msgs in
|
|
theorem wtf (a : Bool) : r' a := by
|
|
simp [r']
|
|
bv_decide
|