From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 4 Dec 2019 20:34:46 +0000 (-0600)
Subject: Fix single invocation solution construction for multiple function case (#3516)
X-Git-Tag: cvc5-1.0.0~3802
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=42d1c64f7d7af06d988bf4f6bf3f20836c78a8eb;p=cvc5.git

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 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)