From: Andrew Reynolds Date: Wed, 23 Mar 2022 00:05:38 +0000 (-0500) Subject: Fix non-termination issue in sygus enumerator (#8340) X-Git-Tag: cvc5-1.0.0~204 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25c955b38086b2342e5b61f0dc0440002ac71d08;p=cvc5.git 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 cf7ee36a6..2b2fa0685 100644 --- 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 bd8684929..7a55d936c 100644 --- 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 594cde97f..f00179307 100644 --- 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 84eb54499..df725ac55 100644 --- 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 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& n, std::vector& v, bool& activeIncomplete) { + Trace("sygus-engine-debug") << "getEnumeratedValues" << std::endl; std::vector ncheck = n; n.clear(); bool ret = true; @@ -695,7 +697,9 @@ bool SynthConjecture::getEnumeratedValues(std::vector& 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 a0a453ba5..0c2b4e146 100644 --- 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 index 000000000..e089dafa5 --- /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)