Split utilites from CEGIS core connective module (#7441)

Towards a new module for enumerating unsat queries via SyGuS.

4 files changed, 67 insertions, 111 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 936310e4e..5a0cf8724 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -33,41 +33,6 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-bool VariadicTrie::add(Node n, const std::vector<Node>& i)
-{
-  VariadicTrie* curr = this;
-  for (const Node& ic : i)
-  {
-    curr = &(curr->d_children[ic]);
-  }
-  if (curr->d_data.isNull())
-  {
-    curr->d_data = n;
-    return true;
-  }
-  return false;
-}
-
-bool VariadicTrie::hasSubset(const std::vector<Node>& is) const
-{
-  if (!d_data.isNull())
-  {
-    return true;
-  }
-  for (const std::pair<const Node, VariadicTrie>& p : d_children)
-  {
-    Node n = p.first;
-    if (std::find(is.begin(), is.end(), n) != is.end())
-    {
-      if (p.second.hasSubset(is))
-      {
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
 CegisCoreConnective::CegisCoreConnective(Env& env,
                                          QuantifiersState& qs,
                                          QuantifiersInferenceManager& qim,
@@ -595,38 +560,6 @@ bool CegisCoreConnective::Component::addToAsserts(CegisCoreConnective* p,
   return true;
 }
 
-void CegisCoreConnective::getModel(SolverEngine& smt,
-                                   std::vector<Node>& vals) const
-{
-  for (const Node& v : d_vars)
-  {
-    Node mv = smt.getValue(v);
-    Trace("sygus-ccore-model") << v << " -> " << mv << " ";
-    vals.push_back(mv);
-  }
-}
-
-bool CegisCoreConnective::getUnsatCore(
-    SolverEngine& smt,
-    const std::unordered_set<Node>& queryAsserts,
-    std::vector<Node>& uasserts) const
-{
-  UnsatCore uc = smt.getUnsatCore();
-  bool hasQuery = false;
-  for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i)
-  {
-    Node uassert = *i;
-    Trace("sygus-ccore-debug") << "  uc " << uassert << std::endl;
-    if (queryAsserts.find(uassert) != queryAsserts.end())
-    {
-      hasQuery = true;
-      continue;
-    }
-    uasserts.push_back(uassert);
-  }
-  return hasQuery;
-}
-
 Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const
 {
   Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl;
@@ -758,7 +691,8 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
       std::unordered_set<Node> queryAsserts;
       queryAsserts.insert(ccheck.getFormula());
       queryAsserts.insert(d_sc);
-      bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts);
+      bool hasQuery =
+          getUnsatCoreFromSubsolver(*checkSol, queryAsserts, uasserts);
       // now, check the side condition
       bool falseCore = false;
       if (!d_sc.isNull())
@@ -794,7 +728,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
             uasserts.clear();
             std::unordered_set<Node> queryAsserts2;
             queryAsserts2.insert(d_sc);
-            getUnsatCore(*checkSc, queryAsserts2, uasserts);
+            getUnsatCoreFromSubsolver(*checkSc, queryAsserts2, uasserts);
             falseCore = true;
           }
         }
@@ -838,7 +772,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
       // it does not entail the postcondition, add an assertion that blocks
       // the current point
       mvs.clear();
-      getModel(*checkSol, mvs);
+      getModelFromSubsolver(*checkSol, d_vars, mvs);
       // should evaluate to true
       Node ean = evaluatePt(an, Node::null(), mvs);
       Assert(ean.isConst() && ean.getConst<bool>());
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
index 3ee631dea..26784f939 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.h
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -22,6 +22,7 @@
 
 #include "expr/node.h"
 #include "expr/node_trie.h"
+#include "expr/variadic_trie.h"
 #include "smt/env_obj.h"
 #include "theory/quantifiers/sygus/cegis.h"
 #include "util/result.h"
@@ -33,30 +34,6 @@ class SolverEngine;
 namespace theory {
 namespace quantifiers {
 
-/**
- * A trie that stores data at undetermined depth. Storing data at
- * undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which
- * assumes all data is stored at a fixed depth.
- *
- * Since data can be stored at any depth, we require both a d_children field
- * and a d_data field.
- */
-class VariadicTrie
-{
- public:
-  /** the children of this node */
-  std::map<Node, VariadicTrie> d_children;
-  /** the data at this node */
-  Node d_data;
-  /**
-   * Add data with identifier n indexed by i, return true if data is not already
-   * stored at the node indexed by i.
-   */
-  bool add(Node n, const std::vector<Node>& i);
-  /** Is there any data in this trie that is indexed by any subset of is? */
-  bool hasSubset(const std::vector<Node>& is) const;
-};
-
 /** CegisCoreConnective
  *
  * A sygus module that is specialized in handling conjectures of the form:
@@ -336,23 +313,6 @@ class CegisCoreConnective : public Cegis
   Node d_sc;
   //-----------------------------------for SMT engine calls
   /**
-   * Assuming smt has just been called to check-sat and returned "SAT", this
-   * method adds the model for d_vars to mvs.
-   */
-  void getModel(SolverEngine& smt, std::vector<Node>& mvs) const;
-  /**
-   * Assuming smt has just been called to check-sat and returned "UNSAT", this
-   * method get the unsat core and adds it to uasserts.
-   *
-   * The assertions in the argument queryAsserts (which we are not interested
-   * in tracking in the unsat core) are excluded from uasserts.
-   * If one of the formulas in queryAsserts was in the unsat core, then this
-   * method returns true. Otherwise, this method returns false.
-   */
-  bool getUnsatCore(SolverEngine& smt,
-                    const std::unordered_set<Node>& queryAsserts,
-                    std::vector<Node>& uasserts) const;
-  /**
    * Return the result of checking satisfiability of formula n.
    * If n was satisfiable, then we store the model for d_vars in mvs.
    */
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index 99e3f7768..d22bde370 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/smt_engine_subsolver.h"
 
+#include "proof/unsat_core.h"
 #include "smt/env.h"
 #include "smt/solver_engine.h"
 #include "smt/solver_engine_scope.h"
@@ -137,5 +138,41 @@ Result checkWithSubsolver(Node query,
   return r;
 }
 
+void getModelFromSubsolver(SolverEngine& smt,
+                           const std::vector<Node>& vars,
+                           std::vector<Node>& vals)
+{
+  for (const Node& v : vars)
+  {
+    Node mv = smt.getValue(v);
+    vals.push_back(mv);
+  }
+}
+
+bool getUnsatCoreFromSubsolver(SolverEngine& smt,
+                               const std::unordered_set<Node>& queryAsserts,
+                               std::vector<Node>& uasserts)
+{
+  UnsatCore uc = smt.getUnsatCore();
+  bool hasQuery = false;
+  for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i)
+  {
+    Node uassert = *i;
+    if (queryAsserts.find(uassert) != queryAsserts.end())
+    {
+      hasQuery = true;
+      continue;
+    }
+    uasserts.push_back(uassert);
+  }
+  return hasQuery;
+}
+
+void getUnsatCoreFromSubsolver(SolverEngine& smt, std::vector<Node>& uasserts)
+{
+  std::unordered_set<Node> queryAsserts;
+  getUnsatCoreFromSubsolver(smt, queryAsserts, uasserts);
+}
+
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index 0e1af29db..5de65a5d2 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -113,6 +113,31 @@ Result checkWithSubsolver(Node query,
                           bool needsTimeout = false,
                           unsigned long timeout = 0);
 
+//--------------- utilities
+
+/**
+ * Assuming smt has just been called to check-sat and returned "SAT", this
+ * method adds the model for d_vars to mvs.
+ */
+void getModelFromSubsolver(SolverEngine& smt,
+                           const std::vector<Node>& vars,
+                           std::vector<Node>& mvs);
+
+/**
+ * Assuming smt has just been called to check-sat and returned "UNSAT", this
+ * method get the unsat core and adds it to uasserts.
+ *
+ * The assertions in the argument queryAsserts (which we are not interested
+ * in tracking in the unsat core) are excluded from uasserts.
+ * If one of the formulas in queryAsserts was in the unsat core, then this
+ * method returns true. Otherwise, this method returns false.
+ */
+bool getUnsatCoreFromSubsolver(SolverEngine& smt,
+                               const std::unordered_set<Node>& queryAsserts,
+                               std::vector<Node>& uasserts);
+/** Same as above, without query asserts */
+void getUnsatCoreFromSubsolver(SolverEngine& smt, std::vector<Node>& uasserts);
+
 }  // namespace theory
 }  // namespace cvc5