summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/theory_arith.cpp34
-rw-r--r--src/theory/arith/theory_arith.h4
-rw-r--r--src/theory/arrays/theory_arrays.cpp8
-rw-r--r--src/theory/arrays/theory_arrays.h4
-rw-r--r--src/theory/booleans/theory_bool.cpp26
-rw-r--r--src/theory/booleans/theory_bool.h6
-rw-r--r--src/theory/builtin/theory_builtin.cpp6
-rw-r--r--src/theory/builtin/theory_builtin.h6
-rw-r--r--src/theory/bv/theory_bv.cpp4
-rw-r--r--src/theory/bv/theory_bv.h6
-rw-r--r--src/theory/bv/theory_bv_rewriter.h2
-rw-r--r--src/theory/theory.h46
-rw-r--r--src/theory/theory_engine.cpp19
-rw-r--r--src/theory/theory_engine.h14
-rw-r--r--src/theory/uf/morgan/theory_uf_morgan.cpp8
-rw-r--r--src/theory/uf/morgan/theory_uf_morgan.h4
-rw-r--r--src/theory/uf/theory_uf.h4
-rw-r--r--src/theory/uf/tim/theory_uf_tim.cpp4
-rw-r--r--src/theory/uf/tim/theory_uf_tim.h6
19 files changed, 115 insertions, 96 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index dfa81cb3f..4b40e582c 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -55,8 +55,8 @@ using namespace CVC4::theory::arith;
struct SlackAttrID;
typedef expr::Attribute<SlackAttrID, Node> Slack;
-TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
- Theory(THEORY_ARITH, c, out),
+TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation) :
+ Theory(THEORY_ARITH, c, out, valuation),
d_partialModel(c),
d_userVariables(),
d_diseq(c),
@@ -497,7 +497,7 @@ void TheoryArith::propagate(Effort e) {
}
}
-Node TheoryArith::getValue(TNode n, Valuation* valuation) {
+Node TheoryArith::getValue(TNode n) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
@@ -508,7 +508,7 @@ Node TheoryArith::getValue(TNode n, Valuation* valuation) {
Node eq = d_removedRows.find(var)->second;
Assert(n == eq[0]);
Node rhs = eq[1];
- return getValue(rhs, valuation);
+ return getValue(rhs);
}
DeltaRational drat = d_partialModel.getAssignment(var);
@@ -521,7 +521,7 @@ Node TheoryArith::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]) );
case kind::PLUS: { // 2+ args
Rational value(0);
@@ -529,7 +529,7 @@ Node TheoryArith::getValue(TNode n, Valuation* valuation) {
iend = n.end();
i != iend;
++i) {
- value += valuation->getValue(*i).getConst<Rational>();
+ value += d_valuation.getValue(*i).getConst<Rational>();
}
return nodeManager->mkConst(value);
}
@@ -540,7 +540,7 @@ Node TheoryArith::getValue(TNode n, Valuation* valuation) {
iend = n.end();
i != iend;
++i) {
- value *= valuation->getValue(*i).getConst<Rational>();
+ value *= d_valuation.getValue(*i).getConst<Rational>();
}
return nodeManager->mkConst(value);
}
@@ -554,24 +554,24 @@ Node TheoryArith::getValue(TNode n, Valuation* valuation) {
Unreachable();
case kind::DIVISION: // 2 args
- return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() /
- valuation->getValue(n[1]).getConst<Rational>() );
+ return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() /
+ d_valuation.getValue(n[1]).getConst<Rational>() );
case kind::LT: // 2 args
- return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() <
- valuation->getValue(n[1]).getConst<Rational>() );
+ return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() <
+ d_valuation.getValue(n[1]).getConst<Rational>() );
case kind::LEQ: // 2 args
- return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() <=
- valuation->getValue(n[1]).getConst<Rational>() );
+ return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() <=
+ d_valuation.getValue(n[1]).getConst<Rational>() );
case kind::GT: // 2 args
- return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() >
- valuation->getValue(n[1]).getConst<Rational>() );
+ return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() >
+ d_valuation.getValue(n[1]).getConst<Rational>() );
case kind::GEQ: // 2 args
- return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() >=
- valuation->getValue(n[1]).getConst<Rational>() );
+ return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() >=
+ d_valuation.getValue(n[1]).getConst<Rational>() );
default:
Unhandled(n.getKind());
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 07ba08e9c..11cbfb425 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -144,7 +144,7 @@ private:
SimplexDecisionProcedure d_simplex;
public:
- TheoryArith(context::Context* c, OutputChannel& out);
+ TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation);
~TheoryArith();
/**
@@ -161,7 +161,7 @@ public:
void notifyEq(TNode lhs, TNode rhs);
- Node getValue(TNode n, Valuation* valuation);
+ Node getValue(TNode n);
void shutdown(){ }
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());
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 5a63fd26c..64fdd8303 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -31,7 +31,7 @@ namespace arrays {
class TheoryArrays : public Theory {
public:
- TheoryArrays(context::Context* c, OutputChannel& out);
+ TheoryArrays(context::Context* c, OutputChannel& out, Valuation valuation);
~TheoryArrays();
void preRegisterTerm(TNode n) { }
void registerTerm(TNode n) { }
@@ -43,7 +43,7 @@ public:
void check(Effort e);
void propagate(Effort e) { }
void explain(TNode n) { }
- Node getValue(TNode n, Valuation* valuation);
+ Node getValue(TNode n);
void shutdown() { }
std::string identify() const { return std::string("TheoryArrays"); }
};/* class TheoryArrays */
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 44f5d60a6..878b18478 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -24,7 +24,7 @@ namespace CVC4 {
namespace theory {
namespace booleans {
-Node TheoryBool::getValue(TNode n, Valuation* valuation) {
+Node TheoryBool::getValue(TNode n) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
@@ -38,14 +38,14 @@ Node TheoryBool::getValue(TNode n, Valuation* valuation) {
Unreachable();
case kind::NOT: // 1 arg
- return nodeManager->mkConst(! valuation->getValue(n[0]).getConst<bool>());
+ return nodeManager->mkConst(! d_valuation.getValue(n[0]).getConst<bool>());
case kind::AND: { // 2+ args
for(TNode::iterator i = n.begin(),
iend = n.end();
i != iend;
++i) {
- if(! valuation->getValue(*i).getConst<bool>()) {
+ if(! d_valuation.getValue(*i).getConst<bool>()) {
return nodeManager->mkConst(false);
}
}
@@ -53,19 +53,19 @@ Node TheoryBool::getValue(TNode n, Valuation* valuation) {
}
case kind::IFF: // 2 args
- return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() ==
- valuation->getValue(n[1]).getConst<bool>() );
+ return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() ==
+ d_valuation.getValue(n[1]).getConst<bool>() );
case kind::IMPLIES: // 2 args
- return nodeManager->mkConst( (! valuation->getValue(n[0]).getConst<bool>()) ||
- valuation->getValue(n[1]).getConst<bool>() );
+ return nodeManager->mkConst( (! d_valuation.getValue(n[0]).getConst<bool>()) ||
+ d_valuation.getValue(n[1]).getConst<bool>() );
case kind::OR: { // 2+ args
for(TNode::iterator i = n.begin(),
iend = n.end();
i != iend;
++i) {
- if(valuation->getValue(*i).getConst<bool>()) {
+ if(d_valuation.getValue(*i).getConst<bool>()) {
return nodeManager->mkConst(true);
}
}
@@ -73,16 +73,16 @@ Node TheoryBool::getValue(TNode n, Valuation* valuation) {
}
case kind::XOR: // 2 args
- return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() !=
- valuation->getValue(n[1]).getConst<bool>() );
+ return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() !=
+ d_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( valuation->getValue(n[0]).getConst<bool>() ?
- valuation->getValue(n[1]).getConst<bool>() :
- valuation->getValue(n[2]).getConst<bool>() );
+ return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() ?
+ d_valuation.getValue(n[1]).getConst<bool>() :
+ d_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 4120159df..dfcdd22b8 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -30,8 +30,8 @@ namespace booleans {
class TheoryBool : public Theory {
public:
- TheoryBool(context::Context* c, OutputChannel& out) :
- Theory(THEORY_BOOL, c, out) {
+ TheoryBool(context::Context* c, OutputChannel& out, Valuation valuation) :
+ Theory(THEORY_BOOL, c, out, valuation) {
}
void preRegisterTerm(TNode n) {
@@ -43,7 +43,7 @@ public:
Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
}
- Node getValue(TNode n, Valuation* valuation);
+ Node getValue(TNode n);
std::string identify() const { return std::string("TheoryBool"); }
};
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 */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 258345ad8..e106f3b84 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -155,7 +155,7 @@ bool TheoryBV::triggerEquality(size_t triggerId) {
return true;
}
-Node TheoryBV::getValue(TNode n, Valuation* valuation) {
+Node TheoryBV::getValue(TNode n) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
@@ -165,7 +165,7 @@ Node TheoryBV::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());
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index f2c2fa332..d65f0388b 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -103,8 +103,8 @@ private:
public:
- TheoryBV(context::Context* c, OutputChannel& out) :
- Theory(THEORY_BV, c, out), d_eqEngine(*this, c, "theory::bv::EqualityEngine"), d_sliceManager(*this, c), d_assertions(c), d_disequalities(c) {
+ TheoryBV(context::Context* c, OutputChannel& out, Valuation valuation) :
+ Theory(THEORY_BV, c, out, valuation), d_eqEngine(*this, c, "theory::bv::EqualityEngine"), d_sliceManager(*this, c), d_assertions(c), d_disequalities(c) {
}
BvEqualityEngine& getEqualityEngine() {
@@ -123,7 +123,7 @@ public:
void explain(TNode n);
- Node getValue(TNode n, Valuation* valuation);
+ Node getValue(TNode n);
std::string identify() const { return std::string("TheoryBV"); }
};/* class TheoryBV */
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index bdf1c8d51..7af5b4496 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -28,7 +28,7 @@ namespace CVC4 {
namespace theory {
namespace bv {
-class AllRewriteRules;
+struct AllRewriteRules;
class TheoryBVRewriter {
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 620c70710..72341869d 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -23,6 +23,7 @@
#include "expr/node.h"
#include "expr/attribute.h"
+#include "theory/valuation.h"
#include "theory/output_channel.h"
#include "context/context.h"
#include "context/cdlist.h"
@@ -37,10 +38,11 @@ namespace CVC4 {
class TheoryEngine;
namespace theory {
- class Valuation;
-}/* CVC4::theory namespace */
-namespace theory {
+/** Tag for the "newFact()-has-been-called-in-this-context" flag on Nodes */
+struct AssertedAttrTag {};
+/** The "newFact()-has-been-called-in-this-context" flag on Nodes */
+typedef CVC4::expr::CDAttribute<AssertedAttrTag, bool> Asserted;
/**
* Base class for T-solvers. Abstract DPLL(T).
@@ -88,16 +90,15 @@ protected:
/**
* Construct a Theory.
*/
- Theory(TheoryId id, context::Context* ctxt, OutputChannel& out) throw() :
+ Theory(TheoryId id, context::Context* ctxt, OutputChannel& out, Valuation valuation) throw() :
d_id(id),
d_context(ctxt),
d_facts(ctxt),
d_factsHead(ctxt, 0),
- d_out(&out) {
+ d_out(&out),
+ d_valuation(valuation) {
}
-
-
/**
* This is called at shutdown time by the TheoryEngine, just before
* destruction. It is important because there are destruction
@@ -114,10 +115,11 @@ protected:
*/
OutputChannel* d_out;
- /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
- struct PreRegistered {};
- /** The "preRegisterTerm()-has-been-called" flag on Nodes */
- typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr;
+ /**
+ * The valuation proxy for the Theory to communicate back with the
+ * theory engine (and other theories).
+ */
+ Valuation d_valuation;
/**
* Returns the next atom in the assertFact() queue. Guarantees that
@@ -135,6 +137,26 @@ protected:
return fact;
}
+ /**
+ * Provides access to the facts queue, primarily intended for theory
+ * debugging purposes.
+ *
+ * @return the iterator to the beginning of the fact queue
+ */
+ context::CDList<Node>::const_iterator facts_begin() const {
+ return d_facts.begin();
+ }
+
+ /**
+ * Provides access to the facts queue, primarily intended for theory
+ * debugging purposes.
+ *
+ * @return the iterator to the end of the fact queue
+ */
+ context::CDList<Node>::const_iterator facts_end() const {
+ return d_facts.end();
+ }
+
public:
static inline TheoryId theoryOf(TypeNode typeNode) {
@@ -345,7 +367,7 @@ public:
* and suspect this situation is the case, return Node::null()
* rather than throwing an exception.
*/
- virtual Node getValue(TNode n, Valuation* valuation) {
+ virtual Node getValue(TNode n) {
Unimplemented("Theory %s doesn't support Theory::getValue interface",
identify().c_str());
return Node::null();
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f8eece3df..2411956f5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -36,18 +36,18 @@ using namespace CVC4::theory;
namespace CVC4 {
+namespace theory {
+
/** Tag for the "registerTerm()-has-been-called" flag on Nodes */
-struct Registered {};
+struct RegisteredAttrTag {};
/** The "registerTerm()-has-been-called" flag on Nodes */
-typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
-
-namespace theory {
+typedef CVC4::expr::CDAttribute<RegisteredAttrTag, bool> RegisteredAttr;
-struct PreRegisteredTag {};
-typedef expr::Attribute<PreRegisteredTag, bool> PreRegistered;
+struct PreRegisteredAttrTag {};
+typedef expr::Attribute<PreRegisteredAttrTag, bool> PreRegistered;
-struct IteRewriteTag {};
-typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr;
+struct IteRewriteAttrTag {};
+typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr;
}/* CVC4::theory namespace */
@@ -136,7 +136,6 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) :
d_theoryRegistration(opts.theoryRegistration),
d_hasShutDown(false),
d_incomplete(ctxt, false),
- d_valuation(this),
d_opts(opts),
d_statistics() {
@@ -347,7 +346,7 @@ Node TheoryEngine::getValue(TNode node) {
}
// otherwise ask the theory-in-charge
- return theoryOf(node)->getValue(node, &d_valuation);
+ return theoryOf(node)->getValue(node);
}/* TheoryEngine::getValue(TNode node) */
bool TheoryEngine::presolve() {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7553b1f0c..787323495 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -151,12 +151,6 @@ class TheoryEngine {
context::CDO<bool> d_incomplete;
/**
- * A "valuation proxy" for this TheoryEngine. Used only in getValue()
- * for decoupled Theory-to-TheoryEngine communication.
- */
- theory::Valuation d_valuation;
-
- /**
* Replace ITE forms in a node.
*/
Node removeITEs(TNode t);
@@ -180,7 +174,7 @@ public:
*/
template <class TheoryClass>
void addTheory() {
- TheoryClass* theory = new TheoryClass(d_context, d_theoryOut);
+ TheoryClass* theory = new TheoryClass(d_context, d_theoryOut, theory::Valuation(this));
d_theoryTable[theory->getId()] = theory;
d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory));
@@ -258,6 +252,12 @@ public:
inline void assertFact(TNode node) {
Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
+ // Mark it as asserted in this context
+ //
+ // [MGD] removed for now, this appears to have a nontrivial
+ // performance penalty
+ // node.setAttribute(theory::Asserted(), true);
+
// Get the atom
TNode atom = node.getKind() == kind::NOT ? node[0] : node;
diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
index 5d4d44d0a..e15467bff 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.cpp
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -31,8 +31,8 @@ using namespace CVC4::theory;
using namespace CVC4::theory::uf;
using namespace CVC4::theory::uf::morgan;
-TheoryUFMorgan::TheoryUFMorgan(Context* ctxt, OutputChannel& out) :
- TheoryUF(ctxt, out),
+TheoryUFMorgan::TheoryUFMorgan(Context* ctxt, OutputChannel& out, Valuation valuation) :
+ TheoryUF(ctxt, out, valuation),
d_assertions(ctxt),
d_ccChannel(this),
d_cc(ctxt, &d_ccChannel),
@@ -567,7 +567,7 @@ void TheoryUFMorgan::notifyRestart() {
Debug("uf") << "uf: end notifyDecisionLevelZero()" << endl;
}
-Node TheoryUFMorgan::getValue(TNode n, Valuation* valuation) {
+Node TheoryUFMorgan::getValue(TNode n) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
@@ -585,7 +585,7 @@ Node TheoryUFMorgan::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());
diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h
index 47c860c9a..c2feef349 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.h
+++ b/src/theory/uf/morgan/theory_uf_morgan.h
@@ -132,7 +132,7 @@ private:
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUFMorgan(context::Context* ctxt, OutputChannel& out);
+ TheoryUFMorgan(context::Context* ctxt, OutputChannel& out, Valuation valuation);
/** Destructor for UF theory, cleans up memory and statistics. */
~TheoryUFMorgan();
@@ -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, Valuation* valuation);
+ Node getValue(TNode n);
std::string identify() const { return std::string("TheoryUFMorgan"); }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index be3d7ac69..9746b38ab 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -37,8 +37,8 @@ class TheoryUF : public Theory {
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUF(context::Context* ctxt, OutputChannel& out)
- : Theory(THEORY_UF, ctxt, out) {}
+ TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation)
+ : Theory(THEORY_UF, ctxt, out, valuation) { }
};/* class TheoryUF */
diff --git a/src/theory/uf/tim/theory_uf_tim.cpp b/src/theory/uf/tim/theory_uf_tim.cpp
index db0574d4f..ef1704426 100644
--- a/src/theory/uf/tim/theory_uf_tim.cpp
+++ b/src/theory/uf/tim/theory_uf_tim.cpp
@@ -27,8 +27,8 @@ using namespace CVC4::theory;
using namespace CVC4::theory::uf;
using namespace CVC4::theory::uf::tim;
-TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out) :
- TheoryUF(c, out),
+TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out, Valuation valuation) :
+ TheoryUF(c, out, valuation),
d_assertions(c),
d_pending(c),
d_currentPendingIdx(c,0),
diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h
index d07f49f03..70c60728f 100644
--- a/src/theory/uf/tim/theory_uf_tim.h
+++ b/src/theory/uf/tim/theory_uf_tim.h
@@ -85,13 +85,11 @@ private:
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUFTim(context::Context* c, OutputChannel& out);
+ TheoryUFTim(context::Context* c, OutputChannel& out, Valuation valuation);
/** Destructor for the TheoryUF object. */
~TheoryUFTim();
-
-
/**
* Registers a previously unseen [in this context] node n.
* For TheoryUF, this sets up and maintains invaraints about
@@ -150,7 +148,7 @@ public:
* Overloads Node getValue(TNode n); from theory.h.
* See theory/theory.h for more information about this method.
*/
- Node getValue(TNode n, Valuation* valuation) {
+ Node getValue(TNode n) {
Unimplemented("TheoryUFTim doesn't support model generation");
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback