From: Tim King Date: Tue, 26 Jan 2010 17:55:28 +0000 (+0000) Subject: Added test/regress/boolean.cvc X-Git-Tag: cvc5-1.0.0~9338 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aaecc4532bb39f7e5c35f6f11c6eb5962ad4016d;p=cvc5.git Added test/regress/boolean.cvc --- diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index c5e6ec676..ba7fd1309 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -33,5 +33,6 @@ TESTS = \ bmc-ibm-12.smt \ bmc-ibm-13.smt \ wiki.cvc \ - logops.cvc + logops.cvc \ + comb2.shuffled-as.sat03-420.smt diff --git a/test/regress/Makefile.in b/test/regress/Makefile.in index 2670ecd65..0db9d0004 100644 --- a/test/regress/Makefile.in +++ b/test/regress/Makefile.in @@ -227,7 +227,8 @@ TESTS = \ bmc-ibm-12.smt \ bmc-ibm-13.smt \ wiki.cvc \ - logops.cvc + logops.cvc \ + comb2.shuffled-as.sat03-420.smt all: all-am diff --git a/test/regress/boolean.cvc b/test/regress/boolean.cvc new file mode 100644 index 000000000..ac9885703 --- /dev/null +++ b/test/regress/boolean.cvc @@ -0,0 +1,809 @@ +%% Regression level = 1 +%% Result = Valid +%% Runtime = 1 +%% Language = presentation +p : BOOLEAN; +q : BOOLEAN; +r : BOOLEAN; +s : BOOLEAN; +t : BOOLEAN; +u : BOOLEAN; +v : BOOLEAN; +P1 : BOOLEAN; +P2 : BOOLEAN; +P3 : BOOLEAN; +P4 : BOOLEAN; +P6 : BOOLEAN; +P5 : BOOLEAN; +a41 : BOOLEAN = + IF p THEN FALSE + ELSE TRUE + ENDIF; +a42 : BOOLEAN = + IF a41 THEN FALSE + ELSE TRUE + ENDIF; +a45 : BOOLEAN = + IF p THEN p + ELSE a41 + ENDIF; +a46 : BOOLEAN = + IF q THEN FALSE + ELSE TRUE + ENDIF; +a49 : BOOLEAN = + IF s THEN t + ELSE FALSE + ENDIF; +a58 : BOOLEAN = + IF q THEN q + ELSE a46 + ENDIF; +a59 : BOOLEAN = + IF r THEN FALSE + ELSE TRUE + ENDIF; +a61 : BOOLEAN = + IF s THEN FALSE + ELSE TRUE + ENDIF; +a62 : BOOLEAN = + IF s THEN s + ELSE a61 + ENDIF; +a65 : BOOLEAN = + IF t THEN FALSE + ELSE TRUE + ENDIF; +a67 : BOOLEAN = + IF u THEN FALSE + ELSE TRUE + ENDIF; +a73 : BOOLEAN = + IF p THEN q + ELSE FALSE + ENDIF; +a74 : BOOLEAN = + IF q THEN p + ELSE FALSE + ENDIF; +a77 : BOOLEAN = + IF r THEN TRUE + ELSE s + ENDIF; +a78 : BOOLEAN = + IF s THEN TRUE + ELSE r + ENDIF; +a81 : BOOLEAN = + IF t THEN u + ELSE a67 + ENDIF; +a82 : BOOLEAN = + IF u THEN t + ELSE a65 + ENDIF; +a88 : BOOLEAN = + IF q THEN r + ELSE FALSE + ENDIF; +a89 : BOOLEAN = + IF p THEN a88 + ELSE FALSE + ENDIF; +a92 : BOOLEAN = + IF s THEN TRUE + ELSE t + ENDIF; +a94 : BOOLEAN = + IF t THEN TRUE + ELSE u + ENDIF; +a95 : BOOLEAN = + IF s THEN TRUE + ELSE a94 + ENDIF; +a105 : BOOLEAN = + IF t THEN u + ELSE FALSE + ENDIF; +a111 : BOOLEAN = + IF p THEN q + ELSE TRUE + ENDIF; +a112 : BOOLEAN = + IF q THEN r + ELSE TRUE + ENDIF; +a114 : BOOLEAN = + IF p THEN r + ELSE TRUE + ENDIF; +a116 : BOOLEAN = + IF s THEN t + ELSE a65 + ENDIF; +a121 : BOOLEAN = + IF a46 THEN a41 + ELSE TRUE + ENDIF; +a126 : BOOLEAN = + IF a59 THEN a61 + ELSE + IF a61 THEN FALSE + ELSE TRUE + ENDIF + ENDIF; +a130 : BOOLEAN = + IF q THEN TRUE + ELSE r + ENDIF; +a132 : BOOLEAN = + IF p THEN r + ELSE FALSE + ENDIF; +a133 : BOOLEAN = + IF a73 THEN TRUE + ELSE a132 + ENDIF; +a138 : BOOLEAN = + IF a92 THEN + IF s THEN TRUE + ELSE u + ENDIF + ELSE FALSE + ENDIF; +a143 : BOOLEAN = + IF a114 THEN a112 + ELSE FALSE + ENDIF; +a145 : BOOLEAN = + IF + IF + IF p THEN TRUE + ELSE q + ENDIF THEN r + ELSE TRUE + ENDIF THEN a143 + ELSE + IF a143 THEN FALSE + ELSE TRUE + ENDIF + ENDIF; +a147 : BOOLEAN = + IF s THEN t + ELSE TRUE + ENDIF; +a148 : BOOLEAN = + IF s THEN u + ELSE TRUE + ENDIF; +a149 : BOOLEAN = + IF a147 THEN TRUE + ELSE a148 + ENDIF; +a153 : BOOLEAN = + IF a73 THEN r + ELSE TRUE + ENDIF; +a154 : BOOLEAN = + IF a114 THEN TRUE + ELSE a112 + ENDIF; +a158 : BOOLEAN = + IF a147 THEN a148 + ELSE FALSE + ENDIF; +a162 : BOOLEAN = + IF p THEN a112 + ELSE TRUE + ENDIF; +a167 : BOOLEAN = + IF a46 THEN TRUE + ELSE a59 + ENDIF; +a171 : BOOLEAN = + IF a61 THEN a65 + ELSE FALSE + ENDIF; +a176 : BOOLEAN = + IF p THEN q + ELSE r + ENDIF; +a178 : BOOLEAN = + IF p THEN a46 + ELSE a59 + ENDIF; +a183 : BOOLEAN = + IF s THEN a65 + ELSE + IF a65 THEN FALSE + ELSE TRUE + ENDIF + ENDIF; +a187 : BOOLEAN = + IF a41 THEN TRUE + ELSE q + ENDIF; +a192 : BOOLEAN = + IF + IF r THEN s + ELSE FALSE + ENDIF THEN TRUE + ELSE + IF a59 THEN t + ELSE FALSE + ENDIF + ENDIF; +a197 : BOOLEAN = + IF a111 THEN + IF a41 THEN r + ELSE TRUE + ENDIF + ELSE FALSE + ENDIF; +a200 : BOOLEAN = + IF a49 THEN TRUE + ELSE a171 + ENDIF; +a204 : BOOLEAN = + IF p THEN q + ELSE a46 + ENDIF; +a205 : BOOLEAN = + IF q THEN p + ELSE TRUE + ENDIF; +a206 : BOOLEAN = + IF a111 THEN a205 + ELSE FALSE + ENDIF; +a210 : BOOLEAN = + IF p THEN a46 + ELSE TRUE + ENDIF; +a214 : BOOLEAN = + IF a73 THEN FALSE + ELSE TRUE + ENDIF; +a221 : BOOLEAN = + IF + IF p THEN a46 + ELSE FALSE + ENDIF THEN r + ELSE TRUE + ENDIF; +a225 : BOOLEAN = + IF a187 THEN a132 + ELSE TRUE + ENDIF; +a228 : BOOLEAN = + IF q THEN r + ELSE a59 + ENDIF; +a231 : BOOLEAN = + IF a204 THEN r + ELSE a59 + ENDIF; +a237 : BOOLEAN = + IF q THEN a132 + ELSE + IF a41 THEN s + ELSE FALSE + ENDIF + ENDIF; +a288 : BOOLEAN = + IF + IF + IF p THEN a41 + ELSE a42 + ENDIF THEN FALSE + ELSE TRUE + ENDIF THEN + IF + IF a45 THEN + IF + IF q THEN TRUE + ELSE a46 + ENDIF THEN + IF + IF r THEN r + ELSE TRUE + ENDIF THEN + IF + IF a49 THEN s + ELSE TRUE + ENDIF THEN + IF u THEN + IF u THEN TRUE + ELSE v + ENDIF + ELSE TRUE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF a58 THEN + IF + IF r THEN r + ELSE a59 + ENDIF THEN a62 + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF a45 THEN + IF a62 THEN + IF + IF t THEN t + ELSE a65 + ENDIF THEN + IF a67 THEN a67 + ELSE + IF a67 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF a73 THEN a74 + ELSE + IF a74 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF a77 THEN a78 + ELSE + IF a78 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF a81 THEN a82 + ELSE + IF a82 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF + IF a73 THEN r + ELSE FALSE + ENDIF THEN a89 + ELSE + IF a89 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF a92 THEN TRUE + ELSE u + ENDIF THEN a95 + ELSE + IF a95 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF + IF p THEN p + ELSE FALSE + ENDIF THEN p + ELSE a41 + ENDIF THEN + IF + IF + IF q THEN TRUE + ELSE q + ENDIF THEN q + ELSE a46 + ENDIF THEN + IF + IF + IF r THEN a77 + ELSE FALSE + ENDIF THEN r + ELSE a59 + ENDIF THEN + IF + IF t THEN TRUE + ELSE a105 + ENDIF THEN t + ELSE a65 + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF a58 THEN + IF + IF + IF + IF a111 THEN a112 + ELSE FALSE + ENDIF THEN a114 + ELSE TRUE + ENDIF THEN + IF + IF a116 THEN a81 + ELSE FALSE + ENDIF THEN + IF s THEN u + ELSE a67 + ENDIF + ELSE TRUE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF a111 THEN a121 + ELSE + IF a121 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF r THEN s + ELSE a61 + ENDIF THEN a126 + ELSE + IF a126 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF + IF p THEN a130 + ELSE FALSE + ENDIF THEN a133 + ELSE + IF a133 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF s THEN TRUE + ELSE a105 + ENDIF THEN a138 + ELSE + IF a138 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF a145 THEN + IF + IF s THEN a94 + ELSE TRUE + ENDIF THEN a149 + ELSE + IF a149 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF a153 THEN a154 + ELSE + IF a154 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF s THEN a105 + ELSE TRUE + ENDIF THEN a158 + ELSE + IF a158 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF a153 THEN a162 + ELSE + IF a162 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF a42 THEN p + ELSE a41 + ENDIF THEN + IF + IF + IF a88 THEN FALSE + ELSE TRUE + ENDIF THEN a167 + ELSE + IF a167 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF a92 THEN FALSE + ELSE TRUE + ENDIF THEN a171 + ELSE + IF a171 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF + IF a176 THEN FALSE + ELSE TRUE + ENDIF THEN a178 + ELSE + IF a178 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF a116 THEN FALSE + ELSE TRUE + ENDIF THEN a183 + ELSE + IF a183 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF a111 THEN a187 + ELSE + IF a187 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF r THEN s + ELSE t + ENDIF THEN a192 + ELSE + IF a192 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF a176 THEN a197 + ELSE + IF a197 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF a116 THEN a200 + ELSE + IF a200 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF a204 THEN a206 + ELSE + IF a206 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF a111 THEN TRUE + ELSE a205 + ENDIF THEN + IF + IF a46 THEN TRUE + ELSE + IF + IF a210 THEN p + ELSE FALSE + ENDIF THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF a210 THEN a214 + ELSE + IF a214 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF a145 THEN + IF + IF a162 THEN a153 + ELSE + IF a153 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF p THEN a130 + ELSE TRUE + ENDIF THEN a221 + ELSE + IF a221 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF p THEN a112 + ELSE FALSE + ENDIF THEN a225 + ELSE + IF a225 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF p THEN a228 + ELSE + IF a228 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN a231 + ELSE + IF a231 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF p THEN a88 + ELSE + IF a46 THEN s + ELSE FALSE + ENDIF + ENDIF THEN a237 + ELSE + IF a237 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF P1 THEN + IF P2 THEN TRUE + ELSE P3 + ENDIF + ELSE + IF P3 THEN TRUE + ELSE P4 + ENDIF + ENDIF THEN + IF + IF P3 THEN + IF P6 THEN FALSE + ELSE TRUE + ENDIF + ELSE + IF P4 THEN P1 + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF P2 THEN P5 + ELSE FALSE + ENDIF THEN FALSE + ELSE TRUE + ENDIF THEN + IF P2 THEN P5 + ELSE TRUE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF P3 THEN P6 + ELSE TRUE + ENDIF THEN FALSE + ELSE TRUE + ENDIF + ELSE TRUE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF; +QUERY a288; diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index aa99c70c4..c5a2bb609 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -15,18 +15,42 @@ #include +#include "expr/node_manager.h" #include "expr/node.h" using namespace CVC4; +using namespace std; class NodeBlack : public CxxTest::TestSuite { +private: + + NodeManagerScope *d_scope; + NodeManager *d_nm; + public: - void testNull() { - Node::null(); + void setUp() { + d_nm = new NodeManager(); + d_scope = new NodeManagerScope(d_nm); + } + + void tearDown(){ + delete d_nm; + delete d_scope; } - void testCopyCtor() { - Node e(Node::null()); + void testEqExpr(){ + /*Node eqExpr(const Node& right) const;*/ + Node left = d_nm->mkNode(TRUE); + Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + + Node eq = left.eqExpr(right); + + Node first = *(eq.begin()); + Node second = *(eq.begin()++); + + TS_ASSERT(first.getKind() == NULL); + TS_ASSERT(second.getKind() == NULL); } + };