summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/command.cpp31
-rw-r--r--src/expr/command.h5
-rw-r--r--src/expr/expr_template.cpp2
-rw-r--r--src/expr/expr_template.h2
-rw-r--r--src/expr/node_manager.h2
-rw-r--r--src/parser/smt2/Smt2.g14
-rw-r--r--src/printer/ast/ast_printer.cpp5
-rw-r--r--src/printer/cvc/cvc_printer.cpp5
-rw-r--r--src/printer/smt2/smt2_printer.cpp5
-rw-r--r--src/theory/builtin/kinds4
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<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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback