diff options
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 6 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.h | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index a276fa0ce..1c779bd79 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -26,7 +26,7 @@ namespace CVC4 { namespace theory { namespace builtin { -Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) { +Node TheoryBuiltin::getValue(TNode n) { switch(n.getKind()) { case kind::VARIABLE: @@ -39,7 +39,7 @@ Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) { Assert(n[0].getKind() == kind::TUPLE && n[1].getKind() == kind::TUPLE); return NodeManager::currentNM()-> - mkConst( getValue(n[0], valuation) == getValue(n[1], valuation) ); + mkConst( getValue(n[0]) == getValue(n[1]) ); } case kind::TUPLE: { // 2+ args @@ -48,7 +48,7 @@ Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) { iend = n.end(); i != iend; ++i) { - nb << valuation->getValue(*i); + nb << d_valuation.getValue(*i); } return Node(nb); } diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 5b9810326..4e62401ff 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -29,9 +29,9 @@ namespace builtin { class TheoryBuiltin : public Theory { public: - TheoryBuiltin(context::Context* c, OutputChannel& out) : - Theory(THEORY_BUILTIN, c, out) {} - Node getValue(TNode n, Valuation* valuation); + TheoryBuiltin(context::Context* c, OutputChannel& out, Valuation valuation) : + Theory(THEORY_BUILTIN, c, out, valuation) {} + Node getValue(TNode n); std::string identify() const { return std::string("TheoryBuiltin"); } };/* class TheoryBuiltin */ |