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/builtin/theory_builtin.cpp | |
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/builtin/theory_builtin.cpp')
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
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()); } } |