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