diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/test_smt.h | 191 | ||||
| -rw-r--r-- | test/unit/theory/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/unit/theory/evaluator_white.cpp | 1 | ||||
| -rw-r--r-- | test/unit/theory/theory_arith_white.cpp | 3 | ||||
| -rw-r--r-- | test/unit/theory/theory_bv_white.cpp | 1 | ||||
| -rw-r--r-- | test/unit/theory/theory_engine_white.cpp | 84 | ||||
| -rw-r--r-- | test/unit/theory/theory_white.cpp | 130 | ||||
| -rw-r--r-- | test/unit/theory/theory_white.h | 309 |
8 files changed, 334 insertions, 387 deletions
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index f87ec5e64..7aecdd3b2 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -15,14 +15,23 @@ #ifndef CVC4__TEST__UNIT__TEST_SMT_H #define CVC4__TEST__UNIT__TEST_SMT_H +#include "expr/node.h" #include "expr/node_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "test.h" +#include "theory/theory.h" +#include "theory/valuation.h" +#include "util/resource_manager.h" +#include "util/unsafe_interrupt_exception.h" namespace CVC4 { namespace test { +/* -------------------------------------------------------------------------- */ +/* Test fixtures. */ +/* -------------------------------------------------------------------------- */ + class TestSmt : public TestInternal { protected: @@ -53,6 +62,188 @@ class TestSmtNoFinishInit : public TestInternal std::unique_ptr<NodeManager> d_nodeManager; std::unique_ptr<SmtEngine> d_smtEngine; }; + +/* -------------------------------------------------------------------------- */ +/* Helpers. */ +/* -------------------------------------------------------------------------- */ + +/** + * Very basic OutputChannel for testing simple Theory Behaviour. + * Stores a call sequence for the output channel + */ +enum OutputChannelCallType +{ + CONFLICT, + PROPAGATE, + PROPAGATE_AS_DECISION, + AUG_LEMMA, + LEMMA, + EXPLANATION +}; + +inline std::ostream& operator<<(std::ostream& out, OutputChannelCallType type) +{ + switch (type) + { + case CONFLICT: return out << "CONFLICT"; + case PROPAGATE: return out << "PROPAGATE"; + case PROPAGATE_AS_DECISION: return out << "PROPAGATE_AS_DECISION"; + case AUG_LEMMA: return out << "AUG_LEMMA"; + case LEMMA: return out << "LEMMA"; + case EXPLANATION: return out << "EXPLANATION"; + default: return out << "UNDEFINED-OutputChannelCallType!" << int(type); + } +} + +class DummyOutputChannel : public CVC4::theory::OutputChannel +{ + public: + DummyOutputChannel() {} + ~DummyOutputChannel() override {} + + void safePoint(ResourceManager::Resource r) override {} + void conflict(TNode n) override { push(CONFLICT, n); } + + void trustedConflict(theory::TrustNode n) override + { + push(CONFLICT, n.getNode()); + } + + bool propagate(TNode n) override + { + push(PROPAGATE, n); + return true; + } + + void lemma(TNode n, + theory::LemmaProperty p = theory::LemmaProperty::NONE) override + { + push(LEMMA, n); + } + + void trustedLemma(theory::TrustNode n, theory::LemmaProperty p) override + { + push(LEMMA, n.getNode()); + } + + void requirePhase(TNode, bool) override {} + void setIncomplete() override {} + void handleUserAttribute(const char* attr, theory::Theory* t) override {} + + void splitLemma(TNode n, bool removable = false) override { push(LEMMA, n); } + + void clear() { d_callHistory.clear(); } + + Node getIthNode(int i) const + { + Node tmp = (d_callHistory[i]).second; + return tmp; + } + + OutputChannelCallType getIthCallType(int i) const + { + return (d_callHistory[i]).first; + } + + unsigned getNumCalls() const { return d_callHistory.size(); } + + void printIth(std::ostream& os, int i) const + { + os << "[DummyOutputChannel " << i; + os << " " << getIthCallType(i); + os << " " << getIthNode(i) << "]"; + } + + private: + void push(OutputChannelCallType call, TNode n) + { + d_callHistory.push_back(std::make_pair(call, n)); + } + + std::vector<std::pair<enum OutputChannelCallType, Node> > d_callHistory; +}; + +/* -------------------------------------------------------------------------- */ + +class DymmyTheoryRewriter : public theory::TheoryRewriter +{ + public: + theory::RewriteResponse preRewrite(TNode n) override + { + return theory::RewriteResponse(theory::REWRITE_DONE, n); + } + + theory::RewriteResponse postRewrite(TNode n) override + { + return theory::RewriteResponse(theory::REWRITE_DONE, n); + } +}; + +/** Dummy Theory interface. */ +template <theory::TheoryId theoryId> +class DummyTheory : public theory::Theory +{ + public: + DummyTheory(context::Context* ctxt, + context::UserContext* uctxt, + theory::OutputChannel& out, + theory::Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, pnm), + d_state(ctxt, uctxt, valuation) + { + // use a default theory state object + d_theoryState = &d_state; + } + + theory::TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } + + void registerTerm(TNode n) + { + // check that we registerTerm() a term only once + ASSERT_TRUE(d_registered.find(n) == d_registered.end()); + + for (TNode::iterator i = n.begin(); i != n.end(); ++i) + { + // check that registerTerm() is called in reverse topological order + ASSERT_TRUE(d_registered.find(*i) != d_registered.end()); + } + + d_registered.insert(n); + } + + void presolve() override { Unimplemented(); } + void preRegisterTerm(TNode n) override { Unimplemented(); } + void propagate(Effort level) override { Unimplemented(); } + bool preNotifyFact( + TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) override + { + // do not assert to equality engine, since this theory does not use one + return true; + } + theory::TrustNode explain(TNode n) override + { + return theory::TrustNode::null(); + } + Node getValue(TNode n) { return Node::null(); } + std::string identify() const override { return "DummyTheory" + d_id; } + + std::set<Node> d_registered; + + private: + /** Default theory state object */ + theory::TheoryState d_state; + /** + * This fake theory class is equally useful for bool, uf, arith, etc. It + * keeps an identifier to identify itself. + */ + std::string d_id; + /** The theory rewriter for this theory. */ + DymmyTheoryRewriter d_rewriter; +}; + +/* -------------------------------------------------------------------------- */ } // namespace test } // namespace CVC4 #endif diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 32219e232..790857d86 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -27,5 +27,5 @@ cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory) cvc4_add_unit_test_white(theory_sets_type_rules_white theory) cvc4_add_cxx_unit_test_white(theory_strings_skolem_cache_black theory) cvc4_add_cxx_unit_test_white(theory_strings_word_white theory) -cvc4_add_cxx_unit_test_white(theory_white theory) +cvc4_add_unit_test_white(theory_white theory) cvc4_add_unit_test_white(type_enumerator_white theory) diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp index 1ced4a584..29877a2d5 100644 --- a/test/unit/theory/evaluator_white.cpp +++ b/test/unit/theory/evaluator_white.cpp @@ -22,7 +22,6 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/evaluator.h" #include "theory/rewriter.h" -#include "theory/theory_test_utils.h" #include "util/rational.h" namespace CVC4 { diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index 53238ca43..8bdf82622 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers_engine.h" #include "theory/theory.h" #include "theory/theory_engine.h" -#include "theory/theory_test_utils.h" #include "util/rational.h" namespace CVC4 { @@ -103,7 +102,7 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit Context* d_context; UserContext* d_user_context; - TestOutputChannel d_outputChannel; + DummyOutputChannel d_outputChannel; LogicInfo d_logicInfo; Theory::Effort d_level = Theory::EFFORT_FULL; TheoryArith* d_arith; diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index 92e359c8f..c07f2c402 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -24,7 +24,6 @@ #include "theory/bv/bv_solver_lazy.h" #include "theory/theory.h" #include "theory/theory_engine.h" -#include "theory/theory_test_utils.h" namespace CVC4 { diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp index baf8f4d9c..a170f3bbd 100644 --- a/test/unit/theory/theory_engine_white.cpp +++ b/test/unit/theory/theory_engine_white.cpp @@ -29,11 +29,7 @@ #include "test_smt.h" #include "theory/bv/theory_bv_rewrite_rules_normalization.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" -#include "theory/rewriter.h" -#include "theory/theory.h" #include "theory/theory_engine.h" -#include "theory/theory_rewriter.h" -#include "theory/valuation.h" #include "util/integer.h" #include "util/rational.h" @@ -47,65 +43,6 @@ using namespace theory::bv; namespace test { -class FakeTheoryRewriter : public TheoryRewriter -{ - public: - RewriteResponse preRewrite(TNode n) override - { - return RewriteResponse(REWRITE_DONE, n); - } - - RewriteResponse postRewrite(TNode n) override - { - return RewriteResponse(REWRITE_DONE, n); - } -}; - -/** - * Fake Theory interface. Looks like a Theory, but really all it does is note - * when and how rewriting behavior is requested. - */ -template <TheoryId theoryId> -class FakeTheory : public Theory -{ - public: - FakeTheory(context::Context* ctxt, - context::UserContext* uctxt, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, pnm) - { - } - - TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } - - std::string identify() const override { return "Fake" + d_id; } - - void presolve() override { Unimplemented(); } - - void preRegisterTerm(TNode) override { Unimplemented(); } - void registerTerm(TNode) { Unimplemented(); } - void propagate(Theory::Effort) override { Unimplemented(); } - TrustNode explain(TNode) override - { - Unimplemented(); - return TrustNode::null(); - } - Node getValue(TNode n) { return Node::null(); } - - private: - /** - * This fake theory class is equally useful for bool, uf, arith, etc. It - * keeps an identifier to identify itself. - */ - std::string d_id; - - /** The theory rewriter for this theory. */ - FakeTheoryRewriter d_rewriter; -}; - class TestTheoryWhiteEngine : public TestSmt { protected: @@ -120,15 +57,15 @@ class TestTheoryWhiteEngine : public TestSmt { delete d_theoryEngine->d_theoryOut[id]; delete d_theoryEngine->d_theoryTable[id]; - d_theoryEngine->d_theoryOut[id] = NULL; - d_theoryEngine->d_theoryTable[id] = NULL; + d_theoryEngine->d_theoryOut[id] = nullptr; + d_theoryEngine->d_theoryTable[id] = nullptr; } - d_theoryEngine->addTheory<FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN); - d_theoryEngine->addTheory<FakeTheory<THEORY_BOOL> >(THEORY_BOOL); - d_theoryEngine->addTheory<FakeTheory<THEORY_UF> >(THEORY_UF); - d_theoryEngine->addTheory<FakeTheory<THEORY_ARITH> >(THEORY_ARITH); - d_theoryEngine->addTheory<FakeTheory<THEORY_ARRAYS> >(THEORY_ARRAYS); - d_theoryEngine->addTheory<FakeTheory<THEORY_BV> >(THEORY_BV); + d_theoryEngine->addTheory<DummyTheory<THEORY_BUILTIN> >(THEORY_BUILTIN); + d_theoryEngine->addTheory<DummyTheory<THEORY_BOOL> >(THEORY_BOOL); + d_theoryEngine->addTheory<DummyTheory<THEORY_UF> >(THEORY_UF); + d_theoryEngine->addTheory<DummyTheory<THEORY_ARITH> >(THEORY_ARITH); + d_theoryEngine->addTheory<DummyTheory<THEORY_ARRAYS> >(THEORY_ARRAYS); + d_theoryEngine->addTheory<DummyTheory<THEORY_BV> >(THEORY_BV); } Context* d_context; @@ -150,7 +87,7 @@ TEST_F(TestTheoryWhiteEngine, rewriter_simple) Node nExpected = n; Node nOut; - // do a full rewrite; FakeTheory::preRewrite() and FakeTheory::postRewrite() + // do a full rewrite; DummyTheory::preRewrite() and DummyTheory::postRewrite() // assert that the rewrite calls that are made match the expected sequence // set up above nOut = Rewriter::rewrite(n); @@ -197,7 +134,7 @@ TEST_F(TestTheoryWhiteEngine, rewriter_complex) Node nExpected = n; Node nOut; - // do a full rewrite; FakeTheory::preRewrite() and FakeTheory::postRewrite() + // do a full rewrite; DummyTheory::preRewrite() and DummyTheory::postRewrite() // assert that the rewrite calls that are made match the expected sequence // set up above nOut = Rewriter::rewrite(n); @@ -244,5 +181,6 @@ TEST_F(TestTheoryWhiteEngine, rewrite_rules) } ASSERT_NE(result, result2); } + } // namespace test } // namespace CVC4 diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp new file mode 100644 index 000000000..7bf0f2426 --- /dev/null +++ b/test/unit/theory/theory_white.cpp @@ -0,0 +1,130 @@ +/********************* */ +/*! \file theory_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Tim King, Dejan Jovanovic + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of CVC4::theory::Theory. + ** + ** Black box testing of CVC4::theory::Theory. + **/ + +#include <memory> +#include <vector> + +#include "context/context.h" +#include "expr/node.h" +#include "test_smt.h" +#include "theory/theory.h" +#include "theory/theory_engine.h" +#include "util/resource_manager.h" + +namespace CVC4 { + +using namespace theory; +using namespace expr; +using namespace context; + +namespace test { + +class TestTheoryWhite : public TestSmtNoFinishInit +{ + protected: + void SetUp() override + { + TestSmtNoFinishInit::SetUp(); + d_context = d_smtEngine->getContext(); + d_user_context = d_smtEngine->getUserContext(); + d_logicInfo.reset(new LogicInfo()); + d_logicInfo->lock(); + d_smtEngine->finishInit(); + delete d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN]; + delete d_smtEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN]; + d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN] = nullptr; + d_smtEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN] = nullptr; + + d_dummy_theory.reset(new DummyTheory<THEORY_BUILTIN>(d_context, + d_user_context, + d_outputChannel, + Valuation(nullptr), + *d_logicInfo, + nullptr)); + d_outputChannel.clear(); + d_atom0 = d_nodeManager->mkConst(true); + d_atom1 = d_nodeManager->mkConst(false); + } + + Context* d_context; + UserContext* d_user_context; + std::unique_ptr<LogicInfo> d_logicInfo; + DummyOutputChannel d_outputChannel; + std::unique_ptr<DummyTheory<THEORY_BUILTIN>> d_dummy_theory; + Node d_atom0; + Node d_atom1; +}; + +TEST_F(TestTheoryWhite, effort) +{ + Theory::Effort s = Theory::EFFORT_STANDARD; + Theory::Effort f = Theory::EFFORT_FULL; + + ASSERT_TRUE(Theory::standardEffortOnly(s)); + ASSERT_FALSE(Theory::standardEffortOnly(f)); + + ASSERT_FALSE(Theory::fullEffort(s)); + ASSERT_TRUE(Theory::fullEffort(f)); + + ASSERT_TRUE(Theory::standardEffortOrMore(s)); + ASSERT_TRUE(Theory::standardEffortOrMore(f)); +} + +TEST_F(TestTheoryWhite, done) +{ + ASSERT_TRUE(d_dummy_theory->done()); + + d_dummy_theory->assertFact(d_atom0, true); + d_dummy_theory->assertFact(d_atom1, true); + + ASSERT_FALSE(d_dummy_theory->done()); + + d_dummy_theory->check(Theory::EFFORT_FULL); + + ASSERT_TRUE(d_dummy_theory->done()); +} + +TEST_F(TestTheoryWhite, outputChannel_accessors) +{ + /* void setOutputChannel(OutputChannel& out) */ + /* OutputChannel& getOutputChannel() */ + + DummyOutputChannel theOtherChannel; + + ASSERT_EQ(&(d_dummy_theory->getOutputChannel()), &d_outputChannel); + + d_dummy_theory->setOutputChannel(theOtherChannel); + + ASSERT_EQ(&(d_dummy_theory->getOutputChannel()), &theOtherChannel); + + const OutputChannel& oc = d_dummy_theory->getOutputChannel(); + + ASSERT_EQ(&oc, &theOtherChannel); +} + +TEST_F(TestTheoryWhite, outputChannel) +{ + Node n = d_atom0.orNode(d_atom1); + d_outputChannel.lemma(n); + d_outputChannel.split(d_atom0); + Node s = d_atom0.orNode(d_atom0.notNode()); + ASSERT_EQ(d_outputChannel.d_callHistory.size(), 2u); + ASSERT_EQ(d_outputChannel.d_callHistory[0], std::make_pair(LEMMA, n)); + ASSERT_EQ(d_outputChannel.d_callHistory[1], std::make_pair(LEMMA, s)); + d_outputChannel.d_callHistory.clear(); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h deleted file mode 100644 index 5ac316612..000000000 --- a/test/unit/theory/theory_white.h +++ /dev/null @@ -1,309 +0,0 @@ -/********************* */ -/*! \file theory_white.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Andrew Reynolds, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of CVC4::theory::Theory. - ** - ** Black box testing of CVC4::theory::Theory. - **/ - -#include <cxxtest/TestSuite.h> - -#include <memory> -#include <vector> - -#include "context/context.h" -#include "expr/node.h" -#include "expr/node_manager.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/theory.h" -#include "theory/theory_engine.h" -#include "util/resource_manager.h" - -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::expr; -using namespace CVC4::context; -using namespace CVC4::smt; - -using namespace std; - -/** - * Very basic OutputChannel for testing simple Theory Behaviour. - * Stores a call sequence for the output channel - */ -enum OutputChannelCallType{CONFLICT, PROPAGATE, LEMMA, EXPLANATION}; -class TestOutputChannel : public OutputChannel { - public: - TestOutputChannel() {} - ~TestOutputChannel() override {} - - void safePoint(ResourceManager::Resource r) override {} - void conflict(TNode n) override { push(CONFLICT, n); } - - bool propagate(TNode n) override { - push(PROPAGATE, n); - return true; - } - - void lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) override - { - push(LEMMA, n); - } - - void splitLemma(TNode n, bool removable) override { push(LEMMA, n); } - - void requirePhase(TNode, bool) override { Unreachable(); } - void setIncomplete() override { Unreachable(); } - - void clear() { d_callHistory.clear(); } - - Node getIthNode(int i) const { - Node tmp = (d_callHistory[i]).second; - return tmp; - } - - OutputChannelCallType getIthCallType(int i) const { - return (d_callHistory[i]).first; - } - - unsigned getNumCalls() const { return d_callHistory.size(); } - - private: - void push(OutputChannelCallType call, TNode n) { - d_callHistory.push_back(make_pair(call, n)); - } - vector<pair<OutputChannelCallType, Node> > d_callHistory; -}; - -class DummyTheory : public Theory { - public: - set<Node> d_registered; - vector<Node> d_getSequence; - - DummyTheory(Context* ctxt, - UserContext* uctxt, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(theory::THEORY_BUILTIN, - ctxt, - uctxt, - out, - valuation, - logicInfo, - pnm), - d_state(ctxt, uctxt, valuation) - { - // use a default theory state object - d_theoryState = &d_state; - } - - TheoryRewriter* getTheoryRewriter() override { return nullptr; } - - void registerTerm(TNode n) { - // check that we registerTerm() a term only once - TS_ASSERT(d_registered.find(n) == d_registered.end()); - - for(TNode::iterator i = n.begin(); i != n.end(); ++i) { - // check that registerTerm() is called in reverse topological order - TS_ASSERT(d_registered.find(*i) != d_registered.end()); - } - - d_registered.insert(n); - } - - Node getWrapper() { - Node n = get(); - d_getSequence.push_back(n); - return n; - } - - bool doneWrapper() { - return done(); - } - - void presolve() override { Unimplemented(); } - void preRegisterTerm(TNode n) override {} - void propagate(Effort level) override {} - bool preNotifyFact( - TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) override - { - // do not assert to equality engine, since this theory does not use one - return true; - } - TrustNode explain(TNode n) override { return TrustNode::null(); } - Node getValue(TNode n) { return Node::null(); } - string identify() const override { return "DummyTheory"; } - /** Default theory state object */ - TheoryState d_state; -};/* class DummyTheory */ - -class TheoryBlack : public CxxTest::TestSuite { - - Context* d_ctxt; - UserContext* d_uctxt; - NodeManager* d_nm; - ExprManager* d_em; - SmtScope* d_scope; - SmtEngine* d_smt; - LogicInfo* d_logicInfo; - - TestOutputChannel d_outputChannel; - - DummyTheory* d_dummy; - - Node atom0; - Node atom1; - - public: - void setUp() override - { - d_em = new ExprManager(); - d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_nm); - d_ctxt = d_smt->getContext(); - d_uctxt = d_smt->getUserContext(); - d_scope = new SmtScope(d_smt); - d_logicInfo = new LogicInfo(); - d_logicInfo->lock(); - - // Notice that this unit test uses the theory engine of a created SMT - // engine d_smt. We must ensure that d_smt is properly initialized via - // the following call, which constructs its underlying theory engine. - d_smt->finishInit(); - // guard against duplicate statistics assertion errors - delete d_smt->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN]; - delete d_smt->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN]; - d_smt->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN] = NULL; - d_smt->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN] = NULL; - - d_dummy = new DummyTheory(d_ctxt, - d_uctxt, - d_outputChannel, - Valuation(NULL), - *d_logicInfo, - nullptr); - d_outputChannel.clear(); - atom0 = d_nm->mkConst(true); - atom1 = d_nm->mkConst(false); - } - - void tearDown() override - { - atom1 = Node::null(); - atom0 = Node::null(); - delete d_dummy; - delete d_logicInfo; - delete d_scope; - delete d_smt; - delete d_em; - } - - void testEffort(){ - Theory::Effort s = Theory::EFFORT_STANDARD; - Theory::Effort f = Theory::EFFORT_FULL; - - TS_ASSERT( Theory::standardEffortOnly(s)); - TS_ASSERT(!Theory::standardEffortOnly(f)); - - TS_ASSERT(!Theory::fullEffort(s)); - TS_ASSERT( Theory::fullEffort(f)); - - TS_ASSERT( Theory::standardEffortOrMore(s)); - TS_ASSERT( Theory::standardEffortOrMore(f)); - } - - void testDone() { - TS_ASSERT(d_dummy->doneWrapper()); - - d_dummy->assertFact(atom0, true); - d_dummy->assertFact(atom1, true); - - TS_ASSERT(!d_dummy->doneWrapper()); - - d_dummy->check(Theory::EFFORT_FULL); - - TS_ASSERT(d_dummy->doneWrapper()); - } - - // FIXME: move this to theory_engine test? -// void testRegisterTerm() { -// TS_ASSERT(d_dummy->doneWrapper()); - -// TypeNode typeX = d_nm->booleanType(); -// TypeNode typeF = d_nm->mkFunctionType(typeX, typeX); - -// Node x = d_nm->mkVar("x",typeX); -// Node f = d_nm->mkVar("f",typeF); -// Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); -// Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); -// Node f_x_eq_x = f_x.eqNode(x); -// Node x_eq_f_f_x = x.eqNode(f_f_x); - -// d_dummy->assertFact(f_x_eq_x); -// d_dummy->assertFact(x_eq_f_f_x); - -// Node got = d_dummy->getWrapper(); - -// TS_ASSERT_EQUALS(got, f_x_eq_x); - -// TS_ASSERT_EQUALS(5u, d_dummy->d_registered.size()); -// TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end()); -// TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end()); -// TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end()); -// TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end()); -// TS_ASSERT(d_dummy->d_registered.find(d_nm->operatorOf(kind::EQUAL)) != d_dummy->d_registered.end()); -// TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end()); -// TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end()); - -// TS_ASSERT(!d_dummy->doneWrapper()); - -// got = d_dummy->getWrapper(); - -// TS_ASSERT_EQUALS(got, x_eq_f_f_x); - -// TS_ASSERT_EQUALS(7u, d_dummy->d_registered.size()); -// TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end()); -// TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end()); - -// TS_ASSERT(d_dummy->doneWrapper()); -// } - - void testOutputChannelAccessors() { - /* void setOutputChannel(OutputChannel& out) */ - /* OutputChannel& getOutputChannel() */ - - TestOutputChannel theOtherChannel; - - TS_ASSERT_EQUALS(&(d_dummy->getOutputChannel()), &d_outputChannel); - - d_dummy->setOutputChannel(theOtherChannel); - - TS_ASSERT_EQUALS(&(d_dummy->getOutputChannel()), &theOtherChannel); - - const OutputChannel& oc = d_dummy->getOutputChannel(); - - TS_ASSERT_EQUALS(&oc, &theOtherChannel); - } - - void testOutputChannel() { - Node n = atom0.orNode(atom1); - d_outputChannel.lemma(n); - d_outputChannel.split(atom0); - Node s = atom0.orNode(atom0.notNode()); - TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u); - TS_ASSERT_EQUALS(d_outputChannel.d_callHistory[0], make_pair(LEMMA, n)); - TS_ASSERT_EQUALS(d_outputChannel.d_callHistory[1], make_pair(LEMMA, s)); - d_outputChannel.d_callHistory.clear(); - } -}; |