Improve pre-skolemization, move quantifiers preprocess to own file (#7153)

This also heavily refactors the preskolemization method (now in QuantifiersPreprocess), in preparation for it being enabled by default. This method previously was doing a tree traversal, it now maintains a visited cache.

It makes minor cleanup to the dependencies of this method.

1 files changed, 29 insertions, 2 deletions

diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 5f91a9488..7ca17b6ad 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -78,8 +78,35 @@ public:
   std::map< Node, bool > d_phase_reqs_equality;
   std::map< Node, Node > d_phase_reqs_equality_term;
 
-  static void getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
-  static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
+  /**
+   * Get the polarity of the child^th child of n, assuming its polarity
+   * is given by (hasPol, pol). A term has polarity if it is only relevant
+   * if asserted with one polarity. Its polarity is (typically) the number
+   * of negations it is beneath.
+   */
+  static void getPolarity(Node n,
+                          size_t child,
+                          bool hasPol,
+                          bool pol,
+                          bool& newHasPol,
+                          bool& newPol);
+
+  /**
+   * Get the entailed polarity of the child^th child of n, assuming its
+   * entailed polarity is given by (hasPol, pol). A term has entailed polarity
+   * if it must be asserted with a polarity. Its polarity is (typically) the
+   * number of negations it is beneath.
+   *
+   * Entailed polarity and polarity above differ, e.g.:
+   *   (and A B): A and B have true polarity and true entailed polarity
+   *   (or A B): A and B have true polarity and no entailed polarity
+   */
+  static void getEntailPolarity(Node n,
+                                size_t child,
+                                bool hasPol,
+                                bool pol,
+                                bool& newHasPol,
+                                bool& newPol);
 };
 
 }