From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 24 Aug 2012 00:29:52 +0000 (+0000)
Subject: fix get-value output in a couple ways; this fixes bug #378
X-Git-Tag: cvc5-1.0.0~7850
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9de66957df6448ba1243cdb7cc84813fe82e69d5;p=cvc5.git

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 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,
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index dd0ccb0ad..456e3c656 100644
--- 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 479c26aaf..48f773c54 100644
--- 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 8121085d3..6a709b833 100644
--- 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 ef8c8fcbc..ed8648c47 100644
--- 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 e52196163..285eb651f 100644
--- 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"