diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/expr/expr_black.h | 414 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 40 | ||||
-rw-r--r-- | test/unit/expr/node_builder_black.h | 21 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 4 |
5 files changed, 448 insertions, 32 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 3d9e65070..0b40698cd 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -1,5 +1,6 @@ # All unit tests UNIT_TESTS = \ + expr/expr_black \ expr/node_white \ expr/node_black \ expr/kind_black \ diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h new file mode 100644 index 000000000..b08b5c6aa --- /dev/null +++ b/test/unit/expr/expr_black.h @@ -0,0 +1,414 @@ +/********************* */ +/** expr_black.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Black box testing of CVC4::Expr. + **/ + +#include <cxxtest/TestSuite.h> + +#include <sstream> +#include <string> + +#include "expr/expr_manager.h" +#include "expr/expr.h" +#include "util/Assert.h" +#include "util/exception.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace std; + +class ExprBlack : public CxxTest::TestSuite { +private: + + ExprManager* d_em; + + Expr* a; + Expr* b; + Expr* c; + Expr* mult; + Expr* plus; + Expr* d; + Expr* null; + + Expr* i1; + Expr* i2; + Expr* r1; + Expr* r2; + +public: + + void setUp() { + try { + d_em = new ExprManager; + + a = new Expr(d_em->mkVar(d_em->booleanType(), "a")); + b = new Expr(d_em->mkVar(d_em->booleanType(), "b")); + c = new Expr(d_em->mkExpr(MULT, *a, *b)); + mult = new Expr(d_em->mkConst(MULT)); + plus = new Expr(d_em->mkConst(PLUS)); + d = new Expr(d_em->mkExpr(APPLY_UF, *plus, *b, *c)); + null = new Expr; + + i1 = new Expr(d_em->mkConst(Integer("0"))); + i2 = new Expr(d_em->mkConst(Integer(23))); + r1 = new Expr(d_em->mkConst(Rational(1, 5))); + r2 = new Expr(d_em->mkConst(Rational("0"))); + } catch(Exception e) { + cerr << "Exception during setUp():" << endl << e; + throw; + } + } + + void tearDown() { + try { + delete r2; + delete r1; + delete i2; + delete i1; + + delete null; + delete d; + delete plus; + delete mult; + delete c; + delete b; + delete a; + + delete d_em; + } catch(Exception e) { + cerr << "Exception during tearDown():" << endl << e; + throw; + } + } + + void testDefaultCtor() { + /* Expr(); */ + Expr e; + TS_ASSERT(e.isNull()); + } + + void testCtors() { + TS_ASSERT(!a->isNull()); + TS_ASSERT(!b->isNull()); + + /* Expr(); */ + Expr e; + TS_ASSERT(e.isNull()); + + /* Expr(const Expr& e) */ + Expr e2(e); + TS_ASSERT(e == e2); + TS_ASSERT(e2 == e); + TS_ASSERT(!(e2 < e)); + TS_ASSERT(!(e < e2)); + TS_ASSERT(e.isNull()); + TS_ASSERT(e2.isNull()); + Expr f = d_em->mkExpr(PLUS, *a, *b); + Expr f2 = f; + TS_ASSERT(!f.isNull()); + TS_ASSERT(!f2.isNull()); + TS_ASSERT(f == f2); + TS_ASSERT(f2 == f); + TS_ASSERT(!(f2 < f)); + TS_ASSERT(!(f < f2)); + TS_ASSERT(f == d_em->mkExpr(PLUS, *a, *b)); + } + + void testAssignment() { + /* Expr& operator=(const Expr& e); */ + Expr e = d_em->mkExpr(PLUS, *a, *b); + Expr f; + TS_ASSERT(f.isNull()); + f = e; + TS_ASSERT(!f.isNull()); + TS_ASSERT(e == f); + TS_ASSERT(f == e); + TS_ASSERT(!(f < e)); + TS_ASSERT(!(e < f)); + TS_ASSERT(f == d_em->mkExpr(PLUS, *a, *b)); + } + + void testEquality() { + /* bool operator==(const Expr& e) const; */ + /* bool operator!=(const Expr& e) const; */ + + TS_ASSERT(*a == *a); + TS_ASSERT(*b == *b); + TS_ASSERT(!(*a != *a)); + TS_ASSERT(!(*b != *b)); + + TS_ASSERT(*a != *b); + TS_ASSERT(*b != *a); + TS_ASSERT(!(*a == *b)); + TS_ASSERT(!(*b == *a)); + } + + void testComparison() { + /* bool operator<(const Expr& e) const; */ + + TS_ASSERT(*null < *a); + TS_ASSERT(*null < *b); + TS_ASSERT(*null < *c); + TS_ASSERT(*null < *d); + TS_ASSERT(*null < *plus); + TS_ASSERT(*null < *mult); + TS_ASSERT(*null < *i1); + TS_ASSERT(*null < *i2); + TS_ASSERT(*null < *r1); + TS_ASSERT(*null < *r2); + + TS_ASSERT(*a < *b); + TS_ASSERT(*a < *c); + TS_ASSERT(*a < *d); + TS_ASSERT(!(*b < *a)); + TS_ASSERT(!(*c < *a)); + TS_ASSERT(!(*d < *a)); + + TS_ASSERT(*b < *c); + TS_ASSERT(*b < *d); + TS_ASSERT(!(*c < *b)); + TS_ASSERT(!(*d < *b)); + + TS_ASSERT(*c < *d); + TS_ASSERT(!(*d < *c)); + + TS_ASSERT(*mult < *c); + TS_ASSERT(*mult < *d); + TS_ASSERT(*plus < *d); + TS_ASSERT(!(*c < *mult)); + TS_ASSERT(!(*d < *mult)); + TS_ASSERT(!(*d < *plus)); + + TS_ASSERT(!(*null < *null)); + TS_ASSERT(!(*a < *a)); + TS_ASSERT(!(*b < *b)); + TS_ASSERT(!(*c < *c)); + TS_ASSERT(!(*plus < *plus)); + TS_ASSERT(!(*mult < *mult)); + TS_ASSERT(!(*d < *d)); + } + + void testGetKind() { + /* Kind getKind() const; */ + + TS_ASSERT(a->getKind() == VARIABLE); + TS_ASSERT(b->getKind() == VARIABLE); + TS_ASSERT(c->getKind() == MULT); + TS_ASSERT(mult->getKind() == BUILTIN); + TS_ASSERT(plus->getKind() == BUILTIN); + TS_ASSERT(d->getKind() == APPLY_UF); + TS_ASSERT(null->getKind() == NULL_EXPR); + + TS_ASSERT(i1->getKind() == CONST_INTEGER); + TS_ASSERT(i2->getKind() == CONST_INTEGER); + TS_ASSERT(r1->getKind() == CONST_RATIONAL); + TS_ASSERT(r2->getKind() == CONST_RATIONAL); + } + + void testGetNumChildren() { + /* size_t getNumChildren() const; */ + + TS_ASSERT(a->getNumChildren() == 0); + TS_ASSERT(b->getNumChildren() == 0); + TS_ASSERT(c->getNumChildren() == 2); + TS_ASSERT(mult->getNumChildren() == 0); + TS_ASSERT(plus->getNumChildren() == 0); + TS_ASSERT(d->getNumChildren() == 2); + TS_ASSERT(null->getNumChildren() == 0); + + TS_ASSERT(i1->getNumChildren() == 0); + TS_ASSERT(i2->getNumChildren() == 0); + TS_ASSERT(r1->getNumChildren() == 0); + TS_ASSERT(r2->getNumChildren() == 0); + } + + void testOperatorFunctions() { + /* bool hasOperator() const; */ + /* Expr getOperator() const; */ + + TS_ASSERT(!a->hasOperator()); + TS_ASSERT(!b->hasOperator()); + TS_ASSERT(c->hasOperator()); + TS_ASSERT(!mult->hasOperator()); + TS_ASSERT(!plus->hasOperator()); + TS_ASSERT(d->hasOperator()); + TS_ASSERT(!null->hasOperator()); + + TS_ASSERT_THROWS(a->getOperator(), IllegalArgumentException); + TS_ASSERT_THROWS(b->getOperator(), IllegalArgumentException); + TS_ASSERT(c->getOperator() == *mult); + TS_ASSERT_THROWS(plus->getOperator(), IllegalArgumentException); + TS_ASSERT_THROWS(mult->getOperator(), IllegalArgumentException); + TS_ASSERT(d->getOperator() == *plus); + TS_ASSERT_THROWS(null->getOperator(), IllegalArgumentException); + } + + void testGetType() { + /* Type* getType() const; */ + + TS_ASSERT(a->getType() == d_em->booleanType()); + TS_ASSERT(b->getType() == d_em->booleanType()); + TS_ASSERT(c->getType() == NULL); + TS_ASSERT(mult->getType() == NULL); + TS_ASSERT(plus->getType() == NULL); + TS_ASSERT(d->getType() == NULL); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(null->getType(), AssertionException); +#endif /* CVC4_ASSERTIONS */ + + TS_ASSERT(i1->getType() == NULL); + TS_ASSERT(i2->getType() == NULL); + TS_ASSERT(r1->getType() == NULL); + TS_ASSERT(r2->getType() == NULL); + } + + void testToString() { + /* std::string toString() const; */ + + TS_ASSERT(a->toString() == "a"); + TS_ASSERT(b->toString() == "b"); + TS_ASSERT(c->toString() == "(MULT a b)"); + TS_ASSERT(mult->toString() == "(BUILTIN MULT)"); + TS_ASSERT(plus->toString() == "(BUILTIN PLUS)"); + TS_ASSERT(d->toString() == "(APPLY_UF (BUILTIN PLUS) b (MULT a b))"); + TS_ASSERT(null->toString() == "null"); + + TS_ASSERT(i1->toString() == "(CONST_INTEGER 0)"); + TS_ASSERT(i2->toString() == "(CONST_INTEGER 23)"); + TS_ASSERT(r1->toString() == "(CONST_RATIONAL 1/5)"); + TS_ASSERT(r2->toString() == "(CONST_RATIONAL 0)"); + } + + void testToStream() { + /* void toStream(std::ostream& out) const; */ + + stringstream sa, sb, sc, smult, splus, sd, snull; + stringstream si1, si2, sr1, sr2; + a->toStream(sa); + b->toStream(sb); + c->toStream(sc); + mult->toStream(smult); + plus->toStream(splus); + d->toStream(sd); + null->toStream(snull); + + i1->toStream(si1); + i2->toStream(si2); + r1->toStream(sr1); + r2->toStream(sr2); + + TS_ASSERT(sa.str() == "a"); + TS_ASSERT(sb.str() == "b"); + TS_ASSERT(sc.str() == "(MULT a b)"); + TS_ASSERT(smult.str() == "(BUILTIN MULT)"); + TS_ASSERT(splus.str() == "(BUILTIN PLUS)"); + TS_ASSERT(sd.str() == "(APPLY_UF (BUILTIN PLUS) b (MULT a b))"); + TS_ASSERT(snull.str() == "null"); + + TS_ASSERT(si1.str() == "(CONST_INTEGER 0)"); + TS_ASSERT(si2.str() == "(CONST_INTEGER 23)"); + TS_ASSERT(sr1.str() == "(CONST_RATIONAL 1/5)"); + TS_ASSERT(sr2.str() == "(CONST_RATIONAL 0)"); + } + + void testIsNull() { + /* bool isNull() const; */ + + TS_ASSERT(!a->isNull()); + TS_ASSERT(!b->isNull()); + TS_ASSERT(!c->isNull()); + TS_ASSERT(!mult->isNull()); + TS_ASSERT(!plus->isNull()); + TS_ASSERT(!d->isNull()); + TS_ASSERT(null->isNull()); + } + + void testIsConst() { + /* bool isConst() const; */ + + TS_ASSERT(!a->isConst()); + TS_ASSERT(!b->isConst()); + TS_ASSERT(!c->isConst()); + TS_ASSERT(mult->isConst()); + TS_ASSERT(plus->isConst()); + TS_ASSERT(!d->isConst()); + TS_ASSERT(!null->isConst()); + } + + void testIsAtomic() { + /* bool isAtomic() const; */ + + TS_ASSERT(a->isAtomic()); + TS_ASSERT(b->isAtomic()); + TS_ASSERT(c->isAtomic()); + TS_ASSERT(mult->isAtomic()); + TS_ASSERT(plus->isAtomic()); + TS_ASSERT(d->isAtomic()); + TS_ASSERT(!null->isAtomic()); + + TS_ASSERT(i1->isAtomic()); + TS_ASSERT(i2->isAtomic()); + TS_ASSERT(r1->isAtomic()); + TS_ASSERT(r2->isAtomic()); + + Expr x = d_em->mkExpr(AND, *a, *b); + Expr y = d_em->mkExpr(XOR, *a, *b, *c); + Expr z = d_em->mkExpr(IFF, x, y); + + TS_ASSERT(!x.isAtomic()); + TS_ASSERT(!y.isAtomic()); + TS_ASSERT(!z.isAtomic()); + } + + void testGetConst() { + /* template <class T> + const T& getConst() const; */ + + TS_ASSERT_THROWS(a->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT_THROWS(b->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT_THROWS(c->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT(mult->getConst<Kind>() == MULT); + TS_ASSERT_THROWS(mult->getConst<Integer>(), IllegalArgumentException); + TS_ASSERT(plus->getConst<Kind>() == PLUS); + TS_ASSERT_THROWS(plus->getConst<Rational>(), IllegalArgumentException); + TS_ASSERT_THROWS(d->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT_THROWS(null->getConst<Kind>(), IllegalArgumentException); + + TS_ASSERT(i1->getConst<Integer>() == 0); + TS_ASSERT(i2->getConst<Integer>() == 23); + TS_ASSERT(r1->getConst<Rational>() == Rational(1, 5)); + TS_ASSERT(r2->getConst<Rational>() == Rational("0")); + + TS_ASSERT_THROWS(i1->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT_THROWS(i2->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT_THROWS(r1->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT_THROWS(r2->getConst<Kind>(), IllegalArgumentException); + } + + void testGetExprManager() { + /* ExprManager* getExprManager() const; */ + + TS_ASSERT(a->getExprManager() == d_em); + TS_ASSERT(b->getExprManager() == d_em); + TS_ASSERT(c->getExprManager() == d_em); + TS_ASSERT(mult->getExprManager() == d_em); + TS_ASSERT(plus->getExprManager() == d_em); + TS_ASSERT(d->getExprManager() == d_em); + TS_ASSERT(null->getExprManager() == NULL); + + TS_ASSERT(i1->getExprManager() == d_em); + TS_ASSERT(i2->getExprManager() == d_em); + TS_ASSERT(r1->getExprManager() == d_em); + TS_ASSERT(r2->getExprManager() == d_em); + } +}; diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index c92ea31f5..0b46b06ce 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -174,8 +174,8 @@ public: #endif /* CVC4_ASSERTIONS */ //Basic access check - Node tb = d_nodeManager->mkNode(TRUE); - Node eb = d_nodeManager->mkNode(FALSE); + Node tb = d_nodeManager->mkConst(true); + Node eb = d_nodeManager->mkConst(false); Node cnd = d_nodeManager->mkNode(XOR, tb, eb); Node ite = cnd.iteNode(tb, eb); @@ -232,7 +232,7 @@ public: */ // simple test of descending descendant property - Node child = d_nodeManager->mkNode(TRUE); + Node child = d_nodeManager->mkConst(true); Node parent = d_nodeManager->mkNode(NOT, child); TS_ASSERT(child < parent); @@ -259,8 +259,8 @@ public: void testEqNode() { /* Node eqNode(const Node& right) const; */ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, d_nodeManager->mkNode(FALSE)); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false)); Node eq = left.eqNode(right); TS_ASSERT(EQUAL == eq.getKind()); @@ -273,7 +273,7 @@ public: void testNotNode() { /* Node notNode() const; */ - Node child = d_nodeManager->mkNode(TRUE); + Node child = d_nodeManager->mkConst(true); Node parent = child.notNode(); TS_ASSERT(NOT == parent.getKind()); @@ -285,8 +285,8 @@ public: void testAndNode() { /*Node andNode(const Node& right) const;*/ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.andNode(right); @@ -301,8 +301,8 @@ public: void testOrNode() { /*Node orNode(const Node& right) const;*/ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.orNode(right); @@ -321,8 +321,8 @@ public: Node b = d_nodeManager->mkVar(); Node cnd = d_nodeManager->mkNode(PLUS, a, b); - Node thenBranch = d_nodeManager->mkNode(TRUE); - Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkNode(FALSE)); + Node thenBranch = d_nodeManager->mkConst(true); + Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false)); Node ite = cnd.iteNode(thenBranch, elseBranch); TS_ASSERT(ITE == ite.getKind()); @@ -336,8 +336,8 @@ public: void testIffNode() { /* Node iffNode(const Node& right) const; */ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.iffNode(right); @@ -351,8 +351,8 @@ public: void testImpNode() { /* Node impNode(const Node& right) const; */ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.impNode(right); @@ -365,8 +365,8 @@ public: void testXorNode() { /*Node xorNode(const Node& right) const;*/ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.xorNode(right); @@ -422,7 +422,7 @@ public: void testNaryExpForSize(Kind k, int N) { NodeBuilder<> nbz(k); - Node trueNode = d_nodeManager->mkNode(TRUE); + Node trueNode = d_nodeManager->mkConst(true); for(int i = 0; i < N; ++i) { nbz << trueNode; } @@ -433,7 +433,7 @@ public: void testNumChildren() { /*inline size_t getNumChildren() const;*/ - Node trueNode = d_nodeManager->mkNode(TRUE); + Node trueNode = d_nodeManager->mkConst(true); //test 0 TS_ASSERT(0 == (Node::null()).getNumChildren()); diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index cae2e0637..cfef88df7 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -57,7 +57,7 @@ public: template <unsigned N> void push_back(NodeBuilder<N>& nb, int n){ for(int i = 0; i < n; ++i){ - nb << d_nm->mkNode(TRUE); + nb << d_nm->mkConst(true); } } @@ -293,8 +293,8 @@ public: */ NodeBuilder<> arr(specKind); - Node i_0 = d_nm->mkNode(FALSE); - Node i_2 = d_nm->mkNode(TRUE); + Node i_0 = d_nm->mkConst(false); + Node i_2 = d_nm->mkConst(true); Node i_K = d_nm->mkNode(NOT, i_0); #ifdef CVC4_DEBUG @@ -318,7 +318,7 @@ public: TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); for(int i = 3; i < K; ++i) { - TS_ASSERT_EQUALS(arr[i], d_nm->mkNode(TRUE)); + TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true)); } arr << i_K; @@ -326,7 +326,7 @@ public: TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); for(int i = 3; i < K; ++i) { - TS_ASSERT_EQUALS(arr[i], d_nm->mkNode(TRUE)); + TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true)); } TS_ASSERT_EQUALS(arr[K], i_K); @@ -401,7 +401,7 @@ public: TS_ASSERT_EQUALS(modified.getKind(), specKind); NodeBuilder<> nb(specKind); - nb << d_nm->mkNode(TRUE) << d_nm->mkNode(FALSE); + nb << d_nm->mkConst(true) << d_nm->mkConst(false); Node n = nb;// avoid warning on clear() nb.clear(PLUS); @@ -423,10 +423,10 @@ public: #endif /* CVC4_ASSERTIONS */ NodeBuilder<> testMixOrder1; - TS_ASSERT_EQUALS((testMixOrder1 << specKind << d_nm->mkNode(TRUE)).getKind(), + TS_ASSERT_EQUALS((testMixOrder1 << specKind << d_nm->mkConst(true)).getKind(), specKind); NodeBuilder<> testMixOrder2; - TS_ASSERT_EQUALS((testMixOrder2 << d_nm->mkNode(TRUE) << specKind).getKind(), + TS_ASSERT_EQUALS((testMixOrder2 << d_nm->mkConst(true) << specKind).getKind(), specKind); } @@ -539,12 +539,13 @@ public: NodeBuilder<K> a(specKind); NodeBuilder<K> b(specKind); - NodeBuilder<K> c(TRUE); + NodeBuilder<K> c(NOT); string astr, bstr, cstr; stringstream astream, bstream, cstream; push_back(a, K / 2); push_back(b, K / 2); + push_back(c, 1); a.toStream(astream); b.toStream(bstream); @@ -668,7 +669,7 @@ public: // build one-past-the-end for(size_t j = 0; j <= n; ++j) { - b << d_nm->mkNode(TRUE); + b << d_nm->mkConst(true); } } } catch(Exception e) { diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 5941b3e5d..7ffc4193a 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -145,8 +145,8 @@ public: d_scope = new NodeManagerScope(d_nm); d_dummy = new DummyTheory(d_ctxt, d_outputChannel); d_outputChannel.clear(); - atom0 = d_nm->mkNode(kind::TRUE); - atom1 = d_nm->mkNode(kind::FALSE); + atom0 = d_nm->mkConst(true); + atom1 = d_nm->mkConst(false); } void tearDown() { |