From 88f1c68a94bd998854cb0bf3a1ce3f516cb774f8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Jan 2020 15:31:26 -0600 Subject: [PATCH] Fix backtracking issue in sygus fast enumerator (#3593) --- .../quantifiers/sygus/sygus_enumerator.cpp | 17 ++++++++-- .../quantifiers/sygus/sygus_enumerator.h | 9 +++--- test/regress/CMakeLists.txt | 1 + .../regress1/sygus/fast-enum-backtrack.sy | 32 +++++++++++++++++++ 4 files changed, 52 insertions(+), 7 deletions(-) create mode 100644 test/regress/regress1/sygus/fast-enum-backtrack.sy diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index f6ec58f56..3a79a526a 100644 --- 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 d4c466b03..c9d1d8fca 100644 --- 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 22848ff97..f8608a34d 100644 --- 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 index 000000000..73a3dc2e2 --- /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 + (( Formula) ( Int)) + (( Formula ( + (P ) + (Op1 ) + (Op2 ) + ) + ) + ( 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) + -- 2.30.2