diff options
| author | Brian Campbell | 2019-03-01 10:41:33 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-01 12:05:29 +0000 |
| commit | 576fb915bc281ea8e59eba896e3404d2f85e918c (patch) | |
| tree | 99267bd1f50e9704acd5407ef98b7e6fefaf0bd4 | |
| parent | dfb2ca35204870809730a0feb0ba98c1f45f57ac (diff) | |
Coq: add a little bit of boolean solving
Just enough for RISC-V to go through
| -rw-r--r-- | lib/coq/Sail2_values.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 1b5da853..e6c5e786 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1208,6 +1208,14 @@ prepare_for_solver; | constructor; eauto 3 with zarith sail (* The datatypes hints give us some list handling, esp In *) | constructor; drop_exists; eauto 3 with datatypes zarith sail + (* Booleans - and_boolMP *) + | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _, _) => + constructor; intros l r H1 H2; + solve [exists l; destruct l; intuition | exists r; destruct l; intuition] + end + | match goal with |- context [@eq _ _ _] => + constructor; intuition + end | constructor; idtac "Unable to solve constraint"; dump_context; fail ]. (* Add an indirection so that you can redefine run_solver to fail to get |