From 1b0aa1c39ff7abe15bbd9305d376d10b007d69d0 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 12 Feb 2018 18:16:59 -0600
Subject: Option to use extended rewriter as a preprocessing pass (#1600)

---
 src/theory/quantifiers/extended_rewrite.h | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'src/theory/quantifiers/extended_rewrite.h')

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 */
-- 
cgit v1.2.3