diff options
Diffstat (limited to 'src/theory/uf')
-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 |
3 files changed, 46 insertions, 1 deletions
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: |