Fix single invocation solution construction for multiple function case (#3516)

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index c34b7d4e31f31ca4ba89580c57b9de58fd659747..61d891f757e35b78c8a93e87e6c6189de5f70f39 100644 (file)
--- 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 510316ae3e24d3e0a370af1bad73d5c3672819e1..cf06d2e90a926d4a49409f692b0b0491bad0909a 100644 (file)
--- 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 (file)
index 0000000..dd6011d
--- /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)