diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-10 15:15:26 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-10 15:15:26 +0100 |
commit | 10df4ba0752eb23c76b9aa847e3ad116673a47b6 (patch) | |
tree | f41eec3963b7a9d96c0ea85179227d88ae57f0f6 /test/regress | |
parent | 8d140a28c76095e148acd64e47b5ca0a92ca09be (diff) |
CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature. Add regressions.
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/uf/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/uf/cnf-iff-base.smt2 | 16 | ||||
-rw-r--r-- | test/regress/regress0/uf/cnf-iff.smt2 | 38 | ||||
-rw-r--r-- | test/regress/regress0/uf/cnf-ite.smt2 | 35 |
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) |