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/bv | |
| 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/bv')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 6 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv.h | 2 |
2 files changed, 4 insertions, 4 deletions
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 */ |