1 files changed, 78 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_preprocess.h b/src/theory/quantifiers/quantifiers_preprocess.h
new file mode 100644
index 000000000..45b7ad07a
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_preprocess.h
@@ -0,0 +1,78 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Preprocessor for the theory of quantifiers.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_PREPROCESS_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_PREPROCESS_H
+
+#include "proof/trust_node.h"
+#include "smt/env_obj.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * Module for doing preprocessing that is pertinent to quantifiers. These
+ * operations cannot be done in the rewriter since e.g. preskolemization
+ * depends on knowing the polarity of the position in which quantifiers occur.
+ */
+class QuantifiersPreprocess : protected EnvObj
+{
+ public:
+  QuantifiersPreprocess(Env& env);
+  /** preprocess
+   *
+   * This returns the result of applying simple quantifiers-specific
+   * pre-processing to n, including but not limited to:
+   * - pre-skolemization,
+   * - aggressive prenexing.
+   * The argument isInst is set to true if n is an instance of a previously
+   * registered quantified formula. If this flag is true, we do not apply
+   * certain steps like pre-skolemization since we know they will have no
+   * effect.
+   *
+   * The result is wrapped in a trust node of kind TrustNodeKind::REWRITE.
+   */
+  TrustNode preprocess(Node n, bool isInst = false) const;
+
+ private:
+  using NodePolPairHashFunction = PairHashFunction<Node, bool, std::hash<Node>>;
+  /**
+   * Pre-skolemize quantifiers. Return the pre-skolemized form of n.
+   *
+   * @param n The formula to preskolemize.
+   * @param polarity The polarity of n in the input.
+   * @param fvs The free variables
+   * @param visited Cache of visited (node, polarity) pairs.
+   */
+  Node preSkolemizeQuantifiers(
+      Node n,
+      bool polarity,
+      std::vector<TNode>& fvs,
+      std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>&
+          visited) const;
+  /**
+   * Apply prenexing aggressively. Returns the prenex normal form of n.
+   */
+  Node computePrenexAgg(Node n, std::map<Node, Node>& visited) const;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */