Flag to check invariance of entire values in sygus explain (#1908)

4 files changed, 80 insertions, 16 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 92fea9586..e8d29835a 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -236,6 +236,7 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
             std::vector<Node> msu;
             std::vector<Node> mexp;
             msu.insert(msu.end(), ms.begin(), ms.end());
+            std::map<TypeNode, int> var_count;
             for (unsigned k = 0; k < vs.size(); k++)
             {
               vsit.setUpdatedTerm(msu[k]);
@@ -249,8 +250,13 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
               Trace("sygus-cref-eval2-debug")
                   << "  compute min explain of : " << vs[k] << " = " << ut
                   << std::endl;
-              tds->getExplain()->getExplanationFor(vs[k], ut, mexp, vsit);
-              msu[k] = ut;
+              tds->getExplain()->getExplanationFor(
+                  vs[k], ut, mexp, vsit, var_count, false);
+              Trace("sygus-cref-eval2-debug")
+                  << "exp now: " << mexp << std::endl;
+              msu[k] = vsit.getUpdatedTerm();
+              Trace("sygus-cref-eval2-debug")
+                  << "updated term : " << msu[k] << std::endl;
             }
             if (!mexp.empty())
             {
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index f76edb1c3..2be6c9d91 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -205,6 +205,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb,
     }
     else
     {
+      // revert
       trb.replaceChild(i, vn[i]);
     }
   }
@@ -273,7 +274,7 @@ void SygusExplain::getExplanationFor(Node n,
   // naive :
   // return getExplanationForEquality( n, vn, exp );
 
-  // set up the recursion object
+  // set up the recursion object;
   std::map<TypeNode, int> var_count;
   TermRecBuild trb;
   trb.init(vn);
@@ -292,10 +293,32 @@ void SygusExplain::getExplanationFor(Node n,
 void SygusExplain::getExplanationFor(Node n,
                                      Node vn,
                                      std::vector<Node>& exp,
-                                     SygusInvarianceTest& et)
+                                     SygusInvarianceTest& et,
+                                     bool strict)
 {
-  int sz = -1;
   std::map<TypeNode, int> var_count;
+  getExplanationFor(n, vn, exp, et, var_count, strict);
+}
+
+void SygusExplain::getExplanationFor(Node n,
+                                     Node vn,
+                                     std::vector<Node>& exp,
+                                     SygusInvarianceTest& et,
+                                     std::map<TypeNode, int>& var_count,
+                                     bool strict)
+{
+  if (!strict)
+  {
+    // check if it is invariant over the entire node
+    TypeNode vtn = vn.getType();
+    Node x = d_tdb->getFreeVarInc(vtn, var_count);
+    if (et.is_invariant(d_tdb, x, x))
+    {
+      return;
+    }
+    var_count[vtn]--;
+  }
+  int sz = -1;
   TermRecBuild trb;
   trb.init(vn);
   Node vnr;
diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h
index 818f51438..056ea7ed5 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.h
+++ b/src/theory/quantifiers/sygus/sygus_explain.h
@@ -182,6 +182,15 @@ class SygusExplain
    * - (if applicable) exp => ( n != vnr ).
    *
    * This function updates sz to be the term size of [[exp]]_n.
+   *
+   * If strict is false, then we also test whether the invariance test holds
+   * independently of the entire value of vn.
+   *
+   * The argument var_count is used for tracking the variables that we introduce
+   * to generalize the shape of vn. This map is passed to
+   * TermDbSygus::getFreeVarInc. This argument should be used if we are
+   * calling this function multiple times and the generalization should not
+   * introduce variables that shadow the variables introduced on previous calls.
    */
   void getExplanationFor(Node n,
                          Node vn,
@@ -192,7 +201,14 @@ class SygusExplain
   void getExplanationFor(Node n,
                          Node vn,
                          std::vector<Node>& exp,
-                         SygusInvarianceTest& et);
+                         SygusInvarianceTest& et,
+                         bool strict = true);
+  void getExplanationFor(Node n,
+                         Node vn,
+                         std::vector<Node>& exp,
+                         SygusInvarianceTest& et,
+                         std::map<TypeNode, int>& var_count,
+                         bool strict = true);
 
  private:
   /** sygus term database associated with this utility */
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index c45d4971e..774ba2180 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -285,11 +285,15 @@ public:
       }
     }
     if( !d_req_type.isNull() ){
+      Trace("sygus-sb-debug") << "- check if " << tn << " is type "
+                              << d_req_type << std::endl;
       if( tn!=d_req_type ){
         return false;
       }
     }
     if( d_req_kind!=UNDEFINED_KIND ){
+      Trace("sygus-sb-debug") << "- check if " << tn << " has " << d_req_kind
+                              << std::endl;
       int c = tdb->getKindConsNum( tn, d_req_kind );
       if( c!=-1 ){
         bool ret = true;
@@ -327,22 +331,37 @@ bool TermDbSygus::considerArgKind( TypeNode tn, TypeNode tnp, Kind k, Kind pk, i
   const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
   Assert( hasKind( tn, k ) );
   Assert( hasKind( tnp, pk ) );
-  Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk << ", arg = " << arg << "?" << std::endl;
+  Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
+                          << ", arg = " << arg << " in " << tnp << "?"
+                          << std::endl;
   int c = getKindConsNum( tn, k );
   int pc = getKindConsNum( tnp, pk );
-  if( k==pk ){
     //check for associativity
-    if( quantifiers::TermUtil::isAssoc( k ) ){
-      //if the operator is associative, then a repeated occurrence should only occur in the leftmost argument position
-      int firstArg = getFirstArgOccurrence( pdt[pc], tn );
-      Assert( firstArg!=-1 );
-      if( arg!=firstArg ){
-        Trace("sygus-sb-simple") << "  sb-simple : do not consider " << k << " at child arg " << arg << " of " << k << " since it is associative, with first arg = " << firstArg << std::endl;
-        return false;
-      }else{
+  if (k == pk && quantifiers::TermUtil::isAssoc(k))
+  {
+    // if the operator is associative, then a repeated occurrence should only
+    // occur in the leftmost argument position
+    int firstArg = getFirstArgOccurrence(pdt[pc], tn);
+    Assert(firstArg != -1);
+    if (arg == firstArg)
+    {
+      return true;
+    }
+    // the argument types of the child must be the parent's type
+    for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
+    {
+      TypeNode tn = TypeNode::fromType(dt[c].getArgType(i));
+      if (tn != tnp)
+      {
         return true;
       }
     }
+    Trace("sygus-sb-simple")
+        << "  sb-simple : do not consider " << k << " at child arg " << arg
+        << " of " << k
+        << " since it is associative, with first arg = " << firstArg
+        << std::endl;
+    return false;
   }
   //describes the shape of an alternate term to construct
   //  we check whether this term is in the sygus grammar below