diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-04 14:34:46 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-04 14:34:46 -0600 |
commit | 42d1c64f7d7af06d988bf4f6bf3f20836c78a8eb (patch) | |
tree | 87999e54bd96bd1c4ac9702af8b3a439f58bb745 /src | |
parent | f3d40cc254026805259c511dd706d87a130c807e (diff) |
Fix single invocation solution construction for multiple function case (#3516)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 22 |
1 files changed, 16 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]; |