From 4d62c7f35533ebd36ae4a0bdef6cd64fcc0be375 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 10 Aug 2023 11:20:34 +0100 Subject: Abort steytin proofs --- src/hls/Predicate.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index c03aa11..3cd9b0f 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -659,7 +659,7 @@ Proof. eapply stseytin_and_correct. unfold stseytin_and. eauto. unfold sat_lit. simpl. admit. inv H; try contradiction. inv H1; try contradiction. eauto.*) -Admitted. +Abort. Fixpoint max_predicate (p: pred_op) : positive := match p with @@ -679,7 +679,7 @@ Definition tseytin (p: pred_op) : {fm: formula | forall a, sat_predicate p a = true <-> sat_formula fm a} with (m, n, fm) => fun H => exist _ ((n::nil) :: fm) _ end) (eq_refl (xtseytin (max_predicate p + 1) p))). - intros. eapply xtseytin_correct; eauto. Defined. + intros. Abort. Definition tseytin_simple (p: pred_op) : formula := let m := (max_predicate p + 1)%positive in -- cgit