summaryrefslogtreecommitdiff
path: root/test/unit
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit')
-rw-r--r--test/unit/Makefile.am2
-rw-r--r--test/unit/expr/attribute_white.h98
-rw-r--r--test/unit/theory/theory_arith_white.h2
-rw-r--r--test/unit/theory/theory_black.h8
-rw-r--r--test/unit/theory/theory_engine_white.h6
-rw-r--r--test/unit/theory/theory_uf_tim_white.h2
6 files changed, 58 insertions, 60 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 725d4a4bb..eb70935e7 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -172,7 +172,7 @@ nodist_libdummy_la_SOURCES = expr/node_black.cpp
libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
endif
-# synonyms for "check"
+# synonyms for "checK" in this directory in this directory
.PHONY: units test
units test: check
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index a121029f3..3dbee87eb 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -26,6 +26,7 @@
#include "expr/node_manager.h"
#include "expr/attribute.h"
#include "expr/node.h"
+#include "theory/theory.h"
#include "theory/theory_engine.h"
#include "theory/uf/theory_uf.h"
#include "util/Assert.h"
@@ -108,17 +109,11 @@ public:
//TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId);
lastId = attr::LastAttributeId<bool, false>::s_id;
- TS_ASSERT_LESS_THAN(theory::Theory::PreRegisteredAttr::s_id, lastId);
TS_ASSERT_LESS_THAN(TestFlag1::s_id, lastId);
TS_ASSERT_LESS_THAN(TestFlag2::s_id, lastId);
TS_ASSERT_LESS_THAN(TestFlag3::s_id, lastId);
TS_ASSERT_LESS_THAN(TestFlag4::s_id, lastId);
TS_ASSERT_LESS_THAN(TestFlag5::s_id, lastId);
- TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag1::s_id);
- TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag2::s_id);
- TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag3::s_id);
- TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag4::s_id);
- TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag5::s_id);
TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag2::s_id);
TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag3::s_id);
TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag4::s_id);
@@ -131,12 +126,15 @@ public:
TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id);
lastId = attr::LastAttributeId<bool, true>::s_id;
-// TS_ASSERT_LESS_THAN(TheoryEngine::RegisteredAttr::s_id, lastId);
+ TS_ASSERT_LESS_THAN(theory::Asserted::s_id, lastId);
TS_ASSERT_LESS_THAN(TestFlag1cd::s_id, lastId);
TS_ASSERT_LESS_THAN(TestFlag2cd::s_id, lastId);
-// TS_ASSERT_DIFFERS(TheoryEngine::RegisteredAttr::s_id, TestFlag1cd::s_id);
-// TS_ASSERT_DIFFERS(TheoryEngine::RegisteredAttr::s_id, TestFlag2cd::s_id);
+ TS_ASSERT_DIFFERS(theory::Asserted::s_id, TestFlag1cd::s_id);
+ TS_ASSERT_DIFFERS(theory::Asserted::s_id, TestFlag2cd::s_id);
TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id);
+ cout << "A: " << theory::Asserted::s_id << endl;
+ cout << "1: " << TestFlag1cd::s_id << endl;
+ cout << "2: " << TestFlag2cd::s_id << endl;
lastId = attr::LastAttributeId<Node, false>::s_id;
// TS_ASSERT_LESS_THAN(theory::PreRewriteCache::s_id, lastId);
@@ -156,27 +154,27 @@ public:
}
void testCDAttributes() {
- //Debug.on("boolattr");
+ //Debug.on("cdboolattr");
Node a = d_nm->mkVar(*d_booleanType);
Node b = d_nm->mkVar(*d_booleanType);
Node c = d_nm->mkVar(*d_booleanType);
- Debug("boolattr", "get flag 1 on a (should be F)\n");
+ Debug("cdboolattr", "get flag 1 on a (should be F)\n");
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on b (should be F)\n");
+ Debug("cdboolattr", "get flag 1 on b (should be F)\n");
TS_ASSERT(! b.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on c (should be F)\n");
+ Debug("cdboolattr", "get flag 1 on c (should be F)\n");
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
d_ctxt->push(); // level 1
// test that all boolean flags are FALSE to start
- Debug("boolattr", "get flag 1 on a (should be F)\n");
+ Debug("cdboolattr", "get flag 1 on a (should be F)\n");
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on b (should be F)\n");
+ Debug("cdboolattr", "get flag 1 on b (should be F)\n");
TS_ASSERT(! b.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on c (should be F)\n");
+ Debug("cdboolattr", "get flag 1 on c (should be F)\n");
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
// test that they all HAVE the boolean attributes
@@ -186,96 +184,96 @@ public:
// test two-arg version of hasAttribute()
bool bb = false;
- Debug("boolattr", "get flag 1 on a (should be F)\n");
+ Debug("cdboolattr", "get flag 1 on a (should be F)\n");
TS_ASSERT(a.getAttribute(TestFlag1cd(), bb));
TS_ASSERT(! bb);
- Debug("boolattr", "get flag 1 on b (should be F)\n");
+ Debug("cdboolattr", "get flag 1 on b (should be F)\n");
TS_ASSERT(b.getAttribute(TestFlag1cd(), bb));
TS_ASSERT(! bb);
- Debug("boolattr", "get flag 1 on c (should be F)\n");
+ Debug("cdboolattr", "get flag 1 on c (should be F)\n");
TS_ASSERT(c.getAttribute(TestFlag1cd(), bb));
TS_ASSERT(! bb);
// setting boolean flags
- Debug("boolattr", "set flag 1 on a to T\n");
+ Debug("cdboolattr", "set flag 1 on a to T\n");
a.setAttribute(TestFlag1cd(), true);
- Debug("boolattr", "set flag 1 on b to F\n");
+ Debug("cdboolattr", "set flag 1 on b to F\n");
b.setAttribute(TestFlag1cd(), false);
- Debug("boolattr", "set flag 1 on c to F\n");
+ Debug("cdboolattr", "set flag 1 on c to F\n");
c.setAttribute(TestFlag1cd(), false);
- Debug("boolattr", "get flag 1 on a (should be T)\n");
+ Debug("cdbootattr", "get flag 1 on a (should be T)\n");
TS_ASSERT(a.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on b (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on b (should be F)\n");
TS_ASSERT(! b.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on c (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on c (should be F)\n");
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
d_ctxt->push(); // level 2
- Debug("boolattr", "get flag 1 on a (should be T)\n");
+ Debug("cdbootattr", "get flag 1 on a (should be T)\n");
TS_ASSERT(a.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on b (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on b (should be F)\n");
TS_ASSERT(! b.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on c (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on c (should be F)\n");
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
- Debug("boolattr", "set flag 1 on a to F\n");
+ Debug("cdbootattr", "set flag 1 on a to F\n");
a.setAttribute(TestFlag1cd(), false);
- Debug("boolattr", "set flag 1 on b to T\n");
+ Debug("cdbootattr", "set flag 1 on b to T\n");
b.setAttribute(TestFlag1cd(), true);
- Debug("boolattr", "get flag 1 on a (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on a (should be F)\n");
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on b (should be T)\n");
+ Debug("cdbootattr", "get flag 1 on b (should be T)\n");
TS_ASSERT(b.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on c (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on c (should be F)\n");
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
d_ctxt->push(); // level 3
- Debug("boolattr", "get flag 1 on a (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on a (should be F)\n");
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on b (should be T)\n");
+ Debug("cdbootattr", "get flag 1 on b (should be T)\n");
TS_ASSERT(b.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on c (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on c (should be F)\n");
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
- Debug("boolattr", "set flag 1 on c to T\n");
+ Debug("cdbootattr", "set flag 1 on c to T\n");
c.setAttribute(TestFlag1cd(), true);
- Debug("boolattr", "get flag 1 on a (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on a (should be F)\n");
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on b (should be T)\n");
+ Debug("cdbootattr", "get flag 1 on b (should be T)\n");
TS_ASSERT(b.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on c (should be T)\n");
+ Debug("cdbootattr", "get flag 1 on c (should be T)\n");
TS_ASSERT(c.getAttribute(TestFlag1cd()));
d_ctxt->pop(); // level 2
- Debug("boolattr", "get flag 1 on a (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on a (should be F)\n");
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on b (should be T)\n");
+ Debug("cdbootattr", "get flag 1 on b (should be T)\n");
TS_ASSERT(b.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on c (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on c (should be F)\n");
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
d_ctxt->pop(); // level 1
- Debug("boolattr", "get flag 1 on a (should be T)\n");
+ Debug("cdbootattr", "get flag 1 on a (should be T)\n");
TS_ASSERT(a.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on b (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on b (should be F)\n");
TS_ASSERT(! b.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on c (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on c (should be F)\n");
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
d_ctxt->pop(); // level 0
- Debug("boolattr", "get flag 1 on a (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on a (should be F)\n");
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on b (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on b (should be F)\n");
TS_ASSERT(! b.getAttribute(TestFlag1cd()));
- Debug("boolattr", "get flag 1 on c (should be F)\n");
+ Debug("cdbootattr", "get flag 1 on c (should be F)\n");
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
#ifdef CVC4_ASSERTIONS
@@ -284,7 +282,7 @@ public:
}
void testAttributes() {
- //Debug.on("boolattr");
+ //Debug.on("bootattr");
Node a = d_nm->mkVar(*d_booleanType);
Node b = d_nm->mkVar(*d_booleanType);
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 4aee8060f..9de8f94b4 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -96,7 +96,7 @@ public:
d_nm = new NodeManager(d_ctxt);
d_scope = new NodeManagerScope(d_nm);
d_outputChannel.clear();
- d_arith = new TheoryArith(d_ctxt, d_outputChannel);
+ d_arith = new TheoryArith(d_ctxt, d_outputChannel, Valuation(NULL));
preregistered = new std::set<Node>();
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 18408acd3..a362a597c 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -104,8 +104,8 @@ public:
set<Node> d_registered;
vector<Node> d_getSequence;
- DummyTheory(Context* ctxt, OutputChannel& out) :
- Theory(theory::THEORY_BUILTIN, ctxt, out) {
+ DummyTheory(Context* ctxt, OutputChannel& out, Valuation valuation) :
+ Theory(theory::THEORY_BUILTIN, ctxt, out, valuation) {
}
void registerTerm(TNode n) {
@@ -142,7 +142,7 @@ public:
void preRegisterTerm(TNode n) {}
void propagate(Effort level) {}
void explain(TNode n, Effort level) {}
- Node getValue(TNode n, Valuation* valuation) { return Node::null(); }
+ Node getValue(TNode n) { return Node::null(); }
string identify() const { return "DummyTheory"; }
};
@@ -165,7 +165,7 @@ public:
d_ctxt = new Context;
d_nm = new NodeManager(d_ctxt);
d_scope = new NodeManagerScope(d_nm);
- d_dummy = new DummyTheory(d_ctxt, d_outputChannel);
+ d_dummy = new DummyTheory(d_ctxt, d_outputChannel, Valuation(NULL));
d_outputChannel.clear();
atom0 = d_nm->mkConst(true);
atom1 = d_nm->mkConst(false);
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 5915ac1f7..f99698204 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -107,8 +107,8 @@ class FakeTheory : public Theory {
// static std::deque<RewriteItem> s_expected;
public:
- FakeTheory(context::Context* ctxt, OutputChannel& out) :
- Theory(theoryId, ctxt, out)
+ FakeTheory(context::Context* ctxt, OutputChannel& out, Valuation valuation) :
+ Theory(theoryId, ctxt, out, valuation)
{ }
/** Register an expected rewrite call */
@@ -212,7 +212,7 @@ public:
void check(Theory::Effort) { Unimplemented(); }
void propagate(Theory::Effort) { Unimplemented(); }
void explain(TNode, Theory::Effort) { Unimplemented(); }
- Node getValue(TNode n, Valuation* valuation) { return Node::null(); }
+ Node getValue(TNode n) { return Node::null(); }
};/* class FakeTheory */
diff --git a/test/unit/theory/theory_uf_tim_white.h b/test/unit/theory/theory_uf_tim_white.h
index 19b289ae7..1940bc199 100644
--- a/test/unit/theory/theory_uf_tim_white.h
+++ b/test/unit/theory/theory_uf_tim_white.h
@@ -61,7 +61,7 @@ public:
d_nm = new NodeManager(d_ctxt);
d_scope = new NodeManagerScope(d_nm);
d_outputChannel.clear();
- d_euf = new TheoryUFTim(d_ctxt, d_outputChannel);
+ d_euf = new TheoryUFTim(d_ctxt, d_outputChannel, Valuation(NULL));
d_booleanType = new TypeNode(d_nm->booleanType());
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback