From 6ad02b5e0599149e0bd1548855aec8ac890f5a87 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 26 Sep 2020 08:51:57 -0500 Subject: [PATCH] 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. --- .../sygus/ce_guided_single_inv.cpp | 11 +++++-- test/regress/CMakeLists.txt | 1 + .../sygus/ground-ite-free-constant-si.sy | 33 +++++++++++++++++++ 3 files changed, 43 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/sygus/ground-ite-free-constant-si.sy diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 3b7c25ff2..4ab92f6a7 100644 --- 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 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& 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 fc2167a4a..8273eb305 100644 --- 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 index 000000000..1d7241399 --- /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) -- 2.30.2