Model generation for arith, boolean, and uf theories via

(get-value ...) SMT-LIBv2 command.  As per SMT-LIBv2 spec,
you must pass --interactive --produce-models on the command
line (although they don't currently make us do any extra
work).  Closes bug #213.

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: