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