diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/delta_rational.cpp | 8 | ||||
-rw-r--r-- | src/theory/arith/delta_rational.h | 4 | ||||
-rw-r--r-- | src/theory/arith/tableau.cpp | 8 | ||||
-rw-r--r-- | src/theory/arith/tableau.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 76 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 18 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 1 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 66 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 2 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 38 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.h | 1 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 24 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 | ||||
-rw-r--r-- | src/theory/theory.h | 66 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 16 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 4 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.cpp | 27 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.h | 10 | ||||
-rw-r--r-- | src/theory/uf/tim/theory_uf_tim.h | 10 |
20 files changed, 354 insertions, 31 deletions
diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index f6a460fee..d0e4ed1f4 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -24,12 +24,12 @@ using namespace std; using namespace CVC4; std::ostream& CVC4::operator<<(std::ostream& os, const DeltaRational& dq){ - return os << "(" << dq.getNoninfintestimalPart() - << "," << dq.getInfintestimalPart() << ")"; + return os << "(" << dq.getNoninfinitesimalPart() + << "," << dq.getInfinitesimalPart() << ")"; } std::string DeltaRational::toString() const { - return "(" + getNoninfintestimalPart().toString() + "," + - getInfintestimalPart().toString() + ")"; + return "(" + getNoninfinitesimalPart().toString() + "," + + getInfinitesimalPart().toString() + ")"; } diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 26212ec66..b75f5334c 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -46,11 +46,11 @@ public: DeltaRational(const CVC4::Rational& base, const CVC4::Rational& coeff) : c(base), k(coeff) {} - const CVC4::Rational& getInfintestimalPart() const { + const CVC4::Rational& getInfinitesimalPart() const { return k; } - const CVC4::Rational& getNoninfintestimalPart() const { + const CVC4::Rational& getNoninfinitesimalPart() const { return c; } diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index aaeadb629..d6a30ac91 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -48,7 +48,7 @@ Row::Row(ArithVar basic, Assert(d_coeffs[var_i] != Rational(0,1)); } } -void Row::subsitute(Row& row_s){ +void Row::substitute(Row& row_s){ ArithVar x_s = row_s.basicVar(); Assert(has(x_s)); @@ -133,7 +133,7 @@ void Tableau::addRow(ArithVar basicVar, Assert(isActiveBasicVariable(var)); Row* row_var = lookup(var); - row_current->subsitute(*row_var); + row_current->substitute(*row_var); } } } @@ -163,7 +163,7 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ Row* row_k = lookup(basic); if(row_k->has(x_s)){ d_activityMonitor.increaseActivity(basic, 30); - row_k->subsitute(*row_s); + row_k->substitute(*row_s); } } } @@ -189,7 +189,7 @@ void Tableau::updateRow(Row* row){ Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var); Assert(row_var != row); - row->subsitute(*row_var); + row->substitute(*row_var); i = row->begin(); endIter = row->end(); diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index a69493ee0..88a5c2317 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -83,7 +83,7 @@ public: void pivot(ArithVar x_j); - void subsitute(Row& row_s); + void substitute(Row& row_s); void printRow(); }; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 26bb58e90..ac3dc3d40 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -22,6 +22,8 @@ #include "expr/metakind.h" #include "expr/node_builder.h" +#include "theory/theory_engine.h" + #include "util/rational.h" #include "util/integer.h" @@ -927,3 +929,77 @@ void TheoryArith::propagate(Effort e) { } } } + +Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { + NodeManager* nodeManager = NodeManager::currentNM(); + + switch(n.getKind()) { + case kind::VARIABLE: { + DeltaRational drat = d_partialModel.getAssignment(asArithVar(n)); + // FIXME our infinitesimal is fixed here at 1e-06 + return nodeManager-> + mkConst( drat.getNoninfinitesimalPart() + + drat.getInfinitesimalPart() * Rational(1, 1000000) ); + } + + case kind::EQUAL: // 2 args + return nodeManager-> + mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + + case kind::PLUS: { // 2+ args + Rational value = d_constants.d_ZERO; + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + value += engine->getValue(*i).getConst<Rational>(); + } + return nodeManager->mkConst(value); + } + + case kind::MULT: { // 2+ args + Rational value = d_constants.d_ONE; + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + value *= engine->getValue(*i).getConst<Rational>(); + } + return nodeManager->mkConst(value); + } + + case kind::MINUS: // 2 args + // should have been rewritten + Unreachable(); + + case kind::UMINUS: // 1 arg + // should have been rewritten + Unreachable(); + + case kind::DIVISION: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() / + engine->getValue(n[1]).getConst<Rational>() ); + + case kind::IDENTITY: // 1 arg + return engine->getValue(n[0]); + + case kind::LT: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() < + engine->getValue(n[1]).getConst<Rational>() ); + + case kind::LEQ: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <= + engine->getValue(n[1]).getConst<Rational>() ); + + case kind::GT: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() > + engine->getValue(n[1]).getConst<Rational>() ); + + case kind::GEQ: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() >= + engine->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 cbfdf27f3..26dcc9825 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -128,6 +128,8 @@ public: void propagate(Effort e); void explain(TNode n, Effort e); + Node getValue(TNode n, TheoryEngine* engine); + void shutdown(){ } std::string identify() const { return std::string("TheoryArith"); } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 8997138cb..55a539f44 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -18,6 +18,7 @@ #include "theory/arrays/theory_arrays.h" +#include "theory/theory_engine.h" #include "expr/kind.h" @@ -58,3 +59,20 @@ void TheoryArrays::check(Effort e) { } Debug("arrays") << "TheoryArrays::check(): done" << endl; } + +Node TheoryArrays::getValue(TNode n, TheoryEngine* engine) { + NodeManager* nodeManager = NodeManager::currentNM(); + + switch(n.getKind()) { + + case kind::VARIABLE: + Unhandled(kind::VARIABLE); + + case kind::EQUAL: // 2 args + return nodeManager-> + mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + + default: + Unhandled(n.getKind()); + } +} diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index cb738d085..89631d59f 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -53,6 +53,7 @@ public: void check(Effort e); void propagate(Effort e) { } void explain(TNode n, Effort e) { } + Node getValue(TNode n, TheoryEngine* engine); 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 a7e343fdc..b1ff472ac 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -18,12 +18,12 @@ #include "theory/theory.h" #include "theory/booleans/theory_bool.h" +#include "theory/theory_engine.h" namespace CVC4 { namespace theory { namespace booleans { - RewriteResponse TheoryBool::preRewrite(TNode n, bool topLevel) { if(n.getKind() == kind::IFF) { NodeManager* nodeManager = NodeManager::currentNM(); @@ -140,6 +140,70 @@ RewriteResponse TheoryBool::postRewrite(TNode n, bool topLevel) { return RewriteComplete(n); } +Node TheoryBool::getValue(TNode n, TheoryEngine* engine) { + NodeManager* nodeManager = NodeManager::currentNM(); + + switch(n.getKind()) { + case kind::VARIABLE: + // case for Boolean vars is implemented in TheoryEngine (since it + // appeals to the PropEngine to get the value) + Unreachable(); + + case kind::EQUAL: // 2 args + // should be handled by IFF + Unreachable(); + + case kind::NOT: // 1 arg + return nodeManager->mkConst(! engine->getValue(n[0]).getConst<bool>()); + + case kind::AND: { // 2+ args + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + if(! engine->getValue(*i).getConst<bool>()) { + return nodeManager->mkConst(false); + } + } + return nodeManager->mkConst(true); + } + + case kind::IFF: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() == + engine->getValue(n[1]).getConst<bool>() ); + + case kind::IMPLIES: // 2 args + return nodeManager->mkConst( (! engine->getValue(n[0]).getConst<bool>()) || + engine->getValue(n[1]).getConst<bool>() ); + + case kind::OR: { // 2+ args + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + if(engine->getValue(*i).getConst<bool>()) { + return nodeManager->mkConst(true); + } + } + return nodeManager->mkConst(false); + } + + case kind::XOR: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() != + engine->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( engine->getValue(n[0]).getConst<bool>() ? + engine->getValue(n[1]).getConst<bool>() : + engine->getValue(n[2]).getConst<bool>() ); + + default: + Unhandled(n.getKind()); + } +} }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index d87aa95b5..2c77c09b3 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -46,6 +46,8 @@ public: void propagate(Effort e) { Unimplemented(); } void explain(TNode n, Effort e) { Unimplemented(); } + Node getValue(TNode n, TheoryEngine* engine); + RewriteResponse preRewrite(TNode n, bool topLevel); RewriteResponse postRewrite(TNode n, bool topLevel); diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index ba258aafd..810cd1d39 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -17,6 +17,7 @@ **/ #include "theory/builtin/theory_builtin.h" +#include "theory/theory_engine.h" #include "expr/kind.h" using namespace std; @@ -26,7 +27,8 @@ namespace theory { namespace builtin { Node TheoryBuiltin::blastDistinct(TNode in) { - Debug("theory-rewrite") << "TheoryBuiltin::blastDistinct: " << in << std::endl; + Debug("theory-rewrite") << "TheoryBuiltin::blastDistinct: " + << in << std::endl; Assert(in.getKind() == kind::DISTINCT); if(in.getNumChildren() == 2) { // if this is the case exactly 1 != pair will be generated so the @@ -67,6 +69,40 @@ RewriteResponse TheoryBuiltin::preRewrite(TNode in, bool topLevel) { } } +Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) { + switch(n.getKind()) { + + case kind::VARIABLE: + // no variables that the builtin theory is responsible for + Unreachable(); + + case kind::EQUAL: { // 2 args + // has to be an EQUAL over tuples, since all others should be + // handled elsewhere + Assert(n[0].getKind() == kind::TUPLE && + n[1].getKind() == kind::TUPLE); + return NodeManager::currentNM()-> + mkConst( getValue(n[0], engine) == getValue(n[1], engine) ); + } + + case kind::TUPLE: { // 2+ args + NodeBuilder<> nb(kind::TUPLE); + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + nb << engine->getValue(*i); + } + return Node(nb); + } + + default: + // all other "builtins" should have been rewritten away or handled + // by theory engine, or handled elsewhere. + Unhandled(n.getKind()); + } +} + }/* CVC4::theory::builtin namespace */ }/* CVC4::theory */ }/* CVC4 namespace */ diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index a08ed9b78..57c5d1558 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -39,6 +39,7 @@ public: void check(Effort e) { Unreachable(); } void propagate(Effort e) { Unreachable(); } void explain(TNode n, Effort e) { Unreachable(); } + Node getValue(TNode n, TheoryEngine* engine); void shutdown() { } RewriteResponse preRewrite(TNode n, bool topLevel); std::string identify() const { return std::string("TheoryBuiltin"); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index bd0d73865..69ff48721 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -17,9 +17,11 @@ ** \todo document this file **/ -#include "theory_bv.h" -#include "theory_bv_utils.h" -#include "theory_bv_rewrite_rules.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/bv/theory_bv_rewrite_rules.h" + +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::theory; @@ -160,3 +162,19 @@ bool TheoryBV::triggerEquality(size_t triggerId) { return true; } +Node TheoryBV::getValue(TNode n, TheoryEngine* engine) { + NodeManager* nodeManager = NodeManager::currentNM(); + + switch(n.getKind()) { + + case kind::VARIABLE: + Unhandled(kind::VARIABLE); + + case kind::EQUAL: // 2 args + return nodeManager-> + mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + + default: + Unhandled(n.getKind()); + } +} diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index ff5d4c2a2..c673a56b4 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -75,6 +75,8 @@ public: void explain(TNode n, Effort e) { } + Node getValue(TNode n, TheoryEngine* engine); + RewriteResponse postRewrite(TNode n, bool topLevel); std::string identify() const { return std::string("TheoryBV"); } diff --git a/src/theory/theory.h b/src/theory/theory.h index 2711a0b95..df9dcafef 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -262,9 +262,11 @@ public: // TODO add compiler annotation "constant function" here static bool minEffortOnly(Effort e) { return e == MIN_EFFORT; } static bool quickCheckOrMore(Effort e) { return e >= QUICK_CHECK; } - static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK && e < STANDARD; } + static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK && + e < STANDARD; } static bool standardEffortOrMore(Effort e) { return e >= STANDARD; } - static bool standardEffortOnly(Effort e) { return e >= STANDARD && e < FULL_EFFORT; } + static bool standardEffortOnly(Effort e) { return e >= STANDARD && + e < FULL_EFFORT; } static bool fullEffort(Effort e) { return e >= FULL_EFFORT; } /** @@ -328,7 +330,8 @@ public: * (ITE true x y). */ virtual RewriteResponse preRewrite(TNode n, bool topLevel) { - Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl; + Debug("theory-rewrite") << "no pre-rewriting to perform for " + << n << std::endl; return RewriteComplete(n); } @@ -340,7 +343,8 @@ public: * memory leakage). */ virtual RewriteResponse postRewrite(TNode n, bool topLevel) { - Debug("theory-rewrite") << "no post-rewriting to perform for " << n << std::endl; + Debug("theory-rewrite") << "no post-rewriting to perform for " + << n << std::endl; return RewriteComplete(n); } @@ -366,18 +370,21 @@ public: } /** - * This method is called to notify a theory that the node n should be considered a "shared term" by this theory + * This method is called to notify a theory that the node n should + * be considered a "shared term" by this theory */ virtual void addSharedTerm(TNode n) { } /** - * This method is called by the shared term manager when a shared term lhs - * which this theory cares about (either because it received a previous - * addSharedTerm call with lhs or because it received a previous notifyEq call - * with lhs as the second argument) becomes equal to another shared term rhs. - * This call also serves as notice to the theory that the shared term manager - * now considers rhs the representative for this equivalence class of shared - * terms, so future notifications for this class will be based on rhs not lhs. + * This method is called by the shared term manager when a shared + * term lhs which this theory cares about (either because it + * received a previous addSharedTerm call with lhs or because it + * received a previous notifyEq call with lhs as the second + * argument) becomes equal to another shared term rhs. This call + * also serves as notice to the theory that the shared term manager + * now considers rhs the representative for this equivalence class + * of shared terms, so future notifications for this class will be + * based on rhs not lhs. */ virtual void notifyEq(TNode lhs, TNode rhs) { } @@ -405,6 +412,38 @@ public: virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0; /** + * Return the value of a node (typically used after a ). If the + * theory supports model generation but has no value for this node, + * it should return Node::null(). If the theory doesn't support + * model generation at all, or usually would but doesn't in its + * current state, it should throw an exception saying so. + * + * The TheoryEngine is passed in so that you can recursively request + * values for the Node's children. This is important because the + * TheoryEngine takes care of simple cases (metakind CONSTANT, + * Boolean-valued VARIABLES, ...) and can dispatch to other theories + * if that's necessary. Only call your own getValue() recursively + * if you *know* that you are responsible handle the Node you're + * asking for; other theories can use your types, so be careful + * here! To be safe, it's best to delegate back to the + * TheoryEngine. + * + * Usually, you need to handle at least the two cases of EQUAL and + * VARIABLE---EQUAL in case a value of yours is on the LHS of an + * EQUAL, and VARIABLE for variables of your types. You also need + * to support any operators that can survive your rewriter. You + * don't need to handle constants, as they are handled by the + * TheoryEngine. + * + * There are some gotchas here. The user may be requesting the + * value of an expression that wasn't part of the satisfiable + * assertion, or has been declared since. If you don't have a value + * and suspect this situation is the case, return Node::null() + * rather than throwing an exception. + */ + virtual Node getValue(TNode n, TheoryEngine* engine) = 0; + + /** * Identify this theory (for debugging, dynamic configuration, * etc..) */ @@ -550,7 +589,8 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level); }/* CVC4::theory namespace */ -inline std::ostream& operator<<(std::ostream& out, const CVC4::theory::Theory& theory) { +inline std::ostream& operator<<(std::ostream& out, + const CVC4::theory::Theory& theory) { return out << theory.identify(); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 041b6852b..388167e00 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -537,4 +537,20 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) { return out; }/* TheoryEngine::rewrite(TNode in) */ + +Node TheoryEngine::getValue(TNode node) { + kind::MetaKind metakind = node.getMetaKind(); + // special case: prop engine handles boolean vars + if(metakind == kind::metakind::VARIABLE && node.getType().isBoolean()) { + return d_propEngine->getValue(node); + } + // special case: value of a constant == itself + if(metakind == kind::metakind::CONSTANT) { + return node; + } + + // otherwise ask the theory-in-charge + return theoryOf(node)->getValue(node, this); +}/* TheoryEngine::getValue(TNode node) */ + }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5227d32f0..0eaf61055 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -380,7 +380,7 @@ public: return d_theoryOut.d_explanationNode; } - inline Node getExplanation(TNode node){ + inline Node getExplanation(TNode node) { d_theoryOut.d_explanationNode = Node::null(); theory::Theory* theory = node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node); @@ -388,6 +388,8 @@ public: return d_theoryOut.d_explanationNode; } + Node getValue(TNode node); + private: class Statistics { public: diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index eb6c430ba..a1eec9d4c 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -17,6 +17,7 @@ **/ #include "theory/uf/morgan/theory_uf_morgan.h" +#include "theory/theory_engine.h" #include "expr/kind.h" #include "util/congruence_closure.h" @@ -451,6 +452,32 @@ void TheoryUFMorgan::propagate(Effort level) { Debug("uf") << "uf: end propagate(" << level << ")" << std::endl; } +Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) { + NodeManager* nodeManager = NodeManager::currentNM(); + + switch(n.getKind()) { + + case kind::VARIABLE: + case kind::APPLY_UF: + if(n.getType().isBoolean()) { + if(d_cc.areCongruent(d_trueNode, n)) { + return nodeManager->mkConst(true); + } else if(d_cc.areCongruent(d_trueNode, n)) { + return nodeManager->mkConst(false); + } + return Node::null(); + } + return d_cc.normalize(n); + + case kind::EQUAL: // 2 args + return nodeManager-> + mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + + default: + Unhandled(n.getKind()); + } +} + void TheoryUFMorgan::dump() { if(!Debug.isOn("uf")) { return; diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index d17eb87f5..7a12f216b 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -151,13 +151,21 @@ public: void propagate(Effort level); /** - * Explains a previously reported conflict. Currently does nothing. + * Explains a previously theory-propagated literal. * * Overloads void explain(TNode n, Effort level); from theory.h. * See theory/theory.h for more information about this method. */ void explain(TNode n, Effort level) {} + /** + * Gets a theory value. + * + * Overloads Node getValue(TNode n); from theory.h. + * See theory/theory.h for more information about this method. + */ + Node getValue(TNode n, TheoryEngine* engine); + std::string identify() const { return std::string("TheoryUFMorgan"); } private: diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h index 9a2d252c0..4c8a1a71a 100644 --- a/src/theory/uf/tim/theory_uf_tim.h +++ b/src/theory/uf/tim/theory_uf_tim.h @@ -156,6 +156,16 @@ public: */ void explain(TNode n, Effort level) {} + /** + * Get a theory value. + * + * Overloads Node getValue(TNode n); from theory.h. + * See theory/theory.h for more information about this method. + */ + Node getValue(TNode n, TheoryEngine* engine) { + Unimplemented("TheoryUFTim doesn't support model generation"); + } + std::string identify() const { return std::string("TheoryUFTim"); } private: |