diff options
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"); } |