Return choice functions for approximate values in get-value (#3304)

5 files changed, 30 insertions, 13 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index e9e8f2ea0..37a73db2d 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -541,8 +541,7 @@ void Smt2Printer::toStream(std::ostream& out,
     return;
 
   case kind::LAMBDA:
-    out << smtKindString(k, d_variant) << " ";
-    break;
+  case kind::CHOICE: out << smtKindString(k, d_variant) << " "; break;
 
   // arith theory
   case kind::PLUS:
@@ -1026,6 +1025,7 @@ static string smtKindString(Kind k, Variant v)
 
   case kind::LAMBDA:
     return "lambda";
+  case kind::CHOICE: return "choice";
 
   // arith theory
   case kind::PLUS: return "+";
@@ -1345,15 +1345,8 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const
   }
   //print the model
   out << "(model" << endl;
-  // print approximations
-  if (m.hasApproximations())
-  {
-    std::vector<std::pair<Expr, Expr> > approx = m.getApproximations();
-    for (unsigned i = 0, size = approx.size(); i < size; i++)
-    {
-      out << "(approximation " << approx[i].second << ")" << std::endl;
-    }
-  }
+  // don't need to print approximations since they are built into choice
+  // functions in the values of variables.
   this->Printer::toStream(out, m);
   out << ")" << endl;
   //print the heap model, if it exists
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fa318aaf1..305c36d13 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4212,8 +4212,10 @@ Expr SmtEngine::getValue(const Expr& ex) const
              || resultNode.getType().isSubtypeOf(expectedType),
          "Run with -t smt for details.");
 
-  // ensure it's a constant
-  Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst());
+  // Ensure it's a constant, or a lambda (for uninterpreted functions), or
+  // a choice (for approximate values).
+  Assert(resultNode.getKind() == kind::LAMBDA
+         || resultNode.getKind() == kind::CHOICE || resultNode.isConst());
 
   if(options::abstractValues() && resultNode.getType().isArray()) {
     resultNode = d_private->mkAbstractValue(resultNode);
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index e0798aa3c..f65d3a203 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -256,6 +256,18 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
     d_modelCache[n] = ret;
     return ret;
   }
+  // it might be approximate
+  std::map<Node, Node>::const_iterator ita = d_approximations.find(n);
+  if (ita != d_approximations.end())
+  {
+    // If the value of n is approximate based on predicate P(n), we return
+    // choice z. P(z).
+    Node v = nm->mkBoundVar(n.getType());
+    Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
+    Node ret = nm->mkNode(CHOICE, bvl, ita->second.substitute(n, v));
+    d_modelCache[n] = ret;
+    return ret;
+  }
   // must rewrite the term at this point
   ret = Rewriter::rewrite(n);
   // return the representative of the term in the equality engine, if it exists
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a97670446..6dc44e314 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -540,6 +540,7 @@ set(regress_0_tests
   regress0/nl/nta/tan-rewrite.smt2
   regress0/nl/real-as-int.smt2
   regress0/nl/real-div-ufnra.smt2
+  regress0/nl/sqrt2-value.smt2
   regress0/nl/subs0-unsat-confirm.smt2
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
diff --git a/test/regress/regress0/nl/sqrt2-value.smt2 b/test/regress/regress0/nl/sqrt2-value.smt2
new file mode 100644
index 000000000..649a792be
--- /dev/null
+++ b/test/regress/regress0/nl/sqrt2-value.smt2
@@ -0,0 +1,9 @@
+; SCRUBBER: sed -e 's/choice.*/choice/'
+; EXPECT: sat
+; EXPECT: ((x (choice
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun x () Real)
+(assert (= (* x x) 2))
+(check-sat)
+(get-value (x))