CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature. Add regressions.

4 files changed, 93 insertions, 1 deletions

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index da992286e..a8e7b6a8e 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -45,7 +45,10 @@ TESTS =	\
 	simple.02.cvc \
 	simple.03.cvc \
 	simple.04.cvc \
-	proof00.smt2
+	proof00.smt2 \
+	cnf-iff.smt2 \
+	cnf-iff-base.smt2 \
+	cnf-ite.smt2
 
 EXTRA_DIST = $(TESTS) \
 	mkpidgeon
diff --git a/test/regress/regress0/uf/cnf-iff-base.smt2 b/test/regress/regress0/uf/cnf-iff-base.smt2
new file mode 100644
index 000000000..9c538de6c
--- /dev/null
+++ b/test/regress/regress0/uf/cnf-iff-base.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort U 0)
+
+(declare-fun f (U) U)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+
+(assert (= (not (= (f a) d)) (not (= d (f b)))))
+
+(assert (or (not (= (f a) d)) (not (= d (f b)))))
+(assert (or (= (f a) d) (= d (f b))))
+
+(check-sat)
diff --git a/test/regress/regress0/uf/cnf-iff.smt2 b/test/regress/regress0/uf/cnf-iff.smt2
new file mode 100644
index 000000000..03377005c
--- /dev/null
+++ b/test/regress/regress0/uf/cnf-iff.smt2
@@ -0,0 +1,38 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort U 0)
+
+(declare-fun f (U) U)
+(declare-fun g (U) U)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(declare-fun e () U)
+(declare-fun h () U)
+(declare-fun i () U)
+
+(assert (or 
+(= a c)
+(= h c)
+(not (= h d))
+(not (= h e))
+(= h i)
+(= (= (f a) d) (= d (f b)))
+(= (not (= (f a) d)) (not (= d (f b))))
+(not (= (not (= d (f b))) (= (f a) d)))
+(not (= (= d (f b)) (not (= (f a) d))))
+(xor (= (f a) d) (not (= d (f b))))
+(xor (not (= (f a) d)) (= d (f b)))
+(not (xor (= (f a) d) (= d (f b))))
+(not (xor (not (= (f a) d)) (not (= d (f b)))))
+))
+(assert (not (= h i)))
+(assert (or (not (= (f a) d)) (not (= d (f b)))))
+(assert (or (= (f a) d) (= d (f b))))
+(assert (and (not (= b e)) (not (= c a))))
+(assert (and (= h e) (not (= b e))))
+
+(assert (not (or (= b h) (= c h))))
+(assert (not (or (= b h) (not (= d h)))))
+(check-sat)
diff --git a/test/regress/regress0/uf/cnf-ite.smt2 b/test/regress/regress0/uf/cnf-ite.smt2
new file mode 100644
index 000000000..851eb45aa
--- /dev/null
+++ b/test/regress/regress0/uf/cnf-ite.smt2
@@ -0,0 +1,35 @@
+; COMMAND-LINE: --simplification=none
+; EXPECT: unsat
+
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort U 0)
+
+(declare-fun f (U) U)
+(declare-fun g (U) U)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(declare-fun e () U)
+(declare-fun h () U)
+(declare-fun i () U)
+
+(assert (or 
+(ite (= (f a) d) (not (= d (f b))) (= a c))
+(ite (not (= (f a) d)) (= d e) (not (= d (f b))))
+(not (ite (not (= (f a) d)) (= d e) (= d (f b))))
+(not (ite (= (f a) d) (= d (f b)) (= a c)))
+(ite (not (= (f a) e)) (= e (f b)) (= a c))
+(ite (= (f a) e) (= e e) (= e (f b)))
+(not (ite (= (f a) e) (= e e) (not (= e (f b)))))
+(not (ite (not (= (f a) e)) (not (= e (f b))) (= a c)))
+(= a b)
+))
+
+(assert (and (= (f a) d) (= d (f b))))
+(assert (and (not (= (f a) e)) (not (= e (f b)))))
+
+(assert (not (= a b)))
+
+(check-sat)