From c321e39de166308d8db2f6ebe577edb3297b507c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 10 Aug 2023 11:16:44 +0100 Subject: Remove tseytin transformation temporarily --- src/hls/Predicate.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index d4bc80a..c03aa11 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -690,7 +690,7 @@ Definition sat_pred_tseytin (p: pred_op) : ({al : alist | sat_predicate p (interp_alist al) = true} + {forall a : asgn, sat_predicate p a = false}). refine - ( match tseytin p with + ( match trans_pred p with | exist _ fm _ => match sat_solve fm with | inleft (exist _ a _) => inleft (exist _ a _) -- cgit