diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-02-26 21:24:18 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-02-26 21:24:18 +0000 |
commit | edf6aaa87da179948e6b233d16fa37d2aea58bbb (patch) | |
tree | fc5429ce891f579b6e5daedd52e423c13d4f4ec8 /src/theory/uf | |
parent | 5c9af4e1382d32352aae7f8c31795831882931b2 (diff) |
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).
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.cpp | 6 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.h | 2 | ||||
-rw-r--r-- | src/theory/uf/tim/theory_uf_tim.h | 3 |
3 files changed, 5 insertions, 6 deletions
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"); } |