summaryrefslogtreecommitdiff
path: root/src/theory/arrays/theory_arrays.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r--src/theory/arrays/theory_arrays.cpp8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index d45320266..8b625613a 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -30,8 +30,8 @@ using namespace CVC4::theory;
using namespace CVC4::theory::arrays;
-TheoryArrays::TheoryArrays(Context* c, OutputChannel& out) :
- Theory(THEORY_ARRAY, c, out)
+TheoryArrays::TheoryArrays(Context* c, OutputChannel& out, Valuation valuation) :
+ Theory(THEORY_ARRAY, c, out, valuation)
{
}
@@ -60,7 +60,7 @@ void TheoryArrays::check(Effort e) {
Debug("arrays") << "TheoryArrays::check(): done" << endl;
}
-Node TheoryArrays::getValue(TNode n, Valuation* valuation) {
+Node TheoryArrays::getValue(TNode n) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
@@ -70,7 +70,7 @@ Node TheoryArrays::getValue(TNode n, Valuation* valuation) {
case kind::EQUAL: // 2 args
return nodeManager->
- mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) );
+ mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
default:
Unhandled(n.getKind());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback