From 9de66957df6448ba1243cdb7cc84813fe82e69d5 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 24 Aug 2012 00:29:52 +0000 Subject: [PATCH] fix get-value output in a couple ways; this fixes bug #378 --- src/expr/command.cpp | 31 ++++++++++++++++++++++++------- src/expr/command.h | 5 +++-- src/expr/expr_template.cpp | 2 +- src/expr/expr_template.h | 2 +- src/expr/node_manager.h | 2 +- src/parser/smt2/Smt2.g | 14 +------------- src/printer/ast/ast_printer.cpp | 5 ++++- src/printer/cvc/cvc_printer.cpp | 5 ++++- src/printer/smt2/smt2_printer.cpp | 5 ++++- src/theory/builtin/kinds | 4 ++-- 10 files changed, 45 insertions(+), 30 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& terms) throw() : + d_terms(terms) { + CheckArgument(terms.size() >= 1, terms, "cannot get-value of an empty set of terms"); +} + +const std::vector& 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 result; + NodeManager* nm = NodeManager::fromExprManager(smtEngine->getExprManager()); + for(std::vector::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 exportedTerms; + for(std::vector::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 d_terms; Expr d_result; public: GetValueCommand(Expr term) throw(); + GetValueCommand(const std::vector& terms) throw(); ~GetValueCommand() throw() {} - Expr getTerm() const throw(); + const std::vector& 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& sorts) { } inline TypeNode NodeManager::mkTupleType(const std::vector& types) { - Assert(types.size() >= 2); + Assert(types.size() >= 1); std::vector 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::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& terms = c->getTerms(); + copy(terms.begin(), terms.end(), ostream_iterator(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& terms = c->getTerms(); + copy(terms.begin(), terms.end(), ostream_iterator(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& terms = c->getTerms(); + copy(terms.begin(), terms.end(), ostream_iterator(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" -- 2.30.2