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.

1 files changed, 14 insertions, 0 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c49d5f38a..961a18bdb 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -130,6 +130,20 @@ Result PropEngine::checkSat() {
   return Result(result ? Result::SAT : Result::UNSAT);
 }
 
+Node PropEngine::getValue(TNode node) {
+  Assert(node.getKind() == kind::VARIABLE &&
+         node.getType().isBoolean());
+  SatLiteralValue v = d_satSolver->value(d_cnfStream->getLiteral(node));
+  if(v == l_True) {
+    return NodeManager::currentNM()->mkConst(true);
+  } else if(v == l_False) {
+    return NodeManager::currentNM()->mkConst(false);
+  } else {
+    Assert(v == l_Undef);
+    return Node::null();
+  }
+}
+
 void PropEngine::push() {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "push()" << endl;