diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 34 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 4 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 8 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 4 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 26 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 6 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 6 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.h | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/theory.h | 46 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 19 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 14 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.cpp | 8 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.h | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 4 | ||||
-rw-r--r-- | src/theory/uf/tim/theory_uf_tim.cpp | 4 | ||||
-rw-r--r-- | src/theory/uf/tim/theory_uf_tim.h | 6 |
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"); } |