theory/theory_rewriter.h
theory/theory_state.cpp
theory/theory_state.h
- theory/theory_test_utils.h
theory/trust_node.cpp
theory/trust_node.h
theory/trust_substitutions.cpp
+++ /dev/null
-/********************* */
-/*! \file theory_test_utils.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King, Morgan Deters, Andrew Reynolds
- ** 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 Common utilities for testing theories
- **
- ** Common utilities for testing theories.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__THEORY__THEORY_TEST_UTILS_H
-#define CVC4__THEORY__THEORY_TEST_UTILS_H
-
-#include <iostream>
-#include <memory>
-#include <utility>
-#include <vector>
-
-#include "expr/node.h"
-#include "theory/interrupted.h"
-#include "theory/output_channel.h"
-#include "util/resource_manager.h"
-#include "util/unsafe_interrupt_exception.h"
-
-namespace CVC4 {
-namespace theory {
-
-/**
- * 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
-};/* enum OutputChannelCallType */
-
-}/* CVC4::theory namespace */
-
-inline std::ostream& operator<<(std::ostream& out, theory::OutputChannelCallType type) {
- switch(type) {
- case theory::CONFLICT: return out << "CONFLICT";
- case theory::PROPAGATE: return out << "PROPAGATE";
- case theory::PROPAGATE_AS_DECISION: return out << "PROPAGATE_AS_DECISION";
- case theory::AUG_LEMMA: return out << "AUG_LEMMA";
- case theory::LEMMA: return out << "LEMMA";
- case theory::EXPLANATION: return out << "EXPLANATION";
- default: return out << "UNDEFINED-OutputChannelCallType!" << int(type);
- }
-}
-
-namespace theory {
-
-class TestOutputChannel : public theory::OutputChannel {
-public:
- TestOutputChannel() {}
- ~TestOutputChannel() override {}
-
- void safePoint(ResourceManager::Resource r) override {}
- void conflict(TNode n) override { push(CONFLICT, n); }
-
- void trustedConflict(TrustNode n) override { push(CONFLICT, n.getNode()); }
-
- bool propagate(TNode n) override {
- push(PROPAGATE, n);
- return true;
- }
-
- void lemma(TNode n, LemmaProperty p) override { push(LEMMA, n); }
-
- void trustedLemma(TrustNode n, 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 << "[TestOutputChannel " << 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 TestOutputChannel */
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__THEORY__THEORY_TEST_UTILS_H */
#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:
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
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)
#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 {
#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 {
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;
#include "theory/bv/bv_solver_lazy.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"
-#include "theory/theory_test_utils.h"
namespace CVC4 {
#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"
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:
{
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;
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);
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);
}
ASSERT_NE(result, result2);
}
+
} // namespace test
} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \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
+++ /dev/null
-/********************* */
-/*! \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();
- }
-};
projects / cvc5.git / commitdiff