8b5443eb22
This is the first step towards fixing the issue of not having mutual recursion between the `Bool` and `BitVec` fragment of `QF_BV` in `bv_decide`. This PR adds support for `BitVec.ofBool` by doing the following: 1. Introduce a new mechanism into the reification engine that allows us to add additional lemmas to the top level on the fly as we are traversing the expression tree. 2. If we encounter an expression `BitVec.ofBool boolExpr` we reify `boolExpr` and then abstract `BitVec.ofBool boolExpr` as some atom `a` 3. We add two lemmas `boolExpr = true -> a = 1#1` and `boolExpr = false -> a = 0#1`. This mirrors the full behavior of `BitVec.ofBool` and thus makes our atom `a` correctly interpreted again. In order to do the reification in step 2 mutual recursion in the reification engine is required. For this reason I started pulling out logic from the, now rather large, mutual block into other files and document the invariants that they assume explicitly. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||