diff options
Diffstat (limited to 'src/theory/quantifiers/extended_rewrite.h')
-rw-r--r-- | src/theory/quantifiers/extended_rewrite.h | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 3a9fdb918..25d710a6b 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -43,12 +43,23 @@ namespace quantifiers { class ExtendedRewriter { public: - ExtendedRewriter(); + ExtendedRewriter(bool aggr = true); ~ExtendedRewriter() {} /** return the extended rewritten form of n */ Node extendedRewrite(Node n); private: + /** + * Whether this extended rewriter applies aggressive rewriting techniques, + * which are more expensive. Examples of aggressive rewriting include: + * - conditional rewriting, + * - condition merging, + * - sorting childing of commutative operators with more than 5 children. + * + * Aggressive rewriting is applied for SyGuS, whereas non-aggressive rewriting + * may be applied as a preprocessing step. + */ + bool d_aggr; /** true and false nodes */ Node d_true; Node d_false; @@ -62,6 +73,8 @@ class ExtendedRewriter * where ---->^E denotes extended rewriting. */ Node extendedRewritePullIte(Node n); + /** extended rewrite aggressive */ + Node extendedRewriteAggr(Node n); }; } /* CVC4::theory::quantifiers namespace */ |