diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 2 | ||||
-rw-r--r-- | test/unit/expr/attribute_white.h | 98 | ||||
-rw-r--r-- | test/unit/theory/theory_arith_white.h | 2 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 8 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 6 | ||||
-rw-r--r-- | test/unit/theory/theory_uf_tim_white.h | 2 |
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()); } |