diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-10-19 22:03:54 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-19 22:03:54 +0100 |
| commit | b82b449b12650133accccd33b1d39a25ae9bb087 (patch) | |
| tree | ad0e07a655af54d9b95f8989c138da3324c53392 /src/hls/RTLBlockInstr.v | |
| parent | fe06668f0de56635efe55310d7a64289a37c1d90 (diff) | |
| download | vericert-b82b449b12650133accccd33b1d39a25ae9bb087.tar.gz vericert-b82b449b12650133accccd33b1d39a25ae9bb087.zip | |
Continuations on proof of predicates
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 56048d4..5e17115 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -159,35 +159,6 @@ Proof. apply satFormula_mult2' in H1. inv H1; crush. Qed. -Fixpoint trans_pred_temp (bound: nat) (p: pred_op) : option formula := - match bound with - | O => None - | S n => - match p with - | Pvar p' => Some (((true, Pos.to_nat p') :: nil) :: nil) - | Ptrue => Some nil - | Pfalse => Some (nil::nil) - | Pand p1 p2 => - match trans_pred_temp n p1, trans_pred_temp n p2 with - | Some p1', Some p2' => - Some (p1' ++ p2') - | _, _ => None - end - | Por p1 p2 => - match trans_pred_temp n p1, trans_pred_temp n p2 with - | Some p1', Some p2' => - Some (mult p1' p2') - | _, _ => None - end - | Pnot Pfalse => Some nil - | Pnot Ptrue => Some (nil::nil) - | Pnot (Pvar p') => Some (((false, Pos.to_nat p') :: nil) :: nil) - | Pnot (Pnot p) => trans_pred_temp n p - | Pnot (Pand p1 p2) => trans_pred_temp n (Por (Pnot p1) (Pnot p2)) - | Pnot (Por p1 p2) => trans_pred_temp n (Pand (Pnot p1) (Pnot p2)) - end - end. - Fixpoint trans_pred (bound: nat) (p: pred_op) : option {fm: formula | forall a, sat_predicate p a = true <-> satFormula fm a}. |