Replace conditional rewrite pass in quantifiers with the extended rewriter (#3841)

Fixes #3839.

Previously, the quantifiers rewriter had a rewriting step that was an ad-hoc version of some of the rewrites that have been incorporated into the extended rewriter. Moreover, the code for that pass was buggy.

This eliminates the previous conditional rewriting step from the "term process" rewrite pass in quantifiers. It additional adds an optional (disabled by default) rewriting pass that calls the extended rewriter on the body of quantified formulas. This subsumes the previous behavior and should not be buggy.

Notice that the indentation in computeProcessTerms changed and subsequently has been updated to the new coding standards.

This PR relies on #3840.

1 files changed, 35 insertions, 8 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index ac87f944c..2a3180e78 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -39,8 +39,10 @@ enum RewriteStep
   COMPUTE_MINISCOPING,
   /** Aggressive miniscoping */
   COMPUTE_AGGRESSIVE_MINISCOPING,
+  /** Apply the extended rewriter to quantified formula bodies */
+  COMPUTE_EXT_REWRITE,
   /**
-   * Term processing (e.g. simplifying terms based on ITE conditions,
+   * Term processing (e.g. simplifying terms based on ITE lifting,
    * eliminating extended arithmetic symbols).
    */
   COMPUTE_PROCESS_TERMS,
@@ -150,12 +152,7 @@ class QuantifiersRewriter : public TheoryRewriter
                              Node n,
                              Node ipl);
   static Node computeProcessTerms2(Node body,
-                                   bool hasPol,
-                                   bool pol,
-                                   std::map<Node, bool>& currCond,
-                                   int nCurrCond,
                                    std::map<Node, Node>& cache,
-                                   std::map<Node, Node>& icache,
                                    std::vector<Node>& new_vars,
                                    std::vector<Node>& new_conds,
                                    bool elimExtArith);
@@ -201,12 +198,42 @@ class QuantifiersRewriter : public TheoryRewriter
                                const std::vector<Node>& args,
                                QAttributes& qa);
   //-------------------------------------end conditional splitting
+  //------------------------------------- process terms
+  /** compute process terms
+   *
+   * This takes as input a quantified formula q with attributes qa whose
+   * body is body.
+   *
+   * This rewrite eliminates problematic terms from the bodies of
+   * quantified formulas, which includes performing:
+   * - Certain cases of ITE lifting,
+   * - Elimination of extended arithmetic functions like to_int/is_int/div/mod,
+   * - Elimination of select over store.
+   *
+   * It may introduce new variables V into new_vars and new conditions C into
+   * new_conds. It returns a node retBody such that q of the form
+   *   forall X. body
+   * is equivalent to:
+   *   forall X, V. ( C => retBody )
+   */
+  static Node computeProcessTerms(Node body,
+                                  std::vector<Node>& new_vars,
+                                  std::vector<Node>& new_conds,
+                                  Node q,
+                                  QAttributes& qa);
+  //------------------------------------- end process terms
+  //------------------------------------- extended rewrite
+  /** compute extended rewrite
+   *
+   * This returns the result of applying the extended rewriter on the body
+   * of quantified formula q.
+   */
+  static Node computeExtendedRewrite(Node q);
+  //------------------------------------- end extended rewrite
  public:
   static Node computeElimSymbols( Node body );
   static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
-  //cache is dependent upon currCond, icache is not, new_conds are negated conditions
-  static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa );
   static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg );
   static Node computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited );
   static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );