diff options
author | François Bobot <francois@bobot.eu> | 2012-07-27 13:36:32 +0000 |
---|---|---|
committer | François Bobot <francois@bobot.eu> | 2012-07-27 13:36:32 +0000 |
commit | 4bfa927dac67bbcadf219f70e61f1d123e33944b (patch) | |
tree | f295343430799748de8b9a823f1a3c641c096905 /src/expr | |
parent | 988c97d92fa617c5dccaeb1ef33121bfa6459afc (diff) |
Merge quantifiers2-trunk:
- new syntax for rewrite rules
- better rewrite rules theory
- remove the rewriting with rewrite rules during ppRewrite temporarily
- theory can define their own candidate generator
- define a general candidate generator (inefficient ask to every theory)
- split inst_match between the pattern matching used for quantifiers (inst_match.*) and
the one used for rewrite rules (rr_inst_match.*):
- the pattern matching is less exhaustive for quantifiers,
- the one for rewrite rules can use efficient-e-matching.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 213 | ||||
-rw-r--r-- | src/expr/command.h | 63 | ||||
-rw-r--r-- | src/expr/node.h | 19 |
3 files changed, 295 insertions, 0 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index f4b40cbb3..12830a618 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1137,6 +1137,219 @@ Command* DatatypeDeclarationCommand::clone() const { return new DatatypeDeclarationCommand(d_datatypes); } +/* class RewriteRuleCommand */ + +RewriteRuleCommand::RewriteRuleCommand(const VExpr & vars, + const std::vector< Expr> & guards, + const Expr & head, const Expr & body, + Triggers triggers) throw() : + d_vars(vars), d_guards(guards), d_head(head), d_body(body), d_triggers(triggers) { +} + +RewriteRuleCommand::RewriteRuleCommand(const VExpr & vars, + const Expr & head, const Expr & body) throw() : + d_vars(vars), d_head(head), d_body(body) { +} + +const RewriteRuleCommand::VExpr & RewriteRuleCommand::getVars() const throw(){ + return d_vars; +}; +const RewriteRuleCommand::VExpr & RewriteRuleCommand::getGuards() const throw(){ + return d_guards; +}; +const Expr & RewriteRuleCommand::getHead() const throw(){ + return d_head; +}; +const Expr & RewriteRuleCommand::getBody() const throw(){ + return d_body; +}; +const RewriteRuleCommand::Triggers & RewriteRuleCommand::getTriggers() const throw(){ + return d_triggers; +}; + + +void RewriteRuleCommand::invoke(SmtEngine* smtEngine) throw() { + try { + ExprManager* em = smtEngine->getExprManager(); + /** build vars list */ + Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); + /** build guards list */ + Expr guards; + if(d_guards.size() == 0) guards = em->mkConst<bool>(true); + else if(d_guards.size() == 1) guards = d_guards[0]; + else guards = em->mkExpr(kind::AND,d_guards); + /** build expression */ + Expr expr; + if( d_triggers.empty() ){ + expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body); + } else { + /** build triggers list */ + std::vector<Expr> vtriggers; + vtriggers.reserve(d_triggers.size()); + for(Triggers::const_iterator i = d_triggers.begin(), + end = d_triggers.end(); i != end; ++i){ + vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i)); + } + Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers); + expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body,triggers); + } + smtEngine->assertFormula(expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + /** Convert variables */ + VExpr vars; vars.reserve(d_vars.size()); + for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); + i == end; ++i){ + vars.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert guards */ + VExpr guards; guards.reserve(d_guards.size()); + for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); + i == end; ++i){ + guards.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert triggers */ + Triggers triggers; triggers.resize(d_triggers.size()); + for(size_t i = 0, end = d_triggers.size(); + i < end; ++i){ + triggers[i].reserve(d_triggers[i].size()); + for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); + j == jend; ++i){ + triggers[i].push_back(j->exportTo(exprManager, variableMap)); + }; + }; + /** Convert head and body */ + Expr head = d_head.exportTo(exprManager, variableMap); + Expr body = d_body.exportTo(exprManager, variableMap); + /** Create the converted rules */ + return new RewriteRuleCommand(vars,guards,head,body,triggers); +} + +Command* RewriteRuleCommand::clone() const { + return new RewriteRuleCommand(d_vars,d_guards,d_head,d_body,d_triggers); +} + +/* class PropagateRuleCommand */ + +PropagateRuleCommand::PropagateRuleCommand(const VExpr & vars, + const VExpr & guards, + const VExpr & heads, + const Expr & body, + const Triggers triggers, + bool deduction + ) throw() : + d_vars(vars), d_guards(guards), d_heads(heads), d_body(body), d_triggers(triggers), d_deduction(deduction) { +} + +PropagateRuleCommand::PropagateRuleCommand(const VExpr & vars, + const VExpr & heads, + const Expr & body, + bool deduction + ) throw() : + d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) { +} + +const PropagateRuleCommand::VExpr & PropagateRuleCommand::getVars() const throw(){ + return d_vars; +}; +const PropagateRuleCommand::VExpr & PropagateRuleCommand::getGuards() const throw(){ + return d_guards; +}; +const PropagateRuleCommand::VExpr & PropagateRuleCommand::getHeads() const throw(){ + return d_heads; +}; +const Expr & PropagateRuleCommand::getBody() const throw(){ + return d_body; +}; +const PropagateRuleCommand::Triggers & PropagateRuleCommand::getTriggers() const throw(){ + return d_triggers; +}; +bool PropagateRuleCommand::isDeduction() const throw(){ + return d_deduction; +}; + + +void PropagateRuleCommand::invoke(SmtEngine* smtEngine) throw() { + try { + ExprManager* em = smtEngine->getExprManager(); + /** build vars list */ + Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); + /** build guards list */ + Expr guards; + if(d_guards.size() == 0) guards = em->mkConst<bool>(true); + else if(d_guards.size() == 1) guards = d_guards[0]; + else guards = em->mkExpr(kind::AND,d_guards); + /** build heads list */ + Expr heads; + if(d_heads.size() == 1) heads = d_heads[0]; + else heads = em->mkExpr(kind::AND,d_heads); + /** build expression */ + Expr expr; + if( d_triggers.empty() ){ + expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body); + } else { + /** build triggers list */ + std::vector<Expr> vtriggers; + vtriggers.reserve(d_triggers.size()); + for(Triggers::const_iterator i = d_triggers.begin(), + end = d_triggers.end(); i != end; ++i){ + vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i)); + } + Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers); + expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body,triggers); + } + smtEngine->assertFormula(expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + /** Convert variables */ + VExpr vars; vars.reserve(d_vars.size()); + for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); + i == end; ++i){ + vars.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert guards */ + VExpr guards; guards.reserve(d_guards.size()); + for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); + i == end; ++i){ + guards.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert heads */ + VExpr heads; heads.reserve(d_heads.size()); + for(VExpr::iterator i = d_heads.begin(), end = d_heads.end(); + i == end; ++i){ + heads.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert triggers */ + Triggers triggers; triggers.resize(d_triggers.size()); + for(size_t i = 0, end = d_triggers.size(); + i < end; ++i){ + triggers[i].reserve(d_triggers[i].size()); + for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); + j == jend; ++i){ + triggers[i].push_back(j->exportTo(exprManager, variableMap)); + }; + }; + /** Convert head and body */ + Expr body = d_body.exportTo(exprManager, variableMap); + /** Create the converted rules */ + return new PropagateRuleCommand(vars,guards,heads,body,triggers); +} + +Command* PropagateRuleCommand::clone() const { + return new PropagateRuleCommand(d_vars,d_guards,d_heads,d_body,d_triggers); +} + + /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) throw() { diff --git a/src/expr/command.h b/src/expr/command.h index 123fe0182..9f1722f9f 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -599,6 +599,69 @@ public: Command* clone() const; };/* class DatatypeDeclarationCommand */ +class CVC4_PUBLIC RewriteRuleCommand : public Command { +protected: + typedef std::vector< Expr > VExpr; + VExpr d_vars; + VExpr d_guards; + Expr d_head; + Expr d_body; + typedef std::vector< std::vector< Expr > > Triggers; + Triggers d_triggers; +public: + RewriteRuleCommand(const VExpr & vars, + const std::vector< Expr> & guards, + const Expr & head, const Expr & body, + Triggers d_triggers + ) throw(); + RewriteRuleCommand(const VExpr & vars, + const Expr & head, const Expr & body) throw(); + ~RewriteRuleCommand() throw() {} + const VExpr & getVars() const throw(); + const VExpr & getGuards() const throw(); + const Expr & getHead() const throw(); + const Expr & getBody() const throw(); + const Triggers & getTriggers() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; +};/* class RewriteRuleCommand */ + +class CVC4_PUBLIC PropagateRuleCommand : public Command { +protected: + typedef std::vector< Expr > VExpr; + VExpr d_vars; + VExpr d_guards; + VExpr d_heads; + Expr d_body; + typedef std::vector< std::vector< Expr > > Triggers; + Triggers d_triggers; + bool d_deduction; +public: + PropagateRuleCommand(const VExpr & vars, + const VExpr & guards, + const VExpr & heads, + const Expr & body, + Triggers d_triggers, + /* true if we want a deduction rule */ + bool d_deduction = false + ) throw(); + PropagateRuleCommand(const VExpr & vars, + const VExpr & heads, const Expr & body, + bool d_deduction = false) throw(); + ~PropagateRuleCommand() throw() {} + const VExpr & getVars() const throw(); + const VExpr & getGuards() const throw(); + const VExpr & getHeads() const throw(); + const Expr & getBody() const throw(); + const Triggers & getTriggers() const throw(); + bool isDeduction() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; +};/* class PropagateRuleCommand */ + + class CVC4_PUBLIC QuitCommand : public Command { public: QuitCommand() throw(); diff --git a/src/expr/node.h b/src/expr/node.h index 0b150d25d..b0fda3354 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -892,6 +892,25 @@ inline std::ostream& operator<<(std::ostream& out, TNode n) { return out; } +/** + * Serializes a vector of node to the given stream. + * + * @param out the output stream to use + * @param ns the vector of nodes to output to the stream + * @return the stream + */ +template<bool ref_count> +inline std::ostream& operator<<(std::ostream& out, + const std::vector< NodeTemplate<ref_count> > & ns) { + for(typename std::vector< NodeTemplate<ref_count> >::const_iterator + i=ns.begin(), end=ns.end(); + i != end; ++i){ + out << *i; + } + return out; +} + + }/* CVC4 namespace */ #include <ext/hash_map> |