Interpolation: Add interface for SyGuS interpolation module (step3) (#4726)

This is the 3rd step of adding interface for SyGuS Interpolation module. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.

The 3rd step partially implemented the interpolation module.

2 files changed, 170 insertions, 21 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 42572a0c7..31f975786 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -39,25 +39,160 @@ SygusInterpol::SygusInterpol(LogicInfo logic) : d_logic(logic) {}
 void SygusInterpol::collectSymbols(const std::vector<Node>& axioms,
                                    const Node& conj)
 {
+  Trace("sygus-interpol-debug") << "Collect symbols..." << std::endl;
+  std::unordered_set<Node, NodeHashFunction> symSetAxioms;
+  std::unordered_set<Node, NodeHashFunction> symSetConj;
+  for (size_t i = 0, size = axioms.size(); i < size; i++)
+  {
+    expr::getSymbols(axioms[i], symSetAxioms);
+  }
+  expr::getSymbols(conj, symSetConj);
+  d_syms.insert(d_syms.end(), symSetAxioms.begin(), symSetAxioms.end());
+  d_syms.insert(d_syms.end(), symSetConj.begin(), symSetConj.end());
+  for (const Node& elem : symSetConj)
+  {
+    if (symSetAxioms.find(elem) != symSetAxioms.end())
+    {
+      d_symSetShared.insert(elem);
+    }
+  }
+  Trace("sygus-interpol-debug")
+      << "...finish, got " << d_syms.size() << " symbols in total. And "
+      << d_symSetShared.size() << " shared symbols." << std::endl;
 }
 
 void SygusInterpol::createVariables(bool needsShared)
 {
+  NodeManager* nm = NodeManager::currentNM();
+  for (const Node& s : d_syms)
+  {
+    TypeNode tn = s.getType();
+    if (tn.isConstructor() || tn.isSelector() || tn.isTester())
+    {
+      // datatype symbols should be considered interpreted symbols here, not
+      // (higher-order) variables.
+      continue;
+    }
+    // Notice that we allow for non-first class (e.g. function) variables here.
+    std::stringstream ss;
+    ss << s;
+    Node var = nm->mkBoundVar(tn);
+    d_vars.push_back(var);
+    Node vlv = nm->mkBoundVar(ss.str(), tn);
+    d_vlvs.push_back(vlv);
+    if (!needsShared || d_symSetShared.find(s) != d_symSetShared.end())
+    {
+      d_varsShared.push_back(var);
+      d_vlvsShared.push_back(vlv);
+      d_varTypesShared.push_back(tn);
+    }
+  }
+  // make the sygus variable list
+  d_ibvlShared = nm->mkNode(kind::BOUND_VAR_LIST, d_vlvsShared);
+  Trace("sygus-interpol-debug") << "...finish" << std::endl;
 }
 
-std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > getIncludeCons(
-    const std::vector<Node>& assumptions, const Node& conclusion)
+void SygusInterpol::getIncludeCons(
+    const std::vector<Node>& axioms,
+    const Node& conj,
+    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& result)
 {
-  std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > result =
-      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >();
-  return result;
+  NodeManager* nm = NodeManager::currentNM();
+  Assert(options::produceInterpols() != options::ProduceInterpols::NONE);
+  // ASSUMPTIONS
+  if (options::produceInterpols() == options::ProduceInterpols::ASSUMPTIONS)
+  {
+    Node tmpAssumptions =
+        (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms));
+    expr::getOperatorsMap(tmpAssumptions, result);
+  }
+  // CONJECTURE
+  else if (options::produceInterpols() == options::ProduceInterpols::CONJECTURE)
+  {
+    expr::getOperatorsMap(conj, result);
+  }
+  // SHARED
+  else if (options::produceInterpols() == options::ProduceInterpols::SHARED)
+  {
+    // Get operators from axioms
+    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>
+        include_cons_axioms;
+    Node tmpAssumptions =
+        (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms));
+    expr::getOperatorsMap(tmpAssumptions, include_cons_axioms);
+
+    // Get operators from conj
+    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>
+        include_cons_conj;
+    expr::getOperatorsMap(conj, include_cons_conj);
+
+    // Compute intersection
+    for (auto& [tn, axiomsOps] : include_cons_axioms)
+    {
+      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
+          concIter = include_cons_conj.find(tn);
+      if (concIter != include_cons_conj.end())
+      {
+        std::unordered_set<Node, NodeHashFunction> conjOps = concIter->second;
+        for (const Node& n : axiomsOps)
+        {
+          if (conjOps.find(n) != conjOps.end())
+          {
+            if (result.find(tn) == result.end())
+            {
+              result[tn] = std::unordered_set<Node, NodeHashFunction>();
+            }
+            result[tn].insert(n);
+          }
+        }
+      }
+    }
+  }
+  // ALL
+  else if (options::produceInterpols() == options::ProduceInterpols::ALL)
+  {
+    Node tmpAssumptions =
+        (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms));
+    Node tmpAll = nm->mkNode(kind::AND, tmpAssumptions, conj);
+    expr::getOperatorsMap(tmpAll, result);
+  }
 }
 
 TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType,
                                         const std::vector<Node>& axioms,
                                         const Node& conj)
 {
+  Trace("sygus-interpol-debug") << "Setup grammar..." << std::endl;
   TypeNode itpGTypeS;
+  if (!itpGType.isNull())
+  {
+    // set user-defined grammar
+    Assert(itpGType.isDatatype() && itpGType.getDType().isSygus());
+    itpGTypeS = datatypes::utils::substituteAndGeneralizeSygusType(
+        itpGType, d_syms, d_vlvs);
+    Assert(itpGTypeS.isDatatype() && itpGTypeS.getDType().isSygus());
+    // TODO(Ying Sheng) check if the vars in user-defined grammar, are
+    // consistent with the shared vars
+  }
+  else
+  {
+    // set default grammar
+    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
+    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exclude_cons;
+    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons;
+    getIncludeCons(axioms, conj, include_cons);
+    std::unordered_set<Node, NodeHashFunction> terms_irrelevant;
+    itpGTypeS =
+        CVC4::theory::quantifiers::CegGrammarConstructor::mkSygusDefaultType(
+            NodeManager::currentNM()->booleanType(),
+            d_ibvlShared,
+            "interpolation_grammar",
+            extra_cons,
+            exclude_cons,
+            include_cons,
+            terms_irrelevant);
+  }
+  Trace("sygus-interpol-debug") << "...finish setting up grammar" << std::endl;
   return itpGTypeS;
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 4655822ec..a79d583cd 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -71,7 +71,7 @@ class SygusInterpol
   /**
    * Collects symbols from axioms (axioms) and conjecture (conj), which are
    * stored in d_syms, and computes the shared symbols between axioms and
-   * conjecture, stored in d_symsShared.
+   * conjecture, stored in d_symSetShared.
    *
    * @param axioms the assertions (Fa above)
    * @param conj the conjecture (Fc above)
@@ -80,11 +80,11 @@ class SygusInterpol
 
   /**
    * Creates free variables and shared free variables from d_syms and
-   * d_symsShared, which are stored in d_vars and d_varsShared. And also creates
-   * the corresponding set of variables for the formal argument list, which is
-   * stored in d_vlvs and d_vlvsShared. Extracts the types of shared variables,
-   * which are stored in d_varTypesShared. Creates the formal argument list of
-   * the interpol-to-synthesis, stored in d_ibvlShared.
+   * d_symSetShared, which are stored in d_vars and d_varsShared. And also
+   * creates the corresponding set of variables for the formal argument list,
+   * which is stored in d_vlvs and d_vlvsShared. Extracts the types of shared
+   * variables, which are stored in d_varTypesShared. Creates the formal
+   * argument list of the interpol-to-synthese, stored in d_ibvlShared.
    *
    * When using default grammar, the needsShared is true. When using
    * user-defined gramar, the needsShared is false.
@@ -96,17 +96,32 @@ class SygusInterpol
   void createVariables(bool needsShared);
 
   /**
+   * Get include_cons for mkSygusDefaultType.
+   * mkSygusDefaultType() is a function to make default grammar. It has an
+   * arguemnt include_cons, which will restrict what operators we want in the
+   * grammar. The return value depends on options::produceInterpols(). In
+   * ASSUMPTIONS option, it will return the operators from axioms. In CONJECTURE
+   * option, it will return the operators from conj. In SHARED option, it will
+   * return the oprators shared by axioms and conj. In ALL option, it will
+   * return the operators from either axioms or conj.
+   *
+   * @param axioms input argument
+   * @param conj input argument
+   * @param result the return value
+   */
+  void getIncludeCons(
+      const std::vector<Node>& axioms,
+      const Node& conj,
+      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& result);
+
+  /**
    * Set up the grammar for the interpol-to-synthesis.
    *
    * The user-defined grammar will be encoded by itpGType. The options for
    * grammar is given by options::produceInterpols(). In DEFAULT option, it will
    * set up the grammar from itpGType. And if itpGType is null, it will set up
-   * the default grammar. In ASSUMPTIONS option, it will set up the grammar by
-   * only using the operators from axioms. In CONJECTURE option, it will set up
-   * the grammar by only using the operators from conj. In SHARED option, it
-   * will set up the grammar by only using the operators shared by axioms and
-   * conj. In ALL option, it will set up the grammar by only using the operators
-   * from either axioms or conj.
+   * the default grammar, which is built according to a policy handled by
+   * getIncludeCons().
    *
    * @param itpGType (if non-null) a sygus datatype type that encodes the
    * grammar that should be used for solutions of the interpolation conjecture.
@@ -165,15 +180,14 @@ class SygusInterpol
    * The logic for the local copy of SMT engine (d_subSolver).
    */
   LogicInfo d_logic;
-
   /**
    * symbols from axioms and conjecture.
    */
   std::vector<Node> d_syms;
   /**
-   * shared symbols between axioms and conjecture.
+   * unordered set for shared symbols between axioms and conjecture.
    */
-  std::vector<Node> d_symsShared;
+  std::unordered_set<Node, NodeHashFunction> d_symSetShared;
   /**
    * free variables created from d_syms.
    */
@@ -183,7 +197,7 @@ class SygusInterpol
    */
   std::vector<Node> d_vlvs;
   /**
-   * free variables created from d_symsShared.
+   * free variables created from d_symSetShared.
    */
   std::vector<Node> d_varsShared;
   /**