Fix backtracking issue in sygus fast enumerator (#3593)

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index f6ec58f5615188c75ddfaca0c6e68e148e1db716..3a79a526a3516633b712766aa55530d1b70d3e2b 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -871,12 +871,21 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal()
         // if not, there is no use continuing.
         if (initializeChildren())
         {
-          Trace("sygus-enum-debug2") << "master(" << d_tn << "): success\n";
+          Trace("sygus-enum-debug2")
+              << "master(" << d_tn << "): success init children\n";
           Assert(d_currChildSize + d_ccWeight <= d_currSize);
           incSuccess = true;
         }
+        else
+        {
+          // failed to initialize the remaining children (likely due to a
+          // child having a non-zero minimum size bound).
+          Trace("sygus-enum-debug2")
+              << "master(" << d_tn << "): fail init children\n";
+          d_currChildSize -= d_children[i].getCurrentSize();
+        }
       }
-      else
+      if (!incSuccess)
       {
         Trace("sygus-enum-debug2") << "master(" << d_tn
                                    << "): fail, backtrack...\n";
@@ -900,14 +909,16 @@ bool SygusEnumerator::TermEnumMaster::initializeChildren()
       << "master(" << d_tn << "): init children, start = " << d_childrenValid
       << ", #types=" << d_ccTypes.size() << ", sizes=" << d_currChildSize << "/"
       << d_currSize << std::endl;
+  unsigned currChildren = d_childrenValid;
   unsigned sizeMin = 0;
   // while we need to initialize the current child
   while (d_childrenValid < d_ccTypes.size())
   {
     if (!initializeChild(d_childrenValid, sizeMin))
     {
-      if (d_childrenValid == 0)
+      if (d_childrenValid == currChildren)
       {
+        // we are back to the child we started with, we terminate now.
         Trace("sygus-enum-debug2") << "master(" << d_tn
                                    << "): init children : failed, finished"
                                    << std::endl;

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h
index d4c466b034d2f1c77f2ce44c3ffc51dee8758d99..c9d1d8fca304580fddcb9bd97deef905d7ddc608 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.h
@@ -353,15 +353,16 @@ class SygusEnumerator : public EnumValGenerator
     unsigned d_childrenValid;
     /** initialize children
      *
-     * Initialize all the uninitialized children of this enumerator. If this
-     * method returns true, then all children d_children are successfully
+     * Initialize all the remaining uninitialized children of this enumerator.
+     * If this method returns true, then each of d_children are
      * initialized to be slave enumerators of the argument types indicated by
      * d_ccTypes, and the sum of their current sizes (d_currChildSize) is
      * exactly (d_currSize - d_ccWeight). If this method returns false, then
      * it was not possible to initialize the children such that they meet the
      * size requirements, and such that the assignments from children to size
-     * has not already been considered. In this case, d_children is cleared
-     * and d_currChildSize and d_childrenValid are reset.
+     * has not already been considered. In this case, all updates to d_children
+     * are reverted and d_currChildSize and d_childrenValid are reset to their
+     * values prior to this call.
      */
     bool initializeChildren();
     /** initialize child

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 22848ff9786d62bfa5296b50e1f9542d97982a44..f8608a34db4f602bda3f202812b9ebd0e997e31e 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1751,6 +1751,7 @@ set(regress_1_tests
   regress1/sygus/dup-op.sy
   regress1/sygus/error1-dt.sy
   regress1/sygus/extract.sy
+  regress1/sygus/fast-enum-backtrack.sy
   regress1/sygus/fg_polynomial3.sy
   regress1/sygus/find_sc_bvult_bvnot.sy
   regress1/sygus/hd-01-d1-prog.sy

diff --git a/test/regress/regress1/sygus/fast-enum-backtrack.sy b/test/regress/regress1/sygus/fast-enum-backtrack.sy
new file mode 100644 (file)
index 0000000..73a3dc2
--- /dev/null
+++ b/test/regress/regress1/sygus/fast-enum-backtrack.sy
@@ -0,0 +1,32 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-active-gen=enum
+
+(set-logic ALL)
+
+(declare-datatype Formula (
+  (P (Id Int))
+  (Op1 (op1 Int) (f Formula))
+  (Op2 (op2 Int) (f1 Formula) (f2 Formula))
+  )
+)
+
+(synth-fun phi () Formula
+  ((<F> Formula) (<O2> Int))
+  ((<F> Formula (
+     (P <O2>)
+     (Op1 <O2> <F>)
+     (Op2 <O2> <F> <F>)
+     )
+   )
+   (<O2> Int (0 1))
+   )
+)
+(define-fun holds ((f Formula)) Bool
+  (and ((_ is Op2) f) (= (op2 f) 1))
+)
+(define-fun holds2 ((f Formula)) Bool
+  (and ((_ is Op2) f) (= (op1 (f1 f)) 1))
+)
+(constraint (holds phi))
+(check-synth)
+