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, 23 insertions, 3 deletions

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