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

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 7f10c533ed68b29c94776cd0b5261a54e7c53f7f..f93df3722f757174a31d2fd7c1a54828356a254e 100644 (file)
--- 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 24281757579171fe7025648bb2373c25aedc4fed..2c56e60d9d514f030ec923b51bd37877bc8d9416 100644 (file)
--- 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 f88914fd269f84f33200b7b6f609e37fa27037a4..b0364348cd0e323d0ceb49e3ea5711b6bdc91fb8 100644 (file)
--- 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 a2e861118eb625cf83a2e42e2e46226c0440c5cb..e1b5cc4e671f861042189541e0200540d8ae99df 100644 (file)
--- 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 bad20b3b65f94e6c0c51cecfec81dde81a409e4c..18b60738f953ff1d2da16cd600866f9846408659 100644 (file)
--- 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,

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index dd0ccb0add319d65817ead681d72574c4b5408c4..456e3c656146b08be615c22bdb80b9d582fcbc59 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -283,19 +283,7 @@ command returns [CVC4::Command* cmd = NULL]
   | /* value query */
     GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     LPAREN_TOK termList[terms,expr] RPAREN_TOK
-    { if(terms.size() == 1) {
-        $cmd = new GetValueCommand(terms[0]);
-      } else {
-        CommandSequence* seq = new CommandSequence();
-        for(std::vector<Expr>::const_iterator i = terms.begin(),
-              iend = terms.end();
-            i != iend;
-            ++i) {
-          seq->addCommand(new GetValueCommand(*i));
-        }
-        $cmd = seq;
-      }
-    }
+    { $cmd = new GetValueCommand(terms); }
   | /* get-assignment */
     GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { cmd = new GetAssignmentCommand; }

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 479c26aafc22aa2fc484c73d9be8491f765ce488..48f773c548d8af04094ca268a05719283570c670 100644 (file)
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -288,7 +288,10 @@ static void toStream(std::ostream& out, const SimplifyCommand* c) throw() {
 }
 
 static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
-  out << "GetValue( << " << c->getTerm() << " >> )";
+  out << "GetValue( << ";
+  const vector<Expr>& terms = c->getTerms();
+  copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", "));
+  out << " >> )";
 }
 
 static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 8121085d3e414b91e38172dcb4a674f9c7180719..6a709b83339a2f3fd380601678fcffdc1f575698 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -835,7 +835,10 @@ static void toStream(std::ostream& out, const SimplifyCommand* c) throw() {
 }
 
 static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
-  out << "% (get-value " << c->getTerm() << ")";
+  out << "% (get-value ( ";
+  const vector<Expr>& terms = c->getTerms();
+  copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
+  out << " ))";
 }
 
 static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index ef8c8fcbc62bc28d8c2f661ba5ab99ec44a2bbf3..ed8648c475a83e5641bb5b86e4e0913f7fecb0bc 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -643,7 +643,10 @@ static void toStream(std::ostream& out, const SimplifyCommand* c) throw() {
 }
 
 static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
-  out << "(get-value " << c->getTerm() << ")";
+  out << "(get-value ( ";
+  const vector<Expr>& terms = c->getTerms();
+  copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
+  out << " ))";
 }
 
 static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index e521961631779269f5954f0f95072924a42c6adf..285eb651f5f8cd0c3ca8780c647f263c931c20ef 100644 (file)
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -295,7 +295,7 @@ operator EQUAL 2 "equality"
 operator DISTINCT 2: "disequality"
 variable SKOLEM "skolem var"
 variable VARIABLE "variable"
-operator TUPLE 2: "a tuple"
+operator TUPLE 1: "a tuple"
 
 constant TYPE_CONSTANT \
     ::CVC4::TypeConstant \
@@ -307,7 +307,7 @@ cardinality FUNCTION_TYPE \
     "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 well-founded FUNCTION_TYPE false
-operator TUPLE_TYPE 2: "tuple type"
+operator TUPLE_TYPE 1: "tuple type"
 cardinality TUPLE_TYPE \
     "::CVC4::theory::builtin::TupleProperties::computeCardinality(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"