diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-09-18 10:55:13 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-09-18 10:55:13 +0100 |
| commit | 1850879e7e196c0e1c00900acf5facaaf5387beb (patch) | |
| tree | 9f02c7e07881b29f1d83a18dd199533751b7e09f /src/hls | |
| parent | 6a74d2e648903e54300f276a024e396978629b30 (diff) | |
| download | vericert-debug/unhashed.tar.gz vericert-debug/unhashed.zip | |
Add benchmarking of unhashed commandsdebug/unhashed
Diffstat (limited to 'src/hls')
| -rw-r--r-- | src/hls/GiblePargenproofEquiv.v | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v index 262e9d5..702da5b 100644 --- a/src/hls/GiblePargenproofEquiv.v +++ b/src/hls/GiblePargenproofEquiv.v @@ -1547,12 +1547,13 @@ Definition check_mutexcl {A} eq_dec (pe: predicated A) := else false. Definition check_mutexcl_unhashed {A} eq_dec (preds: PTree.t pred_pexpr) (pe: predicated A) := - if NE.norepet_check eq_dec pe then - let lpe := NE.to_list pe in - let pairs := map (fun x => fst x → negate (or_list (map fst (remove eq_dec x lpe)))) lpe in - let (np1, h) := TVL.hash_predicate (transf_pred_op (from_pred_op preds (simplify (and_list pairs)))) (Maps.PTree.empty _) in - STV.check_smt_total np1 - else false. + (* if NE.norepet_check eq_dec pe then *) + (* let lpe := NE.to_list pe in *) + (* let pairs := map (fun x => fst x → negate (or_list (map fst (remove eq_dec x lpe)))) lpe in *) + (* let (np1, h) := TVL.hash_predicate (transf_pred_op (from_pred_op preds (simplify (and_list pairs)))) (Maps.PTree.empty _) in *) + (* STV.check_smt_total np1 *) + (* else false. *) + check_mutexcl eq_dec pe. (* Import ListNotations. *) (* Compute deep_simplify peq (and_list (map (fun x => x → negate (or_list (remove (Predicate.eq_dec peq) x [Plit (true, 2)]))) [Plit (true, 2)])). *) |