Fix non-termination issue in sygus enumerator (#8340)

This ensures that the sygus enumerator does not get stuck in rare cases.

In particular this is important when doing PBE and one of the enumerators (among return/condition enumeration) is out of values. This ensures we break when we fail to increment an enumerator for a type that is required to validate a child enumerator.

diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp
index cf7ee36a6fa468901ac1a2dd7e3c8af16ac8e10d..2b2fa0685e9e7fdd1a136f2992522ee4fa5acfde 100644 (file)
--- a/src/theory/quantifiers/sygus/enum_value_manager.cpp
+++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp
@@ -55,6 +55,8 @@ EnumValueManager::~EnumValueManager() {}
 
 Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
 {
+  Trace("sygus-engine-debug2") << "get enumerated value " << d_enum << " "
+                               << d_enum.getType() << std::endl;
   Node e = d_enum;
   bool isEnum = d_tds->isEnumerator(e);
 
@@ -63,14 +65,14 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
     // if the current model value of e was not registered by the datatypes
     // sygus solver, or was excluded by symmetry breaking, then it does not
     // have a proper model value that we should consider, thus we return null.
-    Trace("sygus-engine-debug")
-        << "Enumerator " << e << " does not have proper model value."
-        << std::endl;
+    Trace("sygus-engine-debug2")
+        << "...does not have proper model value." << std::endl;
     return Node::null();
   }
 
   if (!isEnum || d_tds->isPassiveEnumerator(e))
   {
+    Trace("sygus-engine-debug2") << "...take model value" << std::endl;
     return getModelValue(e);
   }
 
@@ -135,8 +137,8 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
   // if we have a waiting value, return it
   if (!d_evActiveGenWaiting.isNull())
   {
-    Trace("sygus-active-gen-debug")
-        << "Active-gen: return waiting " << d_evActiveGenWaiting << std::endl;
+    Trace("sygus-engine-debug2")
+        << "...return waiting " << d_evActiveGenWaiting << std::endl;
     return d_evActiveGenWaiting;
   }
   // Check if there is an (abstract) value absE we were actively generating
@@ -162,7 +164,9 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
   bool inc = true;
   if (!firstTime)
   {
+    Trace("sygus-engine-debug2") << "Increment enum" << std::endl;
     inc = d_evg->increment();
+    Trace("sygus-engine-debug2") << "...finish" << std::endl;
   }
   Node v;
   if (inc)

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index bd8684929487614085c1658bff24c7591eb0368b..7a55d936c29bd306dace06a24afc614499dbed3a 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -391,11 +391,15 @@ unsigned SygusEnumerator::TermCache::getNumTerms() const
 
 bool SygusEnumerator::TermCache::isComplete() const { return d_isComplete; }
 void SygusEnumerator::TermCache::setComplete() { d_isComplete = true; }
-unsigned SygusEnumerator::TermEnum::getCurrentSize() { return d_currSize; }
+unsigned SygusEnumerator::TermEnum::getCurrentSize() const
+{
+  return d_currSize;
+}
 SygusEnumerator::TermEnum::TermEnum() : d_se(nullptr), d_currSize(0) {}
 SygusEnumerator::TermEnumSlave::TermEnumSlave()
     : TermEnum(),
       d_sizeLim(0),
+      d_indexValid(false),
       d_index(0),
       d_indexNextEnd(0),
       d_hasIndexNextEnd(false),
@@ -436,6 +440,7 @@ bool SygusEnumerator::TermEnumSlave::initialize(SygusEnumerator* se,
     Trace("sygus-enum-debug2") << "slave(" << d_tn
                                << "): ...success init force master\n";
   }
+  d_indexValid = false;
   d_index = tc.getIndexForSize(d_currSize);
   Trace("sygus-enum-debug2") << "slave(" << d_tn << "): validate indices...\n";
   // initialize the next end index (marks where size increments)
@@ -454,6 +459,10 @@ bool SygusEnumerator::TermEnumSlave::initialize(SygusEnumerator* se,
 
 Node SygusEnumerator::TermEnumSlave::getCurrent()
 {
+  if (!d_indexValid)
+  {
+    return Node::null();
+  }
   SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
   Node curr = tc.getTerm(d_index);
   Trace("sygus-enum-debug2")
@@ -478,10 +487,11 @@ bool SygusEnumerator::TermEnumSlave::increment()
 
 bool SygusEnumerator::TermEnumSlave::validateIndex()
 {
+  d_indexValid = false;
   Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : validate index...\n";
   SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
   // ensure that index is in the range
-  while (d_index >= tc.getNumTerms())
+  if (d_index >= tc.getNumTerms())
   {
     Assert(d_index == tc.getNumTerms());
     Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : force master...\n";
@@ -501,6 +511,16 @@ bool SygusEnumerator::TermEnumSlave::validateIndex()
     }
     Trace("sygus-enum-debug2") << "slave(" << d_tn
                                << ") : ...success force master\n";
+    if (d_index >= tc.getNumTerms())
+    {
+      // will try this index again
+      d_index--;
+      // The master may have incremented successfully but did not add any
+      // terms to the database, in the case it returns null and breaks. In
+      // this case, we break as well. We return "true" with d_indexValid false
+      // to indicate that we are done, but will return the null term.
+      return true;
+    }
   }
   // always validate the next index end here
   validateIndexNextEnd();
@@ -521,6 +541,7 @@ bool SygusEnumerator::TermEnumSlave::validateIndex()
     validateIndexNextEnd();
   }
   Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : finished\n";
+  d_indexValid = true;
   return true;
 }
 
@@ -975,6 +996,9 @@ bool SygusEnumerator::TermEnumMaster::initializeChild(unsigned i,
   Assert(d_ccWeight <= d_currSize);
   Assert(d_currChildSize + d_ccWeight <= d_currSize);
   unsigned sizeMax = (d_currSize - d_ccWeight) - d_currChildSize;
+  // size should be bound by the size of the top-level enumerator
+  Assert(d_se->d_tlEnum == nullptr
+         || sizeMax <= d_se->d_tlEnum->getCurrentSize());
   Trace("sygus-enum-debug2") << "master(" << d_tn << "): initializeChild " << i
                              << " (" << d_currSize << ", " << d_ccWeight << ", "
                              << d_currChildSize << ")\n";

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h
index 594cde97f0aea0114bcc37aa76855457a62cc5ee..f00179307e28b903da8212a267b5b21746853518 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.h
@@ -243,7 +243,7 @@ class SygusEnumerator : public EnumValGenerator
     TermEnum();
     virtual ~TermEnum() {}
     /** get the current size of terms we are enumerating */
-    unsigned getCurrentSize();
+    unsigned getCurrentSize() const;
     /** get the current term of the enumerator */
     virtual Node getCurrent() = 0;
     /** increment the enumerator, return false if the enumerator is finished */
@@ -300,6 +300,8 @@ class SygusEnumerator : public EnumValGenerator
    private:
     /** the maximum size of terms this enumerator should enumerate */
     unsigned d_sizeLim;
+    /** is the index valid? */
+    bool d_indexValid;
     /** the current index in the term cache we are considering */
     unsigned d_index;
     /** the index in the term cache where terms of the current size end */

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 84eb5449992e30e911077f705db0601a775f2fc0..df725ac5572d5fd93728255750eed3fb95702bf3 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -351,8 +351,8 @@ bool SynthConjecture::doCheck()
 
   Assert(!d_candidates.empty());
 
-  Trace("cegqi-check") << "CegConjuncture : check, build candidates..."
-                       << std::endl;
+  Trace("sygus-engine-debug")
+      << "CegConjuncture : check, build candidates..." << std::endl;
   std::vector<Node> candidate_values;
   bool constructed_cand = false;
 
@@ -493,14 +493,15 @@ bool SynthConjecture::doCheck()
   Node query;
   if (constructed_cand)
   {
-    if (TraceIsOn("cegqi-check"))
+    if (TraceIsOn("sygus-engine-debug"))
     {
-      Trace("cegqi-check") << "CegConjuncture : check candidate : "
-                           << std::endl;
+      Trace("sygus-engine-debug")
+          << "CegConjuncture : check candidate : " << std::endl;
       for (unsigned i = 0, size = candidate_values.size(); i < size; i++)
       {
-        Trace("cegqi-check") << "  " << i << " : " << d_candidates[i] << " -> "
-                             << candidate_values[i] << std::endl;
+        Trace("sygus-engine-debug")
+            << "  " << i << " : " << d_candidates[i] << " -> "
+            << candidate_values[i] << std::endl;
       }
     }
     Assert(candidate_values.size() == d_candidates.size());
@@ -676,6 +677,7 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
                                           std::vector<Node>& v,
                                           bool& activeIncomplete)
 {
+  Trace("sygus-engine-debug") << "getEnumeratedValues" << std::endl;
   std::vector<Node> ncheck = n;
   n.clear();
   bool ret = true;
@@ -695,7 +697,9 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
       }
     }
     EnumValueManager* eman = getEnumValueManagerFor(e);
+    Trace("sygus-engine-debug2") << "- get value for " << e << std::endl;
     Node nv = eman->getEnumeratedValue(activeIncomplete);
+    Trace("sygus-engine-debug2") << "  ...return " << nv << std::endl;
     n.push_back(e);
     v.push_back(nv);
     ret = ret && !nv.isNull();

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index a0a453ba50c3b0763c7cfe1bb2d82bb818858814..0c2b4e1469fa0c5a8e6e1e985e3faa55688e5fe3 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2638,6 +2638,7 @@ set(regress_1_tests
   regress1/sygus/crci-ssb-unk.sy
   regress1/sygus/crcy-si.sy
   regress1/sygus/cube-nia.sy
+  regress1/sygus/discPresent.sy
   regress1/sygus/double.sy
   regress1/sygus/dt-test-ns.sy
   regress1/sygus/dup-op.sy

diff --git a/test/regress/cli/regress1/sygus/discPresent.sy b/test/regress/cli/regress1/sygus/discPresent.sy
new file mode 100644 (file)
index 0000000..e089daf
--- /dev/null
+++ b/test/regress/cli/regress1/sygus/discPresent.sy
@@ -0,0 +1,145 @@
+; COMMAND-LINE: --sygus-out=status
+; EXPECT: unsat
+(set-logic LIA)
+
+;declare enums
+
+(declare-datatypes ((prev_dw.is_c4_model_t 0))
+       (((prev_dw.is_c4_modelIN_DiscPresent) (prev_dw.is_c4_modelIN_Ejecting) (prev_dw.is_c4_modelIN_Empty) (prev_dw.is_c4_modelIN_Inserting) (prev_dw.is_c4_modelIN_NO_ACTIVE_CHILD) )))
+(declare-datatypes ((prev_dw.is_c1_model_t 0))
+       (((prev_dw.is_c1_modelIN_Eject) (prev_dw.is_c1_modelIN_ModeManager) (prev_dw.is_c1_modelIN_NO_ACTIVE_CHILD) )))
+(declare-datatypes ((prev_dw.is_ModeManager_t 0))
+       (((prev_dw.is_ModeManagerIN_NO_ACTIVE_CHILD) (prev_dw.is_ModeManagerIN_ON) (prev_dw.is_ModeManagerIN_Standby) )))
+(declare-datatypes ((prev_dw.was_ModeManager_t 0))
+       (((prev_dw.was_ModeManagerIN_NO_ACTIVE_CHILD) (prev_dw.was_ModeManagerIN_ON) (prev_dw.was_ModeManagerIN_Standby) )))
+(declare-datatypes ((prev_dw.is_ON_t 0))
+       (((prev_dw.is_ONIN_AMMode) (prev_dw.is_ONIN_CDMode) (prev_dw.is_ONIN_FMMode) (prev_dw.is_ONIN_NO_ACTIVE_CHILD) )))
+(declare-datatypes ((prev_dw.was_ON_t 0))
+       (((prev_dw.was_ONIN_AMMode) (prev_dw.was_ONIN_CDMode) (prev_dw.was_ONIN_FMMode) (prev_dw.was_ONIN_NO_ACTIVE_CHILD) )))
+(declare-datatypes ((prev_dw.RadioReq_start_t 0))
+       (((prev_dw.RadioReq_startAM) (prev_dw.RadioReq_startCD) (prev_dw.RadioReq_startFM) (prev_dw.RadioReq_startOFF) )))
+(declare-datatypes ((rtU.RadioReq_t 0))
+       (((rtU.RadioReqAM) (rtU.RadioReqCD) (rtU.RadioReqFM) (rtU.RadioReqOFF) )))
+(declare-datatypes ((rtY.MechCmd_t 0))
+       (((rtY.MechCmdDISCINSERT) (rtY.MechCmdEJECT) (rtY.MechCmdEMPTY) (rtY.MechCmdPLAY) (rtY.MechCmdREW) (rtY.MechCmdSTOP) )))
+
+
+;function to be synthesised
+
+(synth-fun next ((prev_dw.is_c4_model prev_dw.is_c4_model_t)(prev_dw.is_c1_model prev_dw.is_c1_model_t)(prev_dw.is_ModeManager prev_dw.is_ModeManager_t)(prev_dw.was_ModeManager prev_dw.was_ModeManager_t)(prev_dw.is_ON prev_dw.is_ON_t)(prev_dw.was_ON prev_dw.was_ON_t)(prev_dw.temporalCounter_i1 Int) (prev_dw.RadioReq_start prev_dw.RadioReq_start_t)(rtU.DiscInsert Bool) (rtU.RadioReq rtU.RadioReq_t)(rtU.DiscEject Bool) (rtY.MechCmd rtY.MechCmd_t)) Int
+       ((Start Int)  (Var Int) (EnumVar0 prev_dw.is_c4_model_t) (EnumVar1 prev_dw.is_c1_model_t) (EnumVar2 prev_dw.is_ModeManager_t) (EnumVar3 prev_dw.was_ModeManager_t) (EnumVar4 prev_dw.is_ON_t) (EnumVar5 prev_dw.was_ON_t) (EnumVar6 prev_dw.RadioReq_start_t) (EnumVar7 rtU.RadioReq_t) (EnumVar8 rtY.MechCmd_t) (StartBool Bool))
+       ((Start Int (
+                                0
+                                1
+                                (ite StartBool Start Start)))
+
+       (Var Int (
+                                1
+                                2
+                                101
+                                prev_dw.temporalCounter_i1
+                                (abs Var)                                              
+                                (+ Var Var)                                            
+                                (- Var Var)                                            
+                                (* Var Var)))
+
+       (EnumVar0 prev_dw.is_c4_model_t (
+                               prev_dw.is_c4_model
+                               prev_dw.is_c4_modelIN_DiscPresent
+                               prev_dw.is_c4_modelIN_Ejecting
+                               prev_dw.is_c4_modelIN_Empty
+                               prev_dw.is_c4_modelIN_Inserting
+                               prev_dw.is_c4_modelIN_NO_ACTIVE_CHILD
+       ))
+
+       (EnumVar1 prev_dw.is_c1_model_t (
+                               prev_dw.is_c1_model
+                               prev_dw.is_c1_modelIN_Eject
+                               prev_dw.is_c1_modelIN_ModeManager
+                               prev_dw.is_c1_modelIN_NO_ACTIVE_CHILD
+       ))
+
+       (EnumVar2 prev_dw.is_ModeManager_t (
+                               prev_dw.is_ModeManager
+                               prev_dw.is_ModeManagerIN_NO_ACTIVE_CHILD
+                               prev_dw.is_ModeManagerIN_ON
+                               prev_dw.is_ModeManagerIN_Standby
+       ))
+
+       (EnumVar3 prev_dw.was_ModeManager_t (
+                               prev_dw.was_ModeManager
+                               prev_dw.was_ModeManagerIN_NO_ACTIVE_CHILD
+                               prev_dw.was_ModeManagerIN_ON
+                               prev_dw.was_ModeManagerIN_Standby
+       ))
+
+       (EnumVar4 prev_dw.is_ON_t (
+                               prev_dw.is_ON
+                               prev_dw.is_ONIN_AMMode
+                               prev_dw.is_ONIN_CDMode
+                               prev_dw.is_ONIN_FMMode
+                               prev_dw.is_ONIN_NO_ACTIVE_CHILD
+       ))
+
+       (EnumVar5 prev_dw.was_ON_t (
+                               prev_dw.was_ON
+                               prev_dw.was_ONIN_AMMode
+                               prev_dw.was_ONIN_CDMode
+                               prev_dw.was_ONIN_FMMode
+                               prev_dw.was_ONIN_NO_ACTIVE_CHILD
+       ))
+
+       (EnumVar6 prev_dw.RadioReq_start_t (
+                               prev_dw.RadioReq_start
+                               prev_dw.RadioReq_startAM
+                               prev_dw.RadioReq_startCD
+                               prev_dw.RadioReq_startFM
+                               prev_dw.RadioReq_startOFF
+       ))
+
+       (EnumVar7 rtU.RadioReq_t (
+                               rtU.RadioReq
+                               rtU.RadioReqAM
+                               rtU.RadioReqCD
+                               rtU.RadioReqFM
+                               rtU.RadioReqOFF
+       ))
+
+       (EnumVar8 rtY.MechCmd_t (
+                               rtY.MechCmd
+                               rtY.MechCmdDISCINSERT
+                               rtY.MechCmdEJECT
+                               rtY.MechCmdEMPTY
+                               rtY.MechCmdPLAY
+                               rtY.MechCmdREW
+                               rtY.MechCmdSTOP
+       ))
+
+       (StartBool Bool (
+                                rtU.DiscInsert
+                                rtU.DiscEject
+                 (> Var Var)                                            
+                 (>= Var Var)                                           
+                 (< Var Var)                                            
+                 (<= Var Var)                                           
+                 (= Var Var)                                            
+                                ( = EnumVar0 EnumVar0)
+                                ( = EnumVar1 EnumVar1)
+                                ( = EnumVar2 EnumVar2)
+                                ( = EnumVar3 EnumVar3)
+                                ( = EnumVar4 EnumVar4)
+                                ( = EnumVar5 EnumVar5)
+                                ( = EnumVar6 EnumVar6)
+                                ( = EnumVar7 EnumVar7)
+                                ( = EnumVar8 EnumVar8)
+                                (and StartBool StartBool)                      
+                                (or  StartBool StartBool)                              
+                                (not StartBool)))))
+
+;constraints
+
+;c1
+(constraint (= (next prev_dw.is_c4_modelIN_DiscPresent prev_dw.is_c1_modelIN_ModeManager prev_dw.is_ModeManagerIN_ON prev_dw.was_ModeManagerIN_ON prev_dw.is_ONIN_CDMode prev_dw.was_ONIN_CDMode 101 prev_dw.RadioReq_startAM true rtU.RadioReqCD false rtY.MechCmdPLAY ) 0))
+;c2
+(constraint (= (next prev_dw.is_c4_modelIN_DiscPresent prev_dw.is_c1_modelIN_ModeManager prev_dw.is_ModeManagerIN_ON prev_dw.was_ModeManagerIN_ON prev_dw.is_ONIN_CDMode prev_dw.was_ONIN_CDMode 101 prev_dw.RadioReq_startAM true rtU.RadioReqFM false rtY.MechCmdSTOP ) 1))
+(check-synth)