summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--test/regress/Makefile.am3
-rw-r--r--test/regress/Makefile.in3
-rw-r--r--test/regress/boolean.cvc809
-rw-r--r--test/unit/expr/node_black.h32
4 files changed, 841 insertions, 6 deletions
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 <cxxtest/TestSuite.h>
+#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);
}
+
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback