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.

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: