(Move-only) Split quant util (#1306)

* Initial draft of splitting quant util.

* Minor

* Document recursive term builder.

* Rename file, minor.

* Clang format

1 files changed, 104 insertions, 0 deletions

diff --git a/src/theory/quantifiers/quant_epr.h b/src/theory/quantifiers/quant_epr.h
new file mode 100644
index 000000000..f191da68e
--- /dev/null
+++ b/src/theory/quantifiers/quant_epr.h
@@ -0,0 +1,104 @@
+/*********************                                                        */
+/*! \file quant_epr.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 quantifier util
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANT_EPR_H
+#define __CVC4__THEORY__QUANT_EPR_H
+
+#include <map>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Quant EPR
+ *
+ * This class maintains information required for
+ * approaches for effectively propositional logic (EPR),
+ * also called the Bernays-Schoenfinkel fragment.
+ *
+ * It maintains for each type whether the type
+ * has a finite Herbrand universe, stored in d_consts.
+ * This class is used in counterexample-guided instantiation
+ * for EPR, described in Reynolds et al.,
+ * "Reasoning in the Bernays-Schonfinkel-Ramsey Fragment of
+ * Separation Logic", VMCAI 2017.
+ *
+ * Below, we say a type is an "EPR type" if its
+ * Herbrand universe can be restricted to a finite set
+ * based on the set of input assertions,
+ * and a "non-EPR type" otherwise.
+ */
+class QuantEPR
+{
+ public:
+  QuantEPR() {}
+  virtual ~QuantEPR() {}
+  /** constants per type */
+  std::map<TypeNode, std::vector<Node> > d_consts;
+  /** register an input assertion with this class
+   * This updates whether types are EPR are not
+   * based on the constraints in assertion.
+   */
+  void registerAssertion(Node assertion);
+  /** finish initialize
+   * This ensures all EPR sorts are non-empty
+   * (that is, they have at least one term in d_consts),
+   * and clears non-EPR sorts from d_consts.
+   */
+  void finishInit();
+  /** is type tn an EPR type? */
+  bool isEPR(TypeNode tn) const
+  {
+    return d_non_epr.find(tn) == d_non_epr.end();
+  }
+  /** is k an EPR constant for type tn? */
+  bool isEPRConstant(TypeNode tn, Node k);
+  /** add EPR constant k of type tn. */
+  void addEPRConstant(TypeNode tn, Node k);
+  /** get EPR axiom for type
+   * This is a formula of the form:
+   *   forall x : U. ( x = c1 V ... x = cn )
+   * where c1...cn are the constants in the Herbrand
+   * universe of U.
+   */
+  Node mkEPRAxiom(TypeNode tn);
+  /** does this class have an EPR axiom for type tn? */
+  bool hasEPRAxiom(TypeNode tn) const
+  {
+    return d_epr_axiom.find(tn) != d_epr_axiom.end();
+  }
+
+ private:
+  /** register the node */
+  void registerNode(Node n,
+                    std::map<int, std::map<Node, bool> >& visited,
+                    bool beneathQuant,
+                    bool hasPol,
+                    bool pol);
+  /** map from types to a flag says whether they are not EPR */
+  std::map<TypeNode, bool> d_non_epr;
+  /** EPR axioms for each type. */
+  std::map<TypeNode, Node> d_epr_axiom;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANT_EPR_H */