diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-07-16 10:03:02 +0200 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-07-24 16:11:01 +0200 |
| commit | 728eb045e69f6a69c0cd089ba26e921d6bb65540 (patch) | |
| tree | 6c088d38ce3bfb834edaf8b4ef11bf2eadbd0ded | |
| parent | c4d44af5f3135aba4d4878f8f41c80d1f0b9e9a2 (diff) | |
| download | vericert-kvx-728eb045e69f6a69c0cd089ba26e921d6bb65540.tar.gz vericert-kvx-728eb045e69f6a69c0cd089ba26e921d6bb65540.zip | |
Finish SAT proof
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index ecd644b..36856f0 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -198,8 +198,9 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : end end); split; intros; simpl in *; auto. - inv H. inv H0; auto. - - admit. - - admit. + - split; auto. destruct (a p') eqn:?; crush. + - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto. + crush. - apply satFormula_concat. apply andb_prop in H. inv H. apply i in H0. auto. apply andb_prop in H. inv H. apply i0 in H1. auto. @@ -211,7 +212,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : - apply orb_true_intro. apply satFormula_mult2 in H. inv H. apply i in H0. auto. apply i0 in H0. auto. -Admitted. +Qed. Definition sat_pred (bound: nat) (p: pred_op) : option ({al : alist | sat_predicate p (interp_alist al) = true} |