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.

6 files changed, 89 insertions, 11 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"); }