From: Morgan Deters Date: Sat, 26 Feb 2011 21:24:18 +0000 (+0000) Subject: Merge from theory-break-dependences branch to break Theory and TheoryEngine dependenc... X-Git-Tag: cvc5-1.0.0~8687 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=edf6aaa87da179948e6b233d16fa37d2aea58bbb;p=cvc5.git Merge from theory-break-dependences branch to break Theory and TheoryEngine dependences; now, if you touch theory_engine.h, only a few things in theory need be recompiled (TheoryEngine, SharedTermManager, .... but no theory implementations), along with the PropEngine and SmtEngine. If you touch a specific theory's .h file, only that theory must be recompiled (along with the TheoryEngine, since it uses traits, and SmtEngine, since it tells the TheoryEngine which theory implementations to use). --- diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index acf0ed5ee..142aef004 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -21,7 +21,10 @@ libtheory_la_SOURCES = \ shared_data.cpp \ rewriter.h \ rewriter_attributes.h \ - rewriter.cpp + rewriter.cpp \ + valuation.h \ + valuation.cpp + nodist_libtheory_la_SOURCES = \ rewriter_tables.h \ theory_traits.h @@ -47,7 +50,7 @@ BUILT_SOURCES = \ CLEANFILES = \ rewriter_tables.h \ - theory_traits.h + theory_traits.h include @top_srcdir@/src/theory/Makefile.subdirs @@ -66,4 +69,3 @@ theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theo $< \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) - \ No newline at end of file diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6084e3463..2100e0b38 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -22,7 +22,7 @@ #include "expr/metakind.h" #include "expr/node_builder.h" -#include "theory/theory_engine.h" +#include "theory/valuation.h" #include "util/rational.h" #include "util/integer.h" @@ -567,7 +567,7 @@ void TheoryArith::propagate(Effort e) { // } } -Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { +Node TheoryArith::getValue(TNode n, Valuation* valuation) { NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { @@ -578,7 +578,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { Node eq = d_removedRows.find(var)->second; Assert(n == eq[0]); Node rhs = eq[1]; - return getValue(rhs, engine); + return getValue(rhs, valuation); } DeltaRational drat = d_partialModel.getAssignment(var); @@ -591,7 +591,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { case kind::EQUAL: // 2 args return nodeManager-> - mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) ); case kind::PLUS: { // 2+ args Rational value = d_constants.d_ZERO; @@ -599,7 +599,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { iend = n.end(); i != iend; ++i) { - value += engine->getValue(*i).getConst(); + value += valuation->getValue(*i).getConst(); } return nodeManager->mkConst(value); } @@ -610,7 +610,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { iend = n.end(); i != iend; ++i) { - value *= engine->getValue(*i).getConst(); + value *= valuation->getValue(*i).getConst(); } return nodeManager->mkConst(value); } @@ -624,24 +624,24 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { Unreachable(); case kind::DIVISION: // 2 args - return nodeManager->mkConst( engine->getValue(n[0]).getConst() / - engine->getValue(n[1]).getConst() ); + return nodeManager->mkConst( valuation->getValue(n[0]).getConst() / + valuation->getValue(n[1]).getConst() ); case kind::LT: // 2 args - return nodeManager->mkConst( engine->getValue(n[0]).getConst() < - engine->getValue(n[1]).getConst() ); + return nodeManager->mkConst( valuation->getValue(n[0]).getConst() < + valuation->getValue(n[1]).getConst() ); case kind::LEQ: // 2 args - return nodeManager->mkConst( engine->getValue(n[0]).getConst() <= - engine->getValue(n[1]).getConst() ); + return nodeManager->mkConst( valuation->getValue(n[0]).getConst() <= + valuation->getValue(n[1]).getConst() ); case kind::GT: // 2 args - return nodeManager->mkConst( engine->getValue(n[0]).getConst() > - engine->getValue(n[1]).getConst() ); + return nodeManager->mkConst( valuation->getValue(n[0]).getConst() > + valuation->getValue(n[1]).getConst() ); case kind::GEQ: // 2 args - return nodeManager->mkConst( engine->getValue(n[0]).getConst() >= - engine->getValue(n[1]).getConst() ); + return nodeManager->mkConst( valuation->getValue(n[0]).getConst() >= + valuation->getValue(n[1]).getConst() ); default: Unhandled(n.getKind()); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 60d24708c..e29054c16 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -152,7 +152,7 @@ public: void notifyEq(TNode lhs, TNode rhs); - Node getValue(TNode n, TheoryEngine* engine); + Node getValue(TNode n, Valuation* valuation); void shutdown(){ } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index ad7550a6c..d45320266 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -18,7 +18,7 @@ #include "theory/arrays/theory_arrays.h" -#include "theory/theory_engine.h" +#include "theory/valuation.h" #include "expr/kind.h" @@ -60,7 +60,7 @@ void TheoryArrays::check(Effort e) { Debug("arrays") << "TheoryArrays::check(): done" << endl; } -Node TheoryArrays::getValue(TNode n, TheoryEngine* engine) { +Node TheoryArrays::getValue(TNode n, Valuation* valuation) { NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { @@ -70,7 +70,7 @@ Node TheoryArrays::getValue(TNode n, TheoryEngine* engine) { case kind::EQUAL: // 2 args return nodeManager-> - mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) ); default: Unhandled(n.getKind()); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index d3472f952..5a63fd26c 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -43,7 +43,7 @@ public: void check(Effort e); void propagate(Effort e) { } void explain(TNode n) { } - Node getValue(TNode n, TheoryEngine* engine); + Node getValue(TNode n, Valuation* valuation); void shutdown() { } std::string identify() const { return std::string("TheoryArrays"); } };/* class TheoryArrays */ diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index f8071d45d..44f5d60a6 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -18,13 +18,13 @@ #include "theory/theory.h" #include "theory/booleans/theory_bool.h" -#include "theory/theory_engine.h" +#include "theory/valuation.h" namespace CVC4 { namespace theory { namespace booleans { -Node TheoryBool::getValue(TNode n, TheoryEngine* engine) { +Node TheoryBool::getValue(TNode n, Valuation* valuation) { NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { @@ -38,14 +38,14 @@ Node TheoryBool::getValue(TNode n, TheoryEngine* engine) { Unreachable(); case kind::NOT: // 1 arg - return nodeManager->mkConst(! engine->getValue(n[0]).getConst()); + return nodeManager->mkConst(! valuation->getValue(n[0]).getConst()); case kind::AND: { // 2+ args for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { - if(! engine->getValue(*i).getConst()) { + if(! valuation->getValue(*i).getConst()) { return nodeManager->mkConst(false); } } @@ -53,19 +53,19 @@ Node TheoryBool::getValue(TNode n, TheoryEngine* engine) { } case kind::IFF: // 2 args - return nodeManager->mkConst( engine->getValue(n[0]).getConst() == - engine->getValue(n[1]).getConst() ); + return nodeManager->mkConst( valuation->getValue(n[0]).getConst() == + valuation->getValue(n[1]).getConst() ); case kind::IMPLIES: // 2 args - return nodeManager->mkConst( (! engine->getValue(n[0]).getConst()) || - engine->getValue(n[1]).getConst() ); + return nodeManager->mkConst( (! valuation->getValue(n[0]).getConst()) || + valuation->getValue(n[1]).getConst() ); case kind::OR: { // 2+ args for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { - if(engine->getValue(*i).getConst()) { + if(valuation->getValue(*i).getConst()) { return nodeManager->mkConst(true); } } @@ -73,16 +73,16 @@ Node TheoryBool::getValue(TNode n, TheoryEngine* engine) { } case kind::XOR: // 2 args - return nodeManager->mkConst( engine->getValue(n[0]).getConst() != - engine->getValue(n[1]).getConst() ); + return nodeManager->mkConst( valuation->getValue(n[0]).getConst() != + valuation->getValue(n[1]).getConst() ); case kind::ITE: // 3 args // all ITEs should be gone except (bool,bool,bool) ones Assert( n[1].getType() == nodeManager->booleanType() && n[2].getType() == nodeManager->booleanType() ); - return nodeManager->mkConst( engine->getValue(n[0]).getConst() ? - engine->getValue(n[1]).getConst() : - engine->getValue(n[2]).getConst() ); + return nodeManager->mkConst( valuation->getValue(n[0]).getConst() ? + valuation->getValue(n[1]).getConst() : + valuation->getValue(n[2]).getConst() ); default: Unhandled(n.getKind()); diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 5d91842d7..4120159df 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -43,7 +43,7 @@ public: Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl; } - Node getValue(TNode n, TheoryEngine* engine); + Node getValue(TNode n, Valuation* valuation); std::string identify() const { return std::string("TheoryBool"); } }; diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 489c97e67..a276fa0ce 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -17,7 +17,7 @@ **/ #include "theory/builtin/theory_builtin.h" -#include "theory/theory_engine.h" +#include "theory/valuation.h" #include "expr/kind.h" using namespace std; @@ -26,7 +26,7 @@ namespace CVC4 { namespace theory { namespace builtin { -Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) { +Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) { switch(n.getKind()) { case kind::VARIABLE: @@ -39,7 +39,7 @@ Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) { Assert(n[0].getKind() == kind::TUPLE && n[1].getKind() == kind::TUPLE); return NodeManager::currentNM()-> - mkConst( getValue(n[0], engine) == getValue(n[1], engine) ); + mkConst( getValue(n[0], valuation) == getValue(n[1], valuation) ); } case kind::TUPLE: { // 2+ args @@ -48,14 +48,14 @@ Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) { iend = n.end(); i != iend; ++i) { - nb << engine->getValue(*i); + nb << valuation->getValue(*i); } return Node(nb); } default: // all other "builtins" should have been rewritten away or handled - // by theory engine, or handled elsewhere. + // by the valuation, or handled elsewhere. Unhandled(n.getKind()); } } diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index baa1493b6..5b9810326 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -31,7 +31,7 @@ class TheoryBuiltin : public Theory { public: TheoryBuiltin(context::Context* c, OutputChannel& out) : Theory(THEORY_BUILTIN, c, out) {} - Node getValue(TNode n, TheoryEngine* engine); + Node getValue(TNode n, Valuation* valuation); std::string identify() const { return std::string("TheoryBuiltin"); } };/* class TheoryBuiltin */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 0356e5f27..b600bc8f1 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -20,7 +20,7 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/theory_engine.h" +#include "theory/valuation.h" using namespace CVC4; using namespace CVC4::theory; @@ -115,7 +115,7 @@ bool TheoryBV::triggerEquality(size_t triggerId) { return true; } -Node TheoryBV::getValue(TNode n, TheoryEngine* engine) { +Node TheoryBV::getValue(TNode n, Valuation* valuation) { NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { @@ -125,7 +125,7 @@ Node TheoryBV::getValue(TNode n, TheoryEngine* engine) { case kind::EQUAL: // 2 args return nodeManager-> - mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) ); default: Unhandled(n.getKind()); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index ed23bf53f..ede98004f 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -88,7 +88,7 @@ public: void explain(TNode n) { } - Node getValue(TNode n, TheoryEngine* engine); + Node getValue(TNode n, Valuation* valuation); std::string identify() const { return std::string("TheoryBV"); } };/* class TheoryBV */ diff --git a/src/theory/theory.h b/src/theory/theory.h index a4682710f..b4c3a897b 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -35,6 +35,10 @@ namespace CVC4 { class TheoryEngine; +namespace theory { + class Valuation; +}/* CVC4::theory namespace */ + namespace theory { /** @@ -322,7 +326,8 @@ public: * if you *know* that you are responsible handle the Node you're * asking for; other theories can use your types, so be careful * here! To be safe, it's best to delegate back to the - * TheoryEngine. + * TheoryEngine (by way of the Valuation proxy object, which avoids + * direct dependence on TheoryEngine). * * Usually, you need to handle at least the two cases of EQUAL and * VARIABLE---EQUAL in case a value of yours is on the LHS of an @@ -337,7 +342,7 @@ public: * and suspect this situation is the case, return Node::null() * rather than throwing an exception. */ - virtual Node getValue(TNode n, TheoryEngine* engine) = 0; + virtual Node getValue(TNode n, Valuation* valuation) = 0; /** * The theory should only add (via .operator<< or .append()) to the diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 25fe29c67..97cb8f471 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -134,6 +134,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) : d_theoryRegistration(opts.theoryRegistration), d_hasShutDown(false), d_incomplete(ctxt, false), + d_valuation(this), d_statistics() { Rewriter::init(); @@ -226,6 +227,49 @@ Node TheoryEngine::preprocess(TNode node) { return preprocessed; } +/** + * Check all (currently-active) theories for conflicts. + * @param effort the effort level to use + */ +bool TheoryEngine::check(theory::Theory::Effort effort) { + d_theoryOut.d_conflictNode = Node::null(); + d_theoryOut.d_propagatedLiterals.clear(); + +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits::hasCheck) { \ + reinterpret_cast::theory_class*>(d_theoryTable[THEORY])->check(effort); \ + if (!d_theoryOut.d_conflictNode.get().isNull()) { \ + return false; \ + } \ + } + + // Do the checking + try { + CVC4_FOR_EACH_THEORY + } catch(const theory::Interrupted&) { + Debug("theory") << "TheoryEngine::check() => conflict" << std::endl; + } + + return true; +} + +void TheoryEngine::propagate() { + // Definition of the statement that is to be run by every theory +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits::hasPropagate) { \ + reinterpret_cast::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \ + } + + // Propagate for each theory using the statement above + CVC4_FOR_EACH_THEORY +} + /* Our goal is to tease out any ITE's sitting under a theory operator. */ Node TheoryEngine::removeITEs(TNode node) { Debug("ite") << "removeITEs(" << node << ")" << endl; @@ -294,7 +338,7 @@ Node TheoryEngine::getValue(TNode node) { } // otherwise ask the theory-in-charge - return theoryOf(node)->getValue(node, this); + return theoryOf(node)->getValue(node, &d_valuation); }/* TheoryEngine::getValue(TNode node) */ bool TheoryEngine::presolve() { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index bb0e9c10e..6a343717a 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -27,8 +27,8 @@ #include "prop/prop_engine.h" #include "theory/shared_term_manager.h" #include "theory/theory.h" -#include "theory/theory_traits.h" #include "theory/rewriter.h" +#include "theory/valuation.h" #include "util/options.h" #include "util/stats.h" @@ -143,6 +143,12 @@ class TheoryEngine { */ context::CDO d_incomplete; + /** + * A "valuation proxy" for this TheoryEngine. Used only in getValue() + * for decoupled Theory-to-TheoryEngine communication. + */ + theory::Valuation d_valuation; + /** * Replace ITE forms in a node. */ @@ -270,31 +276,7 @@ public: * Check all (currently-active) theories for conflicts. * @param effort the effort level to use */ - inline bool check(theory::Theory::Effort effort) - { - d_theoryOut.d_conflictNode = Node::null(); - d_theoryOut.d_propagatedLiterals.clear(); - -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT -#endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits::hasCheck) { \ - reinterpret_cast::theory_class*>(d_theoryTable[THEORY])->check(effort); \ - if (!d_theoryOut.d_conflictNode.get().isNull()) { \ - return false; \ - } \ - } - - // Do the checking - try { - CVC4_FOR_EACH_THEORY - } catch(const theory::Interrupted&) { - Debug("theory") << "TheoryEngine::check() => conflict" << std::endl; - } - - return true; - } + bool check(theory::Theory::Effort effort); /** * Calls staticLearning() on all active theories, accumulating their @@ -332,20 +314,7 @@ public: return d_theoryOut.d_conflictNode; } - inline void propagate() { - - // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT -#endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits::hasPropagate) { \ - reinterpret_cast::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \ - } - - // Propagate for each theory using the statement above - CVC4_FOR_EACH_THEORY - } + void propagate(); inline Node getExplanation(TNode node, theory::Theory* theory) { theory->explain(node); diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index 33c8bc7b6..5d4d44d0a 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -17,7 +17,7 @@ **/ #include "theory/uf/morgan/theory_uf_morgan.h" -#include "theory/theory_engine.h" +#include "theory/valuation.h" #include "expr/kind.h" #include "util/congruence_closure.h" @@ -567,7 +567,7 @@ void TheoryUFMorgan::notifyRestart() { Debug("uf") << "uf: end notifyDecisionLevelZero()" << endl; } -Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) { +Node TheoryUFMorgan::getValue(TNode n, Valuation* valuation) { NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { @@ -585,7 +585,7 @@ Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) { case kind::EQUAL: // 2 args return nodeManager-> - mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) ); default: Unhandled(n.getKind()); diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index 2a079603b..47c860c9a 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -214,7 +214,7 @@ public: * Overloads Node getValue(TNode n); from theory.h. * See theory/theory.h for more information about this method. */ - Node getValue(TNode n, TheoryEngine* engine); + Node getValue(TNode n, Valuation* valuation); std::string identify() const { return std::string("TheoryUFMorgan"); } diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h index cdaa7975c..d07f49f03 100644 --- a/src/theory/uf/tim/theory_uf_tim.h +++ b/src/theory/uf/tim/theory_uf_tim.h @@ -20,7 +20,6 @@ ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf) ** This has been extended to work in a context-dependent way. ** This interacts heavily with the data-structures given in ecdata.h . - ** **/ #include "cvc4_private.h" @@ -151,7 +150,7 @@ public: * Overloads Node getValue(TNode n); from theory.h. * See theory/theory.h for more information about this method. */ - Node getValue(TNode n, TheoryEngine* engine) { + Node getValue(TNode n, Valuation* valuation) { Unimplemented("TheoryUFTim doesn't support model generation"); } diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp new file mode 100644 index 000000000..20d339b52 --- /dev/null +++ b/src/theory/valuation.cpp @@ -0,0 +1,31 @@ +/********************* */ +/*! \file valuation.cpp + ** \verbatim + ** 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.\endverbatim + ** + ** \brief A "valuation" proxy for TheoryEngine + ** + ** Implementation of Valuation class. + **/ + +#include "expr/node.h" +#include "theory/valuation.h" +#include "theory/theory_engine.h" + +namespace CVC4 { +namespace theory { + +Node Valuation::getValue(TNode n) { + return d_engine->getValue(n); +} + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/valuation.h b/src/theory/valuation.h new file mode 100644 index 000000000..2d38c29cd --- /dev/null +++ b/src/theory/valuation.h @@ -0,0 +1,48 @@ +/********************* */ +/*! \file valuation.h + ** \verbatim + ** 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.\endverbatim + ** + ** \brief A "valuation" proxy for TheoryEngine + ** + ** A "valuation" proxy for TheoryEngine. This class breaks the dependence + ** of theories' getValue() implementations on TheoryEngine. getValue() + ** takes a Valuation, which delegates to TheoryEngine. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__VALUATION_H +#define __CVC4__THEORY__VALUATION_H + +#include "expr/node.h" + +namespace CVC4 { + +class TheoryEngine; + +namespace theory { + +class Valuation { + TheoryEngine* d_engine; +public: + Valuation(TheoryEngine* engine) : + d_engine(engine) { + } + + Node getValue(TNode n); + +};/* class Valuation */ + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__VALUATION_H */ diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 2315268a8..18408acd3 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -142,7 +142,7 @@ public: void preRegisterTerm(TNode n) {} void propagate(Effort level) {} void explain(TNode n, Effort level) {} - Node getValue(TNode n, TheoryEngine* engine) { return Node::null(); } + Node getValue(TNode n, Valuation* valuation) { return Node::null(); } string identify() const { return "DummyTheory"; } }; diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index c78a7456d..5915ac1f7 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -28,6 +28,7 @@ #include "theory/theory.h" #include "theory/theory_engine.h" +#include "theory/valuation.h" #include "theory/rewriter.h" #include "expr/node.h" #include "expr/node_manager.h" @@ -211,7 +212,7 @@ public: void check(Theory::Effort) { Unimplemented(); } void propagate(Theory::Effort) { Unimplemented(); } void explain(TNode, Theory::Effort) { Unimplemented(); } - Node getValue(TNode n, TheoryEngine* engine) { return Node::null(); } + Node getValue(TNode n, Valuation* valuation) { return Node::null(); } };/* class FakeTheory */