diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-26 08:51:57 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-26 08:51:57 -0500 |
| commit | 6ad02b5e0599149e0bd1548855aec8ac890f5a87 (patch) | |
| tree | 5607fd85c45102426314241f193bec9bc2308040 /src/theory/quantifiers | |
| parent | 160a3f55bf4dbfdbc1385ce4898c62b1fd3a8c78 (diff) | |
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.
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
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<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") ){ |