1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Abdalrhman Mohamed, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Utility for processing single invocation synthesis conjectures. |
14 |
|
*/ |
15 |
|
#include "theory/quantifiers/sygus/ce_guided_single_inv.h" |
16 |
|
|
17 |
|
#include "expr/skolem_manager.h" |
18 |
|
#include "options/quantifiers_options.h" |
19 |
|
#include "smt/logic_exception.h" |
20 |
|
#include "smt/smt_statistics_registry.h" |
21 |
|
#include "theory/arith/arith_msum.h" |
22 |
|
#include "theory/quantifiers/quantifiers_attributes.h" |
23 |
|
#include "theory/quantifiers/quantifiers_rewriter.h" |
24 |
|
#include "theory/quantifiers/sygus/sygus_grammar_cons.h" |
25 |
|
#include "theory/quantifiers/sygus/sygus_reconstruct.h" |
26 |
|
#include "theory/quantifiers/sygus/sygus_utils.h" |
27 |
|
#include "theory/quantifiers/sygus/term_database_sygus.h" |
28 |
|
#include "theory/quantifiers/term_enumeration.h" |
29 |
|
#include "theory/quantifiers/term_registry.h" |
30 |
|
#include "theory/quantifiers/term_util.h" |
31 |
|
#include "theory/smt_engine_subsolver.h" |
32 |
|
|
33 |
|
using namespace cvc5::kind; |
34 |
|
|
35 |
|
namespace cvc5 { |
36 |
|
namespace theory { |
37 |
|
namespace quantifiers { |
38 |
|
|
39 |
1900 |
CegSingleInv::CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s) |
40 |
|
: EnvObj(env), |
41 |
|
d_isSolved(false), |
42 |
1900 |
d_sip(new SingleInvocationPartition), |
43 |
1900 |
d_srcons(new SygusReconstruct(env, tr.getTermDatabaseSygus(), s)), |
44 |
|
d_single_invocation(false), |
45 |
5700 |
d_treg(tr) |
46 |
|
{ |
47 |
1900 |
} |
48 |
|
|
49 |
5688 |
CegSingleInv::~CegSingleInv() |
50 |
|
{ |
51 |
1896 |
delete d_sip; // d_sip(new SingleInvocationPartition), |
52 |
3792 |
} |
53 |
|
|
54 |
542 |
void CegSingleInv::initialize(Node q) |
55 |
|
{ |
56 |
|
// can only register one quantified formula with this |
57 |
542 |
Assert(d_quant.isNull()); |
58 |
542 |
d_quant = q; |
59 |
542 |
d_simp_quant = q; |
60 |
542 |
Trace("sygus-si") << "CegSingleInv::initialize : " << q << std::endl; |
61 |
|
|
62 |
|
// decompose the conjecture |
63 |
542 |
SygusUtils::decomposeSygusConjecture(d_quant, d_funs, d_unsolvedf, d_solvedf); |
64 |
|
|
65 |
542 |
Trace("sygus-si") << "functions: " << d_funs << std::endl; |
66 |
542 |
Trace("sygus-si") << " unsolved: " << d_unsolvedf << std::endl; |
67 |
542 |
Trace("sygus-si") << " solved: " << d_solvedf << std::endl; |
68 |
|
|
69 |
|
// infer single invocation-ness |
70 |
|
|
71 |
|
// get the variables |
72 |
1057 |
std::map<Node, std::vector<Node> > progVars; |
73 |
1464 |
for (const Node& sf : q[0]) |
74 |
|
{ |
75 |
|
// get its argument list |
76 |
922 |
SygusUtils::getSygusArgumentListForSynthFun(sf, progVars[sf]); |
77 |
|
} |
78 |
|
// compute single invocation partition |
79 |
1057 |
Node qq; |
80 |
542 |
if (q[1].getKind() == NOT && q[1][0].getKind() == FORALL) |
81 |
|
{ |
82 |
318 |
qq = q[1][0][1]; |
83 |
|
} |
84 |
|
else |
85 |
|
{ |
86 |
224 |
qq = TermUtil::simpleNegate(q[1]); |
87 |
|
} |
88 |
|
// process the single invocation-ness of the property |
89 |
542 |
if (!d_sip->init(d_unsolvedf, qq)) |
90 |
|
{ |
91 |
54 |
Trace("sygus-si") << "...not single invocation (type mismatch)" |
92 |
27 |
<< std::endl; |
93 |
27 |
return; |
94 |
|
} |
95 |
1030 |
Trace("sygus-si") << "- Partitioned to single invocation parts : " |
96 |
515 |
<< std::endl; |
97 |
515 |
d_sip->debugPrint("sygus-si"); |
98 |
|
|
99 |
|
// map from program to bound variables |
100 |
1030 |
std::vector<Node> funcs; |
101 |
515 |
d_sip->getFunctions(funcs); |
102 |
1240 |
for (unsigned j = 0, size = funcs.size(); j < size; j++) |
103 |
|
{ |
104 |
725 |
Assert(std::find(d_funs.begin(), d_funs.end(), funcs[j]) != d_funs.end()); |
105 |
725 |
d_prog_to_sol_index[funcs[j]] = j; |
106 |
|
} |
107 |
|
|
108 |
|
// check if it is single invocation |
109 |
515 |
if (d_sip->isPurelySingleInvocation()) |
110 |
|
{ |
111 |
|
// We are fully single invocation, set single invocation if we haven't |
112 |
|
// disabled single invocation techniques. |
113 |
798 |
if (options().quantifiers.cegqiSingleInvMode |
114 |
399 |
!= options::CegqiSingleInvMode::NONE) |
115 |
|
{ |
116 |
306 |
d_single_invocation = true; |
117 |
|
} |
118 |
|
} |
119 |
|
} |
120 |
|
|
121 |
542 |
void CegSingleInv::finishInit(bool syntaxRestricted) |
122 |
|
{ |
123 |
542 |
Trace("sygus-si-debug") << "Single invocation: finish init" << std::endl; |
124 |
|
// do not do single invocation if grammar is restricted and |
125 |
|
// options::CegqiSingleInvMode::ALL is not enabled |
126 |
1084 |
if (options().quantifiers.cegqiSingleInvMode |
127 |
|
== options::CegqiSingleInvMode::USE |
128 |
542 |
&& d_single_invocation && syntaxRestricted) |
129 |
|
{ |
130 |
166 |
d_single_invocation = false; |
131 |
166 |
Trace("sygus-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl; |
132 |
|
} |
133 |
|
|
134 |
|
// we now have determined whether we will do single invocation techniques |
135 |
542 |
if (!d_single_invocation) |
136 |
|
{ |
137 |
402 |
d_single_inv = Node::null(); |
138 |
402 |
Trace("sygus-si") << "Formula is not single invocation." << std::endl; |
139 |
402 |
if (options().quantifiers.cegqiSingleInvAbort) |
140 |
|
{ |
141 |
|
std::stringstream ss; |
142 |
|
ss << "Property is not handled by single invocation." << std::endl; |
143 |
|
throw LogicException(ss.str()); |
144 |
|
} |
145 |
804 |
return; |
146 |
|
} |
147 |
140 |
NodeManager* nm = NodeManager::currentNM(); |
148 |
140 |
SkolemManager* sm = nm->getSkolemManager(); |
149 |
140 |
d_single_inv = d_sip->getSingleInvocation(); |
150 |
140 |
d_single_inv = TermUtil::simpleNegate(d_single_inv); |
151 |
280 |
std::vector<Node> func_vars; |
152 |
140 |
d_sip->getFunctionVariables(func_vars); |
153 |
140 |
if (!func_vars.empty()) |
154 |
|
{ |
155 |
252 |
Node pbvl = nm->mkNode(BOUND_VAR_LIST, func_vars); |
156 |
|
// make the single invocation conjecture |
157 |
126 |
d_single_inv = nm->mkNode(FORALL, pbvl, d_single_inv); |
158 |
|
} |
159 |
|
// now, introduce the skolems |
160 |
280 |
std::vector<Node> sivars; |
161 |
140 |
d_sip->getSingleInvocationVariables(sivars); |
162 |
349 |
for (unsigned i = 0, size = sivars.size(); i < size; i++) |
163 |
|
{ |
164 |
|
Node v = |
165 |
418 |
sm->mkDummySkolem("a", sivars[i].getType(), "single invocation arg"); |
166 |
209 |
d_single_inv_arg_sk.push_back(v); |
167 |
|
} |
168 |
280 |
d_single_inv = d_single_inv.substitute(sivars.begin(), |
169 |
|
sivars.end(), |
170 |
|
d_single_inv_arg_sk.begin(), |
171 |
140 |
d_single_inv_arg_sk.end()); |
172 |
280 |
Trace("sygus-si") << "Single invocation formula is : " << d_single_inv |
173 |
140 |
<< std::endl; |
174 |
|
// check whether we can handle this quantified formula |
175 |
140 |
CegHandledStatus status = CEG_HANDLED; |
176 |
140 |
if (d_single_inv.getKind() == FORALL) |
177 |
|
{ |
178 |
|
// if the conjecture is trivially solvable, set the solution |
179 |
126 |
if (solveTrivial(d_single_inv)) |
180 |
|
{ |
181 |
46 |
setSolution(); |
182 |
|
} |
183 |
|
else |
184 |
|
{ |
185 |
80 |
status = CegInstantiator::isCbqiQuant(d_single_inv); |
186 |
|
} |
187 |
|
} |
188 |
140 |
Trace("sygus-si") << "CegHandledStatus is " << status << std::endl; |
189 |
140 |
if (status < CEG_HANDLED) |
190 |
|
{ |
191 |
18 |
Trace("sygus-si") << "...do not invoke single invocation techniques since " |
192 |
|
"the quantified formula does not have a handled " |
193 |
9 |
"counterexample-guided instantiation strategy!" |
194 |
9 |
<< std::endl; |
195 |
9 |
d_single_invocation = false; |
196 |
9 |
d_single_inv = Node::null(); |
197 |
|
} |
198 |
|
} |
199 |
|
|
200 |
122 |
bool CegSingleInv::solve() |
201 |
|
{ |
202 |
122 |
if (d_single_inv.isNull()) |
203 |
|
{ |
204 |
|
// not using single invocation techniques |
205 |
|
return false; |
206 |
|
} |
207 |
122 |
if (d_isSolved) |
208 |
|
{ |
209 |
|
// already solved, probably via a call to solveTrivial. |
210 |
44 |
return true; |
211 |
|
} |
212 |
78 |
Trace("sygus-si") << "Solve using single invocation..." << std::endl; |
213 |
78 |
NodeManager* nm = NodeManager::currentNM(); |
214 |
78 |
SkolemManager* sm = nm->getSkolemManager(); |
215 |
|
// Mark the quantified formula with the quantifier elimination attribute to |
216 |
|
// ensure its structure is preserved in the query below. |
217 |
156 |
Node siq = d_single_inv; |
218 |
78 |
if (siq.getKind() == FORALL) |
219 |
|
{ |
220 |
|
Node n_attr = sm->mkDummySkolem( |
221 |
|
"qe_si", |
222 |
128 |
nm->booleanType(), |
223 |
256 |
"Auxiliary variable for qe attr for single invocation."); |
224 |
|
QuantElimAttribute qea; |
225 |
64 |
n_attr.setAttribute(qea, true); |
226 |
64 |
n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr); |
227 |
64 |
n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr); |
228 |
64 |
siq = nm->mkNode(FORALL, siq[0], siq[1], n_attr); |
229 |
|
} |
230 |
|
// solve the single invocation conjecture using a fresh copy of SMT engine |
231 |
156 |
std::unique_ptr<SolverEngine> siSmt; |
232 |
78 |
initializeSubsolver(siSmt, d_env); |
233 |
|
// do not use shared selectors in subsolver, since this leads to solutions |
234 |
|
// with non-user symbols |
235 |
78 |
siSmt->setOption("dt-share-sel", "false"); |
236 |
78 |
siSmt->assertFormula(siq); |
237 |
156 |
Result r = siSmt->checkSat(); |
238 |
78 |
Trace("sygus-si") << "Result: " << r << std::endl; |
239 |
78 |
Result::Sat res = r.asSatisfiabilityResult().isSat(); |
240 |
78 |
if (res != Result::UNSAT) |
241 |
|
{ |
242 |
8 |
warning() << "Warning : the single invocation solver determined the SyGuS " |
243 |
|
"conjecture" |
244 |
8 |
<< (res == Result::SAT ? " is" : " may be") << " infeasible" |
245 |
8 |
<< std::endl; |
246 |
|
// conjecture is infeasible or unknown |
247 |
8 |
return false; |
248 |
|
} |
249 |
|
// now, get the instantiations |
250 |
140 |
std::vector<Node> qs; |
251 |
70 |
siSmt->getInstantiatedQuantifiedFormulas(qs); |
252 |
70 |
Assert(qs.size() <= 1); |
253 |
|
// track the instantiations, as solution construction is based on this |
254 |
140 |
Trace("sygus-si") << "#instantiated quantified formulas=" << qs.size() |
255 |
70 |
<< std::endl; |
256 |
70 |
d_inst.clear(); |
257 |
70 |
d_instConds.clear(); |
258 |
70 |
if (!qs.empty()) |
259 |
|
{ |
260 |
124 |
Node q = qs[0]; |
261 |
62 |
Assert(q.getKind() == FORALL); |
262 |
62 |
siSmt->getInstantiationTermVectors(q, d_inst); |
263 |
124 |
Trace("sygus-si") << "#instantiations of " << q << "=" << d_inst.size() |
264 |
62 |
<< std::endl; |
265 |
|
// We use the original synthesis conjecture siq, since q may contain |
266 |
|
// internal symbols e.g. termITE skolem after preprocessing. |
267 |
124 |
std::vector<Node> vars; |
268 |
344 |
for (const Node& v : siq[0]) |
269 |
|
{ |
270 |
282 |
vars.push_back(v); |
271 |
|
} |
272 |
124 |
Node body = siq[1]; |
273 |
214 |
for (unsigned i = 0, ninsts = d_inst.size(); i < ninsts; i++) |
274 |
|
{ |
275 |
|
// note we do not convert to witness form here, since we could be |
276 |
|
// an internal subsolver |
277 |
152 |
std::vector<Node>& inst = d_inst[i]; |
278 |
152 |
Trace("sygus-si") << " Instantiation: " << inst << std::endl; |
279 |
|
// instantiation should have same arity since we are not allowed to |
280 |
|
// eliminate variables from quantifiers marked with QuantElimAttribute. |
281 |
152 |
Assert(inst.size() == vars.size()); |
282 |
|
Node ilem = |
283 |
304 |
body.substitute(vars.begin(), vars.end(), inst.begin(), inst.end()); |
284 |
152 |
ilem = rewrite(ilem); |
285 |
152 |
d_instConds.push_back(ilem); |
286 |
152 |
Trace("sygus-si") << " Instantiation Lemma: " << ilem << std::endl; |
287 |
|
} |
288 |
|
} |
289 |
|
// set the solution |
290 |
70 |
setSolution(); |
291 |
70 |
return true; |
292 |
|
} |
293 |
|
|
294 |
|
//TODO: use term size? |
295 |
|
struct sortSiInstanceIndices { |
296 |
|
CegSingleInv* d_ccsi; |
297 |
|
int d_i; |
298 |
182 |
bool operator() (unsigned i, unsigned j) { |
299 |
182 |
if( d_ccsi->d_inst[i][d_i].isConst() && !d_ccsi->d_inst[j][d_i].isConst() ){ |
300 |
18 |
return true; |
301 |
|
}else{ |
302 |
164 |
return false; |
303 |
|
} |
304 |
|
} |
305 |
|
}; |
306 |
|
|
307 |
225 |
Node CegSingleInv::getSolution(size_t sol_index, |
308 |
|
TypeNode stn, |
309 |
|
int8_t& reconstructed, |
310 |
|
bool rconsSygus) |
311 |
|
{ |
312 |
225 |
Assert(sol_index < d_quant[0].getNumChildren()); |
313 |
450 |
Node f = d_quant[0][sol_index]; |
314 |
225 |
Trace("csi-sol") << "CegSingleInv::getSolution " << f << std::endl; |
315 |
|
// maybe it is in the solved map already? |
316 |
225 |
if (d_solvedf.contains(f)) |
317 |
|
{ |
318 |
|
// notice that we ignore d_solutions for solved functions |
319 |
|
Trace("csi-sol") << "...return solution from annotation" << std::endl; |
320 |
|
return d_solvedf.apply(f); |
321 |
|
} |
322 |
225 |
Trace("csi-sol") << "...get solution from vector" << std::endl; |
323 |
|
|
324 |
450 |
Node s = d_solutions[sol_index]; |
325 |
450 |
Node sol = s.getKind() == LAMBDA ? s[1] : s; |
326 |
|
// must substitute to be proper variables |
327 |
225 |
const DType& dt = stn.getDType(); |
328 |
450 |
Node varList = dt.getSygusVarList(); |
329 |
225 |
Assert(d_single_inv_arg_sk.size() == varList.getNumChildren()); |
330 |
450 |
std::vector<Node> vars; |
331 |
450 |
std::vector<Node> sygusVars; |
332 |
702 |
for (size_t i = 0, nvars = d_single_inv_arg_sk.size(); i < nvars; i++) |
333 |
|
{ |
334 |
477 |
Trace("csi-sol") << d_single_inv_arg_sk[i] << " "; |
335 |
477 |
vars.push_back(d_single_inv_arg_sk[i]); |
336 |
477 |
sygusVars.push_back(varList[i]); |
337 |
|
} |
338 |
225 |
Trace("csi-sol") << std::endl; |
339 |
225 |
sol = sol.substitute( |
340 |
|
vars.begin(), vars.end(), sygusVars.begin(), sygusVars.end()); |
341 |
225 |
sol = reconstructToSyntax(sol, stn, reconstructed, rconsSygus); |
342 |
225 |
return s.getKind() == LAMBDA |
343 |
|
? NodeManager::currentNM()->mkNode(LAMBDA, s[0], sol) |
344 |
225 |
: sol; |
345 |
|
} |
346 |
|
|
347 |
381 |
Node CegSingleInv::getSolutionFromInst(size_t index) |
348 |
|
{ |
349 |
762 |
Node prog = d_quant[0][index]; |
350 |
762 |
Node s; |
351 |
|
// If it is unconstrained: either the variable does not appear in the |
352 |
|
// conjecture or the conjecture can be solved without a single instantiation. |
353 |
762 |
if (d_prog_to_sol_index.find(prog) == d_prog_to_sol_index.end() |
354 |
381 |
|| d_inst.empty()) |
355 |
|
{ |
356 |
92 |
TypeNode ptn = prog.getType(); |
357 |
46 |
if (ptn.isFunction()) |
358 |
|
{ |
359 |
40 |
ptn = ptn.getRangeType(); |
360 |
|
} |
361 |
46 |
Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl; |
362 |
46 |
s = d_treg.getTermEnumeration()->getEnumerateTerm(ptn, 0); |
363 |
|
} |
364 |
|
else |
365 |
|
{ |
366 |
335 |
Trace("csi-sol") << "Get solution for " << prog << ", with skolems : "; |
367 |
335 |
size_t sol_index = d_prog_to_sol_index[prog]; |
368 |
|
|
369 |
|
//construct the solution |
370 |
335 |
Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl; |
371 |
670 |
std::vector< unsigned > indices; |
372 |
1120 |
for (unsigned i = 0, ninst = d_inst.size(); i < ninst; i++) |
373 |
|
{ |
374 |
785 |
indices.push_back(i); |
375 |
|
} |
376 |
335 |
Assert(!indices.empty()); |
377 |
|
// We are constructing an ITE based on the list of instantiations. We |
378 |
|
// sort this list based on heuristic. Currently, we do all constant values |
379 |
|
// first since this leads to simpler conditions. Notice that we only allow |
380 |
|
// sorting if we have a single variable, since the correctness of |
381 |
|
// Proposition 1 of Reynolds et al CAV 2015 for the case of multiple |
382 |
|
// functions-to-synthesize requires that the instantiations come in the |
383 |
|
// same order for all functions. Thus, we cannot decide on an order for |
384 |
|
// instantiations independently, since this may lead to incorrect solutions. |
385 |
335 |
bool allowSort = (d_quant[0].getNumChildren() == 1); |
386 |
335 |
if (allowSort) |
387 |
|
{ |
388 |
|
sortSiInstanceIndices ssii; |
389 |
87 |
ssii.d_ccsi = this; |
390 |
87 |
ssii.d_i = sol_index; |
391 |
87 |
std::sort(indices.begin(), indices.end(), ssii); |
392 |
|
} |
393 |
335 |
Trace("csi-sol") << "Construct solution" << std::endl; |
394 |
335 |
std::reverse(indices.begin(), indices.end()); |
395 |
335 |
s = d_inst[indices[0]][sol_index]; |
396 |
|
// it is an ITE chain whose conditions are the instantiations |
397 |
335 |
NodeManager* nm = NodeManager::currentNM(); |
398 |
785 |
for (unsigned j = 1, nindices = indices.size(); j < nindices; j++) |
399 |
|
{ |
400 |
450 |
unsigned uindex = indices[j]; |
401 |
900 |
Node cond = d_instConds[uindex]; |
402 |
450 |
cond = TermUtil::simpleNegate(cond); |
403 |
450 |
s = nm->mkNode(ITE, cond, d_inst[uindex][sol_index], s); |
404 |
|
} |
405 |
|
} |
406 |
|
//simplify the solution using the extended rewriter |
407 |
381 |
Trace("csi-sol") << "Solution (pre-simplification): " << s << std::endl; |
408 |
381 |
s = extendedRewrite(s); |
409 |
381 |
Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl; |
410 |
|
// wrap into lambda, as needed |
411 |
762 |
return SygusUtils::wrapSolutionForSynthFun(prog, s); |
412 |
|
} |
413 |
|
|
414 |
116 |
void CegSingleInv::setSolution() |
415 |
|
{ |
416 |
|
// construct the solutions based on the instantiations |
417 |
116 |
d_solutions.clear(); |
418 |
116 |
d_rcSolutions.clear(); |
419 |
232 |
Subs finalSol; |
420 |
497 |
for (size_t i = 0, nvars = d_quant[0].getNumChildren(); i < nvars; i++) |
421 |
|
{ |
422 |
|
// Note this is a dummy solution for solved functions, which are given |
423 |
|
// solutions in the annotation but do not appear in the conjecture. |
424 |
762 |
Node sol = getSolutionFromInst(i); |
425 |
381 |
d_solutions.push_back(sol); |
426 |
|
// haven't reconstructed to syntax yet |
427 |
381 |
d_rcSolutions.push_back(Node::null()); |
428 |
381 |
finalSol.add(d_quant[0][i], sol); |
429 |
|
} |
430 |
116 |
d_isSolved = true; |
431 |
116 |
if (!d_solvedf.empty()) |
432 |
|
{ |
433 |
|
// replace the final solution into the solved functions |
434 |
|
finalSol.applyToRange(d_solvedf, true); |
435 |
|
} |
436 |
116 |
} |
437 |
|
|
438 |
242 |
Node CegSingleInv::reconstructToSyntax(Node s, |
439 |
|
TypeNode stn, |
440 |
|
int8_t& reconstructed, |
441 |
|
bool rconsSygus) |
442 |
|
{ |
443 |
|
// extract the lambda body |
444 |
484 |
Node sol = s; |
445 |
242 |
const DType& dt = stn.getDType(); |
446 |
|
|
447 |
|
// reconstruct the solution into sygus if necessary |
448 |
242 |
reconstructed = 0; |
449 |
484 |
if (options().quantifiers.cegqiSingleInvReconstruct |
450 |
|
!= options::CegqiSingleInvRconsMode::NONE |
451 |
242 |
&& !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus) |
452 |
|
{ |
453 |
28 |
int64_t enumLimit = -1; |
454 |
56 |
if (options().quantifiers.cegqiSingleInvReconstruct |
455 |
28 |
== options::CegqiSingleInvRconsMode::TRY) |
456 |
|
{ |
457 |
|
enumLimit = 0; |
458 |
|
} |
459 |
56 |
else if (options().quantifiers.cegqiSingleInvReconstruct |
460 |
28 |
== options::CegqiSingleInvRconsMode::ALL_LIMIT) |
461 |
|
{ |
462 |
28 |
enumLimit = options().quantifiers.cegqiSingleInvReconstructLimit; |
463 |
|
} |
464 |
28 |
sol = d_srcons->reconstructSolution(s, stn, reconstructed, enumLimit); |
465 |
28 |
if (reconstructed == 1) |
466 |
|
{ |
467 |
56 |
Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << sol |
468 |
28 |
<< std::endl; |
469 |
|
} |
470 |
|
} |
471 |
|
else |
472 |
|
{ |
473 |
214 |
Trace("csi-sol") << "Post-process solution..." << std::endl; |
474 |
428 |
Node prev = sol; |
475 |
214 |
sol = extendedRewrite(sol); |
476 |
214 |
if (prev != sol) |
477 |
|
{ |
478 |
14 |
Trace("csi-sol") << "Solution (after post process) : " << sol |
479 |
7 |
<< std::endl; |
480 |
|
} |
481 |
|
} |
482 |
|
|
483 |
242 |
if (reconstructed == -1) |
484 |
|
{ |
485 |
|
return Node::null(); |
486 |
|
} |
487 |
242 |
return sol; |
488 |
|
} |
489 |
|
|
490 |
544 |
void CegSingleInv::preregisterConjecture(Node q) { d_orig_conjecture = q; } |
491 |
|
|
492 |
126 |
bool CegSingleInv::solveTrivial(Node q) |
493 |
|
{ |
494 |
126 |
Assert(!d_isSolved); |
495 |
126 |
Assert(d_inst.empty()); |
496 |
126 |
Assert(q.getKind() == FORALL); |
497 |
|
// If the conjecture is forall x1...xn. ~(x1 = t1 ^ ... xn = tn), it is |
498 |
|
// trivially solvable. |
499 |
252 |
std::vector<Node> args(q[0].begin(), q[0].end()); |
500 |
|
// keep solving for variables until a fixed point is reached |
501 |
252 |
std::vector<Node> vars; |
502 |
252 |
std::vector<Node> subs; |
503 |
252 |
Node body = q[1]; |
504 |
252 |
Node prev; |
505 |
448 |
while (prev != body && !args.empty()) |
506 |
|
{ |
507 |
161 |
prev = body; |
508 |
|
|
509 |
322 |
std::vector<Node> varsTmp; |
510 |
322 |
std::vector<Node> subsTmp; |
511 |
322 |
QuantifiersRewriter qrew(options()); |
512 |
161 |
qrew.getVarElim(body, args, varsTmp, subsTmp); |
513 |
|
// if we eliminated a variable, update body and reprocess |
514 |
161 |
if (!varsTmp.empty()) |
515 |
|
{ |
516 |
83 |
Assert(varsTmp.size() == subsTmp.size()); |
517 |
|
// remake with eliminated nodes |
518 |
83 |
body = body.substitute( |
519 |
|
varsTmp.begin(), varsTmp.end(), subsTmp.begin(), subsTmp.end()); |
520 |
83 |
body = rewrite(body); |
521 |
|
// apply to subs |
522 |
|
// this ensures we behave correctly if we solve x before y in |
523 |
|
// x = y+1 ^ y = 2. |
524 |
104 |
for (size_t i = 0, ssize = subs.size(); i < ssize; i++) |
525 |
|
{ |
526 |
21 |
subs[i] = subs[i].substitute( |
527 |
|
varsTmp.begin(), varsTmp.end(), subsTmp.begin(), subsTmp.end()); |
528 |
21 |
subs[i] = rewrite(subs[i]); |
529 |
|
} |
530 |
83 |
vars.insert(vars.end(), varsTmp.begin(), varsTmp.end()); |
531 |
83 |
subs.insert(subs.end(), subsTmp.begin(), subsTmp.end()); |
532 |
|
} |
533 |
|
} |
534 |
|
// if we solved all arguments |
535 |
126 |
if (args.empty() && body.isConst() && !body.getConst<bool>()) |
536 |
|
{ |
537 |
92 |
Trace("sygus-si-trivial-solve") |
538 |
46 |
<< q << " is trivially solvable by substitution " << vars << " -> " |
539 |
46 |
<< subs << std::endl; |
540 |
92 |
std::map<Node, Node> imap; |
541 |
99 |
for (size_t j = 0, vsize = vars.size(); j < vsize; j++) |
542 |
|
{ |
543 |
53 |
imap[vars[j]] = subs[j]; |
544 |
|
} |
545 |
92 |
std::vector<Node> inst; |
546 |
99 |
for (const Node& v : q[0]) |
547 |
|
{ |
548 |
53 |
Assert(imap.find(v) != imap.end()); |
549 |
53 |
inst.push_back(imap[v]); |
550 |
|
} |
551 |
46 |
d_inst.push_back(inst); |
552 |
46 |
d_instConds.push_back(NodeManager::currentNM()->mkConst(true)); |
553 |
46 |
return true; |
554 |
|
} |
555 |
160 |
Trace("sygus-si-trivial-solve") |
556 |
80 |
<< q << " is not trivially solvable." << std::endl; |
557 |
|
|
558 |
80 |
return false; |
559 |
|
} |
560 |
|
|
561 |
|
} // namespace quantifiers |
562 |
|
} // namespace theory |
563 |
31137 |
} // namespace cvc5 |