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/booleans | |
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/booleans')
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 28 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 2 |
2 files changed, 15 insertions, 15 deletions
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<bool>()); + return nodeManager->mkConst(! valuation->getValue(n[0]).getConst<bool>()); case kind::AND: { // 2+ args for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { - if(! engine->getValue(*i).getConst<bool>()) { + if(! valuation->getValue(*i).getConst<bool>()) { 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<bool>() == - engine->getValue(n[1]).getConst<bool>() ); + return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() == + valuation->getValue(n[1]).getConst<bool>() ); case kind::IMPLIES: // 2 args - return nodeManager->mkConst( (! engine->getValue(n[0]).getConst<bool>()) || - engine->getValue(n[1]).getConst<bool>() ); + return nodeManager->mkConst( (! valuation->getValue(n[0]).getConst<bool>()) || + valuation->getValue(n[1]).getConst<bool>() ); case kind::OR: { // 2+ args for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { - if(engine->getValue(*i).getConst<bool>()) { + if(valuation->getValue(*i).getConst<bool>()) { 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<bool>() != - engine->getValue(n[1]).getConst<bool>() ); + return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() != + valuation->getValue(n[1]).getConst<bool>() ); 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<bool>() ? - engine->getValue(n[1]).getConst<bool>() : - engine->getValue(n[2]).getConst<bool>() ); + return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() ? + valuation->getValue(n[1]).getConst<bool>() : + valuation->getValue(n[2]).getConst<bool>() ); 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"); } }; |