Add nested quantifier elimination module (#5422)

This has static utilities for doing nested quantifier elimination and some data structures for maintaining a context-dependent set of quantified formulas that have been processed.

This is work towards CVC4/cvc4-wishues#26, and work reimplementation of the option --ceqgi-nested-qe.

4 files changed, 238 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c570dfdb4..aaa1f04f8 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -616,6 +616,8 @@ libcvc4_add_sources(
   theory/quantifiers/cegqi/ceg_instantiator.h
   theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
   theory/quantifiers/cegqi/inst_strategy_cegqi.h
+  theory/quantifiers/cegqi/nested_qe.cpp
+  theory/quantifiers/cegqi/nested_qe.h
   theory/quantifiers/cegqi/vts_term_cache.cpp
   theory/quantifiers/cegqi/vts_term_cache.h
   theory/quantifiers/conjecture_generator.cpp
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index fb3df5327..430303f6b 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -112,6 +112,8 @@ libcvc4_add_sources(
   record.h
   sequence.cpp
   sequence.h
+  subs.cpp
+  subs.h
   sygus_datatype.cpp
   sygus_datatype.h
   uninterpreted_constant.cpp
diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp
new file mode 100644
index 000000000..7f77a1daf
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/nested_qe.cpp
@@ -0,0 +1,148 @@
+/*********************                                                        */
+/*! \file nested_qe.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Methods for counterexample-guided quantifier instantiation
+ ** based on nested quantifier elimination.
+ **/
+
+#include "theory/quantifiers/cegqi/nested_qe.h"
+
+#include "expr/node_algorithm.h"
+#include "expr/subs.h"
+#include "theory/smt_engine_subsolver.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+NestedQe::NestedQe(context::UserContext* u) : d_qnqe(u) {}
+
+bool NestedQe::process(Node q, std::vector<Node>& lems)
+{
+  NodeNodeMap::iterator it = d_qnqe.find(q);
+  if (it != d_qnqe.end())
+  {
+    // already processed
+    return (*it).second != q;
+  }
+  Trace("cegqi-nested-qe") << "Check nested QE on " << q << std::endl;
+  Node qqe = doNestedQe(q, true);
+  d_qnqe[q] = qqe;
+  if (qqe == q)
+  {
+    Trace("cegqi-nested-qe") << "...did not apply nested QE" << std::endl;
+    return false;
+  }
+  Trace("cegqi-nested-qe") << "...applied nested QE" << std::endl;
+  Trace("cegqi-nested-qe") << "Result is " << qqe << std::endl;
+
+  // add as lemma
+  lems.push_back(q.eqNode(qqe));
+  return true;
+}
+
+bool NestedQe::hasProcessed(Node q) const
+{
+  return d_qnqe.find(q) != d_qnqe.end();
+}
+
+bool NestedQe::getNestedQuantification(
+    Node q, std::unordered_set<Node, NodeHashFunction>& nqs)
+{
+  expr::getKindSubterms(q[1], kind::FORALL, true, nqs);
+  return !nqs.empty();
+}
+
+bool NestedQe::hasNestedQuantification(Node q)
+{
+  std::unordered_set<Node, NodeHashFunction> nqs;
+  return getNestedQuantification(q, nqs);
+}
+
+Node NestedQe::doNestedQe(Node q, bool keepTopLevel)
+{
+  Assert(q.getKind() == kind::FORALL);
+  std::unordered_set<Node, NodeHashFunction> nqs;
+  if (!getNestedQuantification(q, nqs))
+  {
+    Trace("cegqi-nested-qe-debug")
+        << "...no nested quantification" << std::endl;
+    if (keepTopLevel)
+    {
+      return q;
+    }
+    // just do ordinary quantifier elimination
+    Node qqe = doQe(q);
+    Trace("cegqi-nested-qe-debug") << "...did ordinary qe" << std::endl;
+    return qqe;
+  }
+  Trace("cegqi-nested-qe-debug")
+      << "..." << nqs.size() << " nested quantifiers" << std::endl;
+  // otherwise, skolemize the arguments of this and apply
+  std::vector<Node> vars(q[0].begin(), q[0].end());
+  Subs sk;
+  sk.add(vars);
+  // do nested quantifier elimination on each nested quantifier, skolemizing the
+  // free variables
+  Subs snqe;
+  for (const Node& nq : nqs)
+  {
+    Node nqk = sk.apply(nq);
+    Node nqqe = doNestedQe(nqk);
+    if (nqqe == nqk)
+    {
+      // failed
+      Trace("cegqi-nested-qe-debug")
+          << "...failed to apply to nested" << std::endl;
+      return q;
+    }
+    snqe.add(nqk, nqqe);
+  }
+  // get the result of nested quantifier elimination
+  Node qeBody = sk.apply(q[1]);
+  qeBody = snqe.apply(qeBody);
+  // undo the skolemization
+  qeBody = sk.rapply(qeBody, true);
+  // reconstruct the body
+  std::vector<Node> qargs;
+  qargs.push_back(q[0]);
+  qargs.push_back(qeBody);
+  if (q.getNumChildren() == 3)
+  {
+    qargs.push_back(q[2]);
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  return nm->mkNode(kind::FORALL, qargs);
+}
+
+Node NestedQe::doQe(Node q)
+{
+  Assert(q.getKind() == kind::FORALL);
+  Trace("cegqi-nested-qe") << "  Apply qe to " << q << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  q = nm->mkNode(kind::EXISTS, q[0], q[1].negate());
+  std::unique_ptr<SmtEngine> smt_qe;
+  initializeSubsolver(smt_qe);
+  Node qqe = smt_qe->getQuantifierElimination(q, true, false);
+  if (expr::hasBoundVar(qqe))
+  {
+    Trace("cegqi-nested-qe") << "  ...failed QE" << std::endl;
+    //...failed to apply
+    return q;
+  }
+  Node res = qqe.negate();
+  Trace("cegqi-nested-qe") << "  ...success, result = " << res << std::endl;
+  return res;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h
new file mode 100644
index 000000000..ef690afd5
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/nested_qe.h
@@ -0,0 +1,86 @@
+/*********************                                                        */
+/*! \file nested_qe.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Methods for counterexample-guided quantifier instantiation
+ ** based on nested quantifier elimination.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
+#define CVC4__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
+
+#include <unordered_set>
+
+#include "context/cdhashmap.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class NestedQe
+{
+  using NodeNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+
+ public:
+  NestedQe(context::UserContext* u);
+  ~NestedQe() {}
+  /**
+   * Process quantified formula. If this returns true, then q was processed
+   * via nested quantifier elimination (either during this call or previously
+   * in this user context). If q was processed in this call, the lemma:
+   *   (= q qqe)
+   * is added to lem, where qqe is the result of nested quantifier elimination
+   * on q.
+   */
+  bool process(Node q, std::vector<Node>& lems);
+  /**
+   * Have we processed q using the above method?
+   */
+  bool hasProcessed(Node q) const;
+
+  /**
+   * Get nested quantification. Returns true if q has nested quantifiers.
+   * Adds each nested quantifier in the body of q to nqs.
+   */
+  static bool getNestedQuantification(
+      Node q, std::unordered_set<Node, NodeHashFunction>& nqs);
+  /**
+   * Does quantified formula q have nested quantification?
+   */
+  static bool hasNestedQuantification(Node q);
+  /**
+   * Do nested quantifier elimination. Returns a formula that is equivalent to
+   * q and has no nested quantification. If keepTopLevel is false, then the
+   * returned formula is quantifier-free. Otherwise, it is a quantified formula
+   * with no nested quantification.
+   */
+  static Node doNestedQe(Node q, bool keepTopLevel = false);
+  /**
+   * Run quantifier elimination on quantified formula q, where q has no nested
+   * quantification. This method invokes a subsolver for performing quantifier
+   * elimination.
+   */
+  static Node doQe(Node q);
+
+ private:
+  /**
+   * Mapping from quantified formulas q to the result of doNestedQe(q, true).
+   */
+  NodeNodeMap d_qnqe;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif