fix get-value output in a couple ways; this fixes bug #378

5 files changed, 30 insertions, 12 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 7f10c533e..f93df3722 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -686,17 +686,29 @@ Command* SimplifyCommand::clone() const {
 /* class GetValueCommand */
 
 GetValueCommand::GetValueCommand(Expr term) throw() :
-  d_term(term) {
+  d_terms() {
+  d_terms.push_back(term);
 }
 
-Expr GetValueCommand::getTerm() const throw() {
-  return d_term;
+GetValueCommand::GetValueCommand(const std::vector<Expr>& terms) throw() :
+  d_terms(terms) {
+  CheckArgument(terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
+}
+
+const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
+  return d_terms;
 }
 
 void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
-    d_result = d_term.getExprManager()->mkExpr(kind::TUPLE, d_term,
-                                               smtEngine->getValue(d_term));
+    vector<Node> result;
+    NodeManager* nm = NodeManager::fromExprManager(smtEngine->getExprManager());
+    for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
+      Assert(nm == NodeManager::fromExprManager((*i).getExprManager()));
+      result.push_back(nm->mkNode(kind::TUPLE, Node::fromExpr(*i), Node::fromExpr(smtEngine->getValue(*i))));
+    }
+    Node n = nm->mkNode(kind::TUPLE, result);
+    d_result = nm->toExpr(n);
     d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
@@ -711,18 +723,23 @@ void GetValueCommand::printResult(std::ostream& out) const throw() {
   if(! ok()) {
     this->Command::printResult(out);
   } else {
+    Expr::dag::Scope scope(out, false);
     out << d_result << endl;
   }
 }
 
 Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  GetValueCommand* c = new GetValueCommand(d_term.exportTo(exprManager, variableMap));
+  vector<Expr> exportedTerms;
+  for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
+    exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
+  }
+  GetValueCommand* c = new GetValueCommand(exportedTerms);
   c->d_result = d_result.exportTo(exprManager, variableMap);
   return c;
 }
 
 Command* GetValueCommand::clone() const {
-  GetValueCommand* c = new GetValueCommand(d_term);
+  GetValueCommand* c = new GetValueCommand(d_terms);
   c->d_result = d_result;
   return c;
 }
diff --git a/src/expr/command.h b/src/expr/command.h
index 242817575..2c56e60d9 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -438,12 +438,13 @@ public:
 
 class CVC4_PUBLIC GetValueCommand : public Command {
 protected:
-  Expr d_term;
+  std::vector<Expr> d_terms;
   Expr d_result;
 public:
   GetValueCommand(Expr term) throw();
+  GetValueCommand(const std::vector<Expr>& terms) throw();
   ~GetValueCommand() throw() {}
-  Expr getTerm() const throw();
+  const std::vector<Expr>& getTerms() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Expr getResult() const throw();
   void printResult(std::ostream& out) const throw();
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index f88914fd2..b0364348c 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -168,7 +168,7 @@ Debug("export") << "+ child: " << *i << std::endl;
 
 }/* CVC4::expr namespace */
 
-Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) const {
   Assert(d_exprManager != exprManager,
          "No sense in cloning an Expr in the same ExprManager");
   ExprManagerScope ems(*this);
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index a2e861118..e1b5cc4e6 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -461,7 +461,7 @@ public:
    * variableMap for the translation and extending it with any new
    * mappings.
    */
-  Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) const;
 
   /**
    * IOStream manipulator to set the maximum depth of Exprs when
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index bad20b3b6..18b60738f 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -976,7 +976,7 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
 }
 
 inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
-  Assert(types.size() >= 2);
+  Assert(types.size() >= 1);
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {
     CheckArgument(!types[i].isFunctionLike(), types,