From de7eaa6a891e9b4d0111f7ccc11fdc59bb3f2ac6 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 5 Feb 2025 14:16:39 -0300 Subject: [PATCH] tests --- simple-cong.cnf | 24 ++++++++++++++++++++++++ simple-cong.smt2 | 24 ++++++++++++++++++++++++ 2 files changed, 48 insertions(+) create mode 100644 simple-cong.cnf create mode 100644 simple-cong.smt2 diff --git a/simple-cong.cnf b/simple-cong.cnf new file mode 100644 index 00000000000..59ef19905cd --- /dev/null +++ b/simple-cong.cnf @@ -0,0 +1,24 @@ +p cnf 10 10 +1 0 +2 0 +3 0 +c 4 0 +-9 6 0 +c 5 0 +-8 -10 0 +6 -7 -8 0 +-6 8 0 +-6 7 0 +9 0 +10 -1 -2 0 + +c 1 (= a b) +c 2 (= c d) +c 3 (and p1 true) +c 4 (or (not p1) (and p2 p3)) +c 5 (or (not p3) (not (= (f a c) (f b d)))) +c 6 (and p2 p3) +c 7 (not p2) +c 8 (not p3) +c 9 p1 +c 10 (= (f a c) (f b d)) \ No newline at end of file diff --git a/simple-cong.smt2 b/simple-cong.smt2 new file mode 100644 index 00000000000..948d3256580 --- /dev/null +++ b/simple-cong.smt2 @@ -0,0 +1,24 @@ +(set-logic QF_UF) +(set-option :simplification none) + +(declare-sort U 0) + +(declare-const p1 Bool) +(declare-const p2 Bool) +(declare-const p3 Bool) + +(declare-const a U) +(declare-const b U) +(declare-const c U) +(declare-const d U) +(declare-fun f (U U) U) + +(assert (= a b)) +(assert (= c d)) +(assert (and p1 true)) +(assert (or (not p1) (and p2 p3))) +(assert (or (not p3) (not (= (f a c) (f b d))))) + +; (or (not (= a b)) (not (= c d)) (= (f a c) (f b d))) + +(check-sat)