1 files changed, 89 insertions, 0 deletions
diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h
new file mode 100644
index 000000000..092a62942
--- /dev/null
+++ b/src/preprocessing/passes/quantifier_macros.h
@@ -0,0 +1,89 @@
+/*********************                                                        */
+/*! \file quantifier_macros.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief Pre-process step for detecting quantifier macro definitions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
+#define __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
+
+#include <map>
+#include <string>
+#include <vector>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class QuantifierMacros : public PreprocessingPass
+{
+ public:
+  QuantifierMacros(PreprocessingPassContext* preprocContext);
+  ~QuantifierMacros() {}
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  bool processAssertion(Node n);
+  bool isBoundVarApplyUf(Node n);
+  bool process(Node n, bool pol, std::vector<Node>& args, Node f);
+  bool containsBadOp(Node n,
+                     Node op,
+                     std::vector<Node>& opc,
+                     std::map<Node, bool>& visited);
+  bool isMacroLiteral(Node n, bool pol);
+  bool isGroundUfTerm(Node f, Node n);
+  void getMacroCandidates(Node n,
+                          std::vector<Node>& candidates,
+                          std::map<Node, bool>& visited);
+  Node solveInEquality(Node n, Node lit);
+  bool getFreeVariables(Node n,
+                        std::vector<Node>& v_quant,
+                        std::vector<Node>& vars,
+                        bool retOnly,
+                        std::map<Node, bool>& visited);
+  bool getSubstitution(std::vector<Node>& v_quant,
+                       std::map<Node, Node>& solved,
+                       std::vector<Node>& vars,
+                       std::vector<Node>& subs,
+                       bool reqComplete);
+  void addMacro(Node op, Node n, std::vector<Node>& opc);
+  void debugMacroDefinition(Node oo, Node n);
+  bool simplify(std::vector<Node>& assertions, bool doRewrite = false);
+  Node simplify(Node n);
+  void finalizeDefinitions();
+  void clearMaps();
+
+  // map from operators to macro basis terms
+  std::map<Node, std::vector<Node> > d_macro_basis;
+  // map from operators to macro definition
+  std::map<Node, Node> d_macro_defs;
+  std::map<Node, Node> d_macro_defs_new;
+  // operators to macro ops that contain them
+  std::map<Node, std::vector<Node> > d_macro_def_contains;
+  // simplify caches
+  std::map<Node, Node> d_simplify_cache;
+  std::map<Node, bool> d_quant_macros;
+  bool d_ground_macros;
+};
+
+}  // passes
+}  // preprocessing
+}  // CVC4
+
+#endif /*__CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */