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/command.h | |
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/command.h')
-rw-r--r-- | src/expr/command.h | 63 |
1 files changed, 63 insertions, 0 deletions
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(); |