Fix interface for bindingsnext_model_cherry_fix

3 files changed, 15 insertions, 25 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index f648dcdea..f2d8c48f0 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1663,35 +1663,24 @@ void GetValueCommand::invoke(SmtEngine* smtEngine)
   try
   {
     ExprManager* em = smtEngine->getExprManager();
-    NodeManager* nm = NodeManager::fromExprManager(em);
     smt::SmtScope scope(smtEngine);
-    vector<Node> termNodes;
-    for (Expr e : d_terms)  {
-      termNodes.push_back(Node::fromExpr(e));
-    }
-    vector<Node> result = smtEngine->getValues(termNodes);
+    vector<Expr> result = smtEngine->getValues(d_terms);
     Assert(result.size() == d_terms.size());
-    for (int i=0; i < d_terms.size(); i++) 
+    for (size_t i=0; i < d_terms.size(); i++)
     {
       Expr e = d_terms[i];
-      Assert(nm == NodeManager::fromExprManager(e.getExprManager()));
-      Node request = Node::fromExpr( options::expandDefinitions()
-          ? smtEngine->expandDefinitions(e) : e);
-      Node value = result[i];
-      if (value.getType().isInteger() && request.getType() == nm->realType())
+      Expr request = options::expandDefinitions() ? smtEngine->expandDefinitions(e) : e;
+      Expr value = result[i];
+      if (value.getType().isInteger() && request.getType() == em->realType())
       {
         // Need to wrap in division-by-one so that output printers know this
         // is an integer-looking constant that really should be output as
         // a rational.  Necessary for SMT-LIB standards compliance.
-        value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1)));
+        value = em->mkExpr(kind::DIVISION, value, em->mkConst(Rational(1)));
       }
-      result[i] = nm->mkNode(kind::SEXPR, request, value);
-    }
-    std::vector<Expr> resultExpr;
-    for (Node n : result) {
-      resultExpr.push_back(n.toExpr());
+      result[i] = em->mkExpr(kind::SEXPR, request, value);
     }
-    d_result = em->mkExpr(kind::SEXPR, resultExpr);
+    d_result = em->mkExpr(kind::SEXPR, result);
     d_commandStatus = CommandSuccess::instance();
   }
   catch (RecoverableModalException& e)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index aefe17584..7a4c94cb0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4208,11 +4208,12 @@ Expr SmtEngine::getValue(const Expr& ex) const
   return resultNode.toExpr();
 }
 
-vector<Node> SmtEngine::getValues(const vector<Node>& nodes) {
-  vector<Node> result;
-  for (Node n : nodes) {
-    Node value = Node::fromExpr(getValue(n.toExpr()));
-    result.push_back(value);
+vector<Expr> SmtEngine::getValues(const vector<Expr>& exprs) {
+  vector<Expr> result;
+  vector<Node> nodes;
+  for (Expr e : exprs) {
+    nodes.push_back(Node::fromExpr(e));
+    result.push_back(getValue(e));
   }
 
   if (options::blockModelsMode() != BLOCK_MODELS_NONE)
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index d6ace0ae1..93bfc69ab 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -745,7 +745,7 @@ class CVC4_PUBLIC SmtEngine {
   /**
    * Same as getValue but for a vector of expressions
    */
-  std::vector<Node> getValues(const std::vector<Node>& nodes);
+  std::vector<Expr> getValues(const std::vector<Expr>& exprs);
 
 
   /**