diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 22 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue3514.smt2 | 13 |
3 files changed, 30 insertions, 6 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index c34b7d4e3..61d891f75 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -502,12 +502,22 @@ Node CegSingleInv::getSolution(unsigned sol_index, indices.push_back(i); } Assert(!indices.empty()); - //sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions) - // TODO : to minimize solution size, put the largest term last - sortSiInstanceIndices ssii; - ssii.d_ccsi = this; - ssii.d_i = sol_index; - std::sort( indices.begin(), indices.end(), ssii ); + // We are constructing an ITE based on the list of instantiations. We + // sort this list based on heuristic. Currently, we do all constant values + // first since this leads to simpler conditions. Notice that we only allow + // sorting if we have a single variable, since the correctness of + // Proposition 1 of Reynolds et al CAV 2015 for the case of multiple + // functions-to-synthesize requires that the instantiations come in the + // same order for all functions. Thus, we cannot decide on an order for + // instantiations independently, since this may lead to incorrect solutions. + bool allowSort = (d_quant[0].getNumChildren() == 1); + if (allowSort) + { + sortSiInstanceIndices ssii; + ssii.d_ccsi = this; + ssii.d_i = sol_index; + std::sort(indices.begin(), indices.end(), ssii); + } Trace("csi-sol") << "Construct solution" << std::endl; std::reverse(indices.begin(), indices.end()); s = d_inst[indices[0]][sol_index]; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 510316ae3..cf06d2e90 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1726,6 +1726,7 @@ set(regress_1_tests regress1/sygus/issue3320-quant.sy regress1/sygus/issue3461.sy regress1/sygus/issue3498.smt2 + regress1/sygus/issue3514.smt2 regress1/sygus/issue3507.smt2 regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy diff --git a/test/regress/regress1/sygus/issue3514.smt2 b/test/regress/regress1/sygus/issue3514.smt2 new file mode 100644 index 000000000..dd6011df9 --- /dev/null +++ b/test/regress/regress1/sygus/issue3514.smt2 @@ -0,0 +1,13 @@ +; EXPECT: sat +; COMMAND-LINE: --sygus-inference +(set-logic ALL) +(assert + (forall ((a Real)) + (exists ((b Real)) + (exists ((c Real)) + (and + (< (+ a c) 0.0) + (or (distinct a 0.0) (= b 5.0)) + (distinct (+ b c) 1.0) + (< c 1)))))) +(check-sat) |