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.

2 files changed, 38 insertions, 1 deletions

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"); }