diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-24 00:29:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-24 00:29:52 +0000 |
commit | 9de66957df6448ba1243cdb7cc84813fe82e69d5 (patch) | |
tree | 9c013455d7f0c0e057f44f51abdead7ff1ebd01c /src/expr | |
parent | 23367b1eac54a17a060697b1cf187ad2cc2ff503 (diff) |
fix get-value output in a couple ways; this fixes bug #378
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 31 | ||||
-rw-r--r-- | src/expr/command.h | 5 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr_template.h | 2 | ||||
-rw-r--r-- | src/expr/node_manager.h | 2 |
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, |