Use original quantified formula for single invocation reconstruction (#5129)

This fixes an issue with single invocation solution reconstruction where the preprocessed quantified formula contains internal skolems, thus prohibiting reconstruction. The solution is to use the original quantified formula when doing solution reconstruction. This adds a regression demonstrating the issue.

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 3b7c25ff28ecf58d4808b4d9976f3f1e9266bde6..4ab92f6a71854e1510dec1dad2559c58371354e3 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -402,12 +402,14 @@ bool CegSingleInv::solve()
     siSmt->getInstantiationTermVectors(q, tvecs);
     Trace("sygus-si") << "#instantiations of " << q << "=" << tvecs.size()
                       << std::endl;
+    // We use the original synthesis conjecture siq, since qn may contain
+    // internal symbols e.g. termITE skolem after preprocessing.
     std::vector<Node> vars;
-    for (const Node& v : qn[0])
+    for (const Node& v : siq[0])
     {
       vars.push_back(v);
     }
-    Node body = qn[1];
+    Node body = siq[1];
     for (unsigned i = 0, ninsts = tvecs.size(); i < ninsts; i++)
     {
       std::vector<Expr>& tvi = tvecs[i];
@@ -418,6 +420,8 @@ bool CegSingleInv::solve()
       }
       Trace("sygus-si") << "  Instantiation: " << inst << std::endl;
       d_inst.push_back(inst);
+      // instantiation should have same arity since we are not allowed to
+      // eliminate variables from quantifiers marked with QuantElimAttribute.
       Assert(inst.size() == vars.size());
       Node ilem =
           body.substitute(vars.begin(), vars.end(), inst.begin(), inst.end());
@@ -573,6 +577,9 @@ Node CegSingleInv::reconstructToSyntax(Node s,
     // In this case, we fail, since the solution is not valid.
     Trace("csi-sol") << "FAIL : solution " << d_solution
                      << " contains free constants." << std::endl;
+    Warning() <<
+        "Cannot get synth function: free constants encountered in synthesis "
+        "solution.";
     reconstructed = -1;
   }
   if( Trace.isOn("cegqi-stats") ){

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fc2167a4a1354dabc818a22cc2496fb588ebc15a..8273eb30540f6cac9c39e9a588fed4b7722965d0 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1942,6 +1942,7 @@ set(regress_1_tests
   regress1/sygus/fg_polynomial3.sy
   regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy
   regress1/sygus/find_sc_bvult_bvnot.sy
+  regress1/sygus/ground-ite-free-constant-si.sy
   regress1/sygus/hd-01-d1-prog.sy
   regress1/sygus/hd-19-d1-prog-dup-op.sy
   regress1/sygus/hd-sdiv.sy

diff --git a/test/regress/regress1/sygus/ground-ite-free-constant-si.sy b/test/regress/regress1/sygus/ground-ite-free-constant-si.sy
new file mode 100644 (file)
index 0000000..1d72413
--- /dev/null
+++ b/test/regress/regress1/sygus/ground-ite-free-constant-si.sy
@@ -0,0 +1,33 @@
+; EXPECT: unsat
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic BV)
+
+(synth-fun inv ((s (_ BitVec 4)) (t (_ BitVec 4))) (_ BitVec 4))
+(declare-var s (_ BitVec 4))
+(declare-var t (_ BitVec 4))
+(define-fun udivtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4)
+  (ite (= b #x0) #xF (bvudiv a b))
+)
+(define-fun uremtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4)
+  (ite (= b #x0) a (bvurem a b))
+)
+(define-fun min () (_ BitVec 4)
+  (bvnot (bvlshr (bvnot #x0) #x1))
+)
+(define-fun max () (_ BitVec 4)
+  (bvnot min)
+)
+(define-fun l ( (s (_ BitVec 4)) (t (_ BitVec 4))) Bool 
+     (= (udivtotal s (inv s t)) t)
+)
+(define-fun SC ((s (_ BitVec 4)) (t (_ BitVec 4))) Bool 
+    (= (udivtotal s (udivtotal s t)) t)
+)
+(constraint
+  (=> 
+    (SC s t)
+    (l s t)
+  )
+)
+
+(check-synth)