diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:20:34 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:20:34 +0100 |
| commit | 4d62c7f35533ebd36ae4a0bdef6cd64fcc0be375 (patch) | |
| tree | f540d9c6a48eef5478950aa8572b5706fcc11ab2 | |
| parent | 471e2df0abea898607f20ac78c123ff8d9835777 (diff) | |
| download | vericert-4d62c7f35533ebd36ae4a0bdef6cd64fcc0be375.tar.gz vericert-4d62c7f35533ebd36ae4a0bdef6cd64fcc0be375.zip | |
Abort steytin proofs
| -rw-r--r-- | src/hls/Predicate.v | 4 |
1 files 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 |