diff options
Diffstat (limited to 'src/hls/GiblePargenproofEquiv.v')
| -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)])). *) |