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