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

8 files changed, 261 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
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 52eb63789..5cb24d072 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1475,6 +1475,7 @@ REG1_TESTS = \
 	regress1/sygus/commutative.sy \
 	regress1/sygus/constant.sy \
 	regress1/sygus/constant-ite-bv.sy \
+	regress1/sygus/crci-ssb-unk.sy \
 	regress1/sygus/dt-test-ns.sy \
 	regress1/sygus/dup-op.sy \
 	regress1/sygus/fg_polynomial3.sy \
@@ -1598,7 +1599,9 @@ REG2_TESTS = \
 	regress2/sygus/process-10-vars-2fun.sy \
 	regress2/sygus/process-arg-invariance.sy \
 	regress2/sygus/real-grammar-neg.sy \
+	regress2/sygus/sixfuncs.sy \
 	regress2/sygus/three.sy \
+	regress2/sygus/vcb.sy \
 	regress2/typed_v1l50016-simp.cvc \
 	regress2/uflia-error0.smt2 \
 	regress2/xs-09-16-3-4-1-5.decn.smt \
diff --git a/test/regress/regress1/sygus/crci-ssb-unk.sy b/test/regress/regress1/sygus/crci-ssb-unk.sy
new file mode 100644
index 000000000..f2b28db9c
--- /dev/null
+++ b/test/regress/regress1/sygus/crci-ssb-unk.sy
@@ -0,0 +1,43 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic BV)
+
+
+(define-fun origCir ( (LN4 Bool) (LN91 Bool)  )  Bool    
+          (and  LN91 LN4 )
+)
+
+
+(synth-fun skel ( (LN4 Bool) (LN91 Bool)  )  Bool    
+          ((Start Bool (
+                                  (and depth1 depth1)
+                                  (xor depth1 depth1)
+          ))
+          (depth1 Bool (
+                                  (not depth2)
+                                  LN91
+          ))
+          (depth2 Bool (
+                                  (and depth3 depth3)
+                                  (not depth3)
+                                  (or depth3 depth3)
+          ))
+          (depth3 Bool (
+                                  (and depth4 depth4)
+                                  (not depth4)
+                                  (or depth4 depth4)
+                                  (xor depth4 depth4)
+          ))
+          (depth4 Bool (
+                                  LN4
+          )))
+)
+
+
+(declare-var LN4 Bool)
+(declare-var LN91 Bool)
+
+(constraint (= (origCir LN4 LN91 ) (skel LN4 LN91 )))
+
+(check-synth)
diff --git a/test/regress/regress2/sygus/sixfuncs.sy b/test/regress/regress2/sygus/sixfuncs.sy
new file mode 100644
index 000000000..5280ffb20
--- /dev/null
+++ b/test/regress/regress2/sygus/sixfuncs.sy
@@ -0,0 +1,81 @@
+(set-logic LIA)
+
+(synth-fun f1 ((p1 Int) (P1 Int)) Int
+	   ((Start Int (
+			p1
+			P1
+			(- Start Start)
+			(+ Start Start)
+                     )
+           )))
+
+(synth-fun f2 ((p1 Int) (P1 Int)) Int
+	   ((Start Int (
+			p1
+			P1
+			(+ Start Start)
+                     )
+           )))
+
+(synth-fun f3 ((p1 Int) (P1 Int)) Int
+	   ((Start Int (
+			p1
+			P1
+			(- Start Start)
+			(+ Start Start)
+                     )
+           )))
+
+(synth-fun f4 ((p1 Int) (P1 Int)) Int
+	   ((Start Int (
+			p1
+			P1
+			(- Start Start)
+			(+ Start Start)
+                     )
+           )))
+
+(synth-fun f5 ((p1 Int) (P1 Int)) Int
+	   ((Start Int (
+			p1
+			P1
+			(- Start Start)
+			(+ Start Start)
+                     )
+           )))
+
+(synth-fun g1 ((p1 Int) (P1 Int)) Int
+	   ((Start Int (
+			p1
+			P1
+			(- Start Start)
+			(+ Start Start)
+                     )
+           )))
+
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (+ (f1 x y) (f1 x y)) (f2 x y)))
+(constraint (= (- (+ (f1 x y) (f2 x y)) y) (f3 x y)))
+(constraint (= (+ (f2 x y) (f2 x y)) (f4 x y))) 
+(constraint (= (+ (f4 x y) (f1 x y)) (f5 x y))) 
+
+(constraint (= (- (f1 x y) y) (g1 x y)))
+
+
+(check-synth)
+
+;; possible solution
+;; f1: y+x+1
+;; f2: y+2x+2
+;; f3: y+3x+3
+;; f4: 4y+4x+4
+;; f5: 5y+5x+5
+;; g1: x+1
+;; g2: y+2
+;; g3: y+3
+;; g4: 2y+6
+;; g5: 3y+x+7
+
diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress2/sygus/vcb.sy
new file mode 100644
index 000000000..9cc2389f3
--- /dev/null
+++ b/test/regress/regress2/sygus/vcb.sy
@@ -0,0 +1,54 @@
+(set-logic LIA)
+
+(synth-fun f1 ((x1 Int) (x2 Int)) Int)
+
+(synth-fun f2 ((x1 Int) (x2 Int)) Int)
+
+(define-fun vmin () Int 1)
+(define-fun vmax () Int 2)
+
+(define-fun AllZero ((v1 Int) (v2 Int)) Bool
+	    (and (= v1 0) (= v2 0)))
+
+(define-fun InV ((v1 Int) (v2 Int)) Bool
+	    (and (and (and (>= v1 vmin) (<= v1 vmax)) (>= v2 vmin)) (<= v2 vmax)))
+
+(define-fun InVorZero ((v1 Int) (v2 Int)) Bool
+	    (or (InV v1 v2) (AllZero v1 v2)))
+
+(define-fun UnsafeSame ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool
+	    (or (and (>= x1 x2) (>= (+ x2 v2) (+ x1 v1)))
+	    	(and (>= x2 x1) (>= (+ x1 v1) (+ x2 v2)))))
+
+(define-fun BadSame ((x1 Int) (x2 Int)) Bool
+	    (= x1 x2))
+
+(define-fun Bad ((x1 Int) (x2 Int)) Bool
+	    (BadSame x1 x2))
+
+(define-fun Unsafe ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool
+	    (UnsafeSame x1 x2 v1 v2))
+
+
+(declare-var x1 Int)
+(declare-var x2 Int)
+(declare-var v1 Int)
+(declare-var v2 Int)
+
+(constraint (InVorZero (f1 x1 x2) (f2 x1 x2)))
+
+(constraint (or (or (not (InV v1 v2))
+                    (AllZero (f1 x1 x2) (f2 x1 x2)))
+                (and (not (Unsafe x1 x2 (f1 x1 x2) (f2 x1 x2)))
+                     (not (AllZero (f1 (+ x1 (f1 x1 x2)) (+ x2 (f2 x1 x2)))
+                                   (f2 (+ x1 (f1 x1 x2)) (+ x2 (f2 x1 x2))))))))
+
+(constraint (or (or (or (not (InV v1 v2))
+	    	    	(Unsafe x1 x2 v1 v2))
+				   (AllZero (f1 (+ x1 v1) (+ x2 v2)) (f2 (+ x1 v1) (+ x2 v2))))
+                (not (AllZero (f1 x1 x2) (f2 x1 x2)))))
+
+
+(constraint (or (Bad x1 x2) (not (AllZero (f1 x1 x2) (f2 x1 x2)))))
+
+(check-synth)
\ No newline at end of file