diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:16:44 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:16:44 +0100 |
| commit | c321e39de166308d8db2f6ebe577edb3297b507c (patch) | |
| tree | b3b4d1769b3f19915ccecfe778d71543c7020bdc | |
| parent | 05afcff334725e885522e9859b9ab735a404014c (diff) | |
| download | vericert-c321e39de166308d8db2f6ebe577edb3297b507c.tar.gz vericert-c321e39de166308d8db2f6ebe577edb3297b507c.zip | |
Remove tseytin transformation temporarily
| -rw-r--r-- | src/hls/Predicate.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 _) |