From 1850879e7e196c0e1c00900acf5facaaf5387beb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 18 Sep 2023 10:55:13 +0100 Subject: Add benchmarking of unhashed commands --- src/hls/GiblePargenproofEquiv.v | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'src/hls') 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)])). *) -- cgit