1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
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 |
|
* Implementation of techniqures for static preprocessing and analysis |
14 |
|
* of sygus conjectures. |
15 |
|
*/ |
16 |
|
#include "theory/quantifiers/sygus/sygus_process_conj.h" |
17 |
|
|
18 |
|
#include <sstream> |
19 |
|
#include <stack> |
20 |
|
|
21 |
|
#include "options/quantifiers_options.h" |
22 |
|
#include "theory/quantifiers/sygus/term_database_sygus.h" |
23 |
|
#include "theory/quantifiers/term_util.h" |
24 |
|
#include "theory/rewriter.h" |
25 |
|
|
26 |
|
using namespace cvc5::kind; |
27 |
|
using namespace std; |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
namespace theory { |
31 |
|
namespace quantifiers { |
32 |
|
|
33 |
4 |
void SynthConjectureProcessFun::init(Node f) |
34 |
|
{ |
35 |
4 |
d_synth_fun = f; |
36 |
4 |
Assert(f.getType().isFunction()); |
37 |
|
|
38 |
|
// initialize the arguments |
39 |
8 |
std::unordered_map<TypeNode, unsigned> type_to_init_deq_id; |
40 |
8 |
std::vector<TypeNode> argTypes = f.getType().getArgTypes(); |
41 |
44 |
for (unsigned j = 0; j < argTypes.size(); j++) |
42 |
|
{ |
43 |
80 |
TypeNode atn = argTypes[j]; |
44 |
80 |
std::stringstream ss; |
45 |
40 |
ss << "a" << j; |
46 |
80 |
Node k = NodeManager::currentNM()->mkBoundVar(ss.str(), atn); |
47 |
40 |
d_arg_vars.push_back(k); |
48 |
40 |
d_arg_var_num[k] = j; |
49 |
40 |
d_arg_props.push_back(SynthConjectureProcessArg()); |
50 |
|
} |
51 |
4 |
} |
52 |
|
|
53 |
9 |
bool SynthConjectureProcessFun::checkMatch( |
54 |
|
Node cn, Node n, std::unordered_map<unsigned, Node>& n_arg_map) |
55 |
|
{ |
56 |
18 |
std::vector<Node> vars; |
57 |
18 |
std::vector<Node> subs; |
58 |
99 |
for (std::unordered_map<unsigned, Node>::iterator it = n_arg_map.begin(); |
59 |
99 |
it != n_arg_map.end(); |
60 |
|
++it) |
61 |
|
{ |
62 |
90 |
Assert(it->first < d_arg_vars.size()); |
63 |
90 |
Assert( |
64 |
|
it->second.getType().isComparableTo(d_arg_vars[it->first].getType())); |
65 |
90 |
vars.push_back(d_arg_vars[it->first]); |
66 |
90 |
subs.push_back(it->second); |
67 |
|
} |
68 |
|
Node cn_subs = |
69 |
18 |
cn.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); |
70 |
9 |
cn_subs = Rewriter::rewrite(cn_subs); |
71 |
9 |
n = Rewriter::rewrite(n); |
72 |
18 |
return cn_subs == n; |
73 |
|
} |
74 |
|
|
75 |
|
bool SynthConjectureProcessFun::isArgVar(Node n, unsigned& arg_index) |
76 |
|
{ |
77 |
|
if (n.isVar()) |
78 |
|
{ |
79 |
|
std::unordered_map<Node, unsigned>::iterator ita = d_arg_var_num.find(n); |
80 |
|
if (ita != d_arg_var_num.end()) |
81 |
|
{ |
82 |
|
arg_index = ita->second; |
83 |
|
return true; |
84 |
|
} |
85 |
|
} |
86 |
|
return false; |
87 |
|
} |
88 |
|
|
89 |
10 |
Node SynthConjectureProcessFun::inferDefinition( |
90 |
|
Node n, |
91 |
|
std::unordered_map<Node, unsigned>& term_to_arg_carry, |
92 |
|
std::unordered_map<Node, std::unordered_set<Node>>& free_vars) |
93 |
|
{ |
94 |
20 |
std::unordered_map<TNode, Node> visited; |
95 |
10 |
std::unordered_map<TNode, Node>::iterator it; |
96 |
20 |
std::stack<TNode> visit; |
97 |
20 |
TNode cur; |
98 |
10 |
visit.push(n); |
99 |
8 |
do |
100 |
|
{ |
101 |
18 |
cur = visit.top(); |
102 |
18 |
visit.pop(); |
103 |
18 |
it = visited.find(cur); |
104 |
18 |
if (it == visited.end()) |
105 |
|
{ |
106 |
|
// if it is ground, we can use it |
107 |
16 |
if (free_vars[cur].empty()) |
108 |
|
{ |
109 |
3 |
visited[cur] = cur; |
110 |
|
} |
111 |
|
else |
112 |
|
{ |
113 |
|
// if it is term used by another argument, use it |
114 |
|
std::unordered_map<Node, unsigned>::iterator itt = |
115 |
13 |
term_to_arg_carry.find(cur); |
116 |
13 |
if (itt != term_to_arg_carry.end()) |
117 |
|
{ |
118 |
3 |
visited[cur] = d_arg_vars[itt->second]; |
119 |
|
} |
120 |
10 |
else if (cur.getNumChildren() > 0) |
121 |
|
{ |
122 |
|
// try constructing children |
123 |
4 |
visited[cur] = Node::null(); |
124 |
4 |
visit.push(cur); |
125 |
12 |
for (unsigned i = 0; i < cur.getNumChildren(); i++) |
126 |
|
{ |
127 |
8 |
visit.push(cur[i]); |
128 |
|
} |
129 |
|
} |
130 |
|
else |
131 |
|
{ |
132 |
6 |
return Node::null(); |
133 |
|
} |
134 |
|
} |
135 |
|
} |
136 |
2 |
else if (it->second.isNull()) |
137 |
|
{ |
138 |
4 |
Node ret = cur; |
139 |
2 |
bool childChanged = false; |
140 |
4 |
std::vector<Node> children; |
141 |
2 |
if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) |
142 |
|
{ |
143 |
|
children.push_back(cur.getOperator()); |
144 |
|
} |
145 |
6 |
for (unsigned i = 0; i < cur.getNumChildren(); i++) |
146 |
|
{ |
147 |
4 |
it = visited.find(cur[i]); |
148 |
4 |
Assert(it != visited.end()); |
149 |
4 |
Assert(!it->second.isNull()); |
150 |
4 |
childChanged = childChanged || cur[i] != it->second; |
151 |
4 |
children.push_back(it->second); |
152 |
|
} |
153 |
2 |
if (childChanged) |
154 |
|
{ |
155 |
2 |
ret = NodeManager::currentNM()->mkNode(cur.getKind(), children); |
156 |
|
} |
157 |
2 |
visited[cur] = ret; |
158 |
|
} |
159 |
12 |
} while (!visit.empty()); |
160 |
4 |
Assert(visited.find(n) != visited.end()); |
161 |
4 |
Assert(!visited.find(n)->second.isNull()); |
162 |
4 |
return visited[n]; |
163 |
|
} |
164 |
|
|
165 |
8 |
unsigned SynthConjectureProcessFun::assignRelevantDef( |
166 |
|
Node def, std::vector<unsigned>& args) |
167 |
|
{ |
168 |
8 |
unsigned id = 0; |
169 |
8 |
if (def.isNull()) |
170 |
|
{ |
171 |
|
// prefer one that already has a definition, if one exists |
172 |
12 |
for (unsigned j = 0; j < args.size(); j++) |
173 |
|
{ |
174 |
8 |
unsigned i = args[j]; |
175 |
8 |
if (!d_arg_props[i].d_template.isNull()) |
176 |
|
{ |
177 |
|
id = j; |
178 |
|
break; |
179 |
|
} |
180 |
|
} |
181 |
|
} |
182 |
8 |
unsigned rid = args[id]; |
183 |
|
// for merging previously equivalent definitions |
184 |
16 |
std::unordered_map<Node, unsigned> prev_defs; |
185 |
25 |
for (unsigned j = 0; j < args.size(); j++) |
186 |
|
{ |
187 |
17 |
unsigned i = args[j]; |
188 |
17 |
Trace("sygus-process-arg-deps") << " ...processed arg #" << i; |
189 |
17 |
if (!d_arg_props[i].d_template.isNull()) |
190 |
|
{ |
191 |
4 |
if (d_arg_props[i].d_template == def) |
192 |
|
{ |
193 |
|
// definition was consistent |
194 |
|
} |
195 |
|
else |
196 |
|
{ |
197 |
8 |
Node t = d_arg_props[i].d_template; |
198 |
4 |
std::unordered_map<Node, unsigned>::iterator itt = prev_defs.find(t); |
199 |
4 |
if (itt != prev_defs.end()) |
200 |
|
{ |
201 |
|
// merge previously equivalent definitions |
202 |
2 |
d_arg_props[i].d_template = d_arg_vars[itt->second]; |
203 |
4 |
Trace("sygus-process-arg-deps") |
204 |
2 |
<< " (merged equivalent def from argument "; |
205 |
2 |
Trace("sygus-process-arg-deps") << itt->second << ")." << std::endl; |
206 |
|
} |
207 |
|
else |
208 |
|
{ |
209 |
|
// store this as previous |
210 |
2 |
prev_defs[t] = i; |
211 |
|
// now must be relevant |
212 |
2 |
d_arg_props[i].d_relevant = true; |
213 |
4 |
Trace("sygus-process-arg-deps") |
214 |
2 |
<< " (marked relevant, overwrite definition)." << std::endl; |
215 |
|
} |
216 |
|
} |
217 |
|
} |
218 |
|
else |
219 |
|
{ |
220 |
13 |
if (def.isNull()) |
221 |
|
{ |
222 |
8 |
if (i != rid) |
223 |
|
{ |
224 |
|
// marked as relevant, but template can be set equal to master |
225 |
4 |
d_arg_props[i].d_template = d_arg_vars[rid]; |
226 |
8 |
Trace("sygus-process-arg-deps") << " (new definition, map to master " |
227 |
4 |
<< d_arg_vars[rid] << ")." |
228 |
4 |
<< std::endl; |
229 |
|
} |
230 |
|
else |
231 |
|
{ |
232 |
4 |
d_arg_props[i].d_relevant = true; |
233 |
4 |
Trace("sygus-process-arg-deps") << " (marked relevant)." << std::endl; |
234 |
|
} |
235 |
|
} |
236 |
|
else |
237 |
|
{ |
238 |
|
// has new definition |
239 |
5 |
d_arg_props[i].d_template = def; |
240 |
10 |
Trace("sygus-process-arg-deps") << " (new definition " << def << ")." |
241 |
5 |
<< std::endl; |
242 |
|
} |
243 |
|
} |
244 |
|
} |
245 |
16 |
return rid; |
246 |
|
} |
247 |
|
|
248 |
5 |
void SynthConjectureProcessFun::processTerms( |
249 |
|
std::vector<Node>& ns, |
250 |
|
std::vector<Node>& ks, |
251 |
|
Node nf, |
252 |
|
std::unordered_set<Node>& synth_fv, |
253 |
|
std::unordered_map<Node, std::unordered_set<Node>>& free_vars) |
254 |
|
{ |
255 |
5 |
Assert(ns.size() == ks.size()); |
256 |
10 |
Trace("sygus-process-arg-deps") << "Process " << ns.size() |
257 |
5 |
<< " applications of " << d_synth_fun << "..." |
258 |
5 |
<< std::endl; |
259 |
|
|
260 |
|
// get the relevant variables |
261 |
|
// relevant variables are those that appear in the body of the conjunction |
262 |
10 |
std::unordered_set<Node> rlv_vars; |
263 |
5 |
Assert(free_vars.find(nf) != free_vars.end()); |
264 |
5 |
rlv_vars = free_vars[nf]; |
265 |
|
|
266 |
|
// get the single occurrence variables |
267 |
|
// single occurrence variables are those that appear in only one position, |
268 |
|
// as an argument to the function-to-synthesize. |
269 |
10 |
std::unordered_map<Node, bool> single_occ_variables; |
270 |
10 |
for (unsigned index = 0; index < ns.size(); index++) |
271 |
|
{ |
272 |
10 |
Node n = ns[index]; |
273 |
55 |
for (unsigned i = 0; i < n.getNumChildren(); i++) |
274 |
|
{ |
275 |
100 |
Node nn = n[i]; |
276 |
50 |
if (nn.isVar()) |
277 |
|
{ |
278 |
|
std::unordered_map<Node, bool>::iterator its = |
279 |
44 |
single_occ_variables.find(nn); |
280 |
44 |
if (its == single_occ_variables.end()) |
281 |
|
{ |
282 |
|
// only irrelevant variables |
283 |
31 |
single_occ_variables[nn] = rlv_vars.find(nn) == rlv_vars.end(); |
284 |
|
} |
285 |
|
else |
286 |
|
{ |
287 |
13 |
single_occ_variables[nn] = false; |
288 |
|
} |
289 |
|
} |
290 |
|
else |
291 |
|
{ |
292 |
|
std::unordered_map<Node, std::unordered_set<Node>>::iterator itf = |
293 |
6 |
free_vars.find(nn); |
294 |
6 |
Assert(itf != free_vars.end()); |
295 |
10 |
for (std::unordered_set<Node>::iterator itfv = itf->second.begin(); |
296 |
10 |
itfv != itf->second.end(); |
297 |
|
++itfv) |
298 |
|
{ |
299 |
4 |
single_occ_variables[*itfv] = false; |
300 |
|
} |
301 |
|
} |
302 |
|
} |
303 |
|
} |
304 |
|
|
305 |
|
// update constant argument information |
306 |
10 |
for (unsigned index = 0; index < ns.size(); index++) |
307 |
|
{ |
308 |
10 |
Node n = ns[index]; |
309 |
10 |
Trace("sygus-process-arg-deps") |
310 |
5 |
<< " Analyze argument information for application #" << index << ": " |
311 |
5 |
<< n << std::endl; |
312 |
|
|
313 |
|
// in the following, we say an argument a "carries" a term t if |
314 |
|
// the function to synthesize would use argument a to construct |
315 |
|
// the term t in its definition. |
316 |
|
|
317 |
|
// map that assumes all arguments carry their respective term |
318 |
10 |
std::unordered_map<unsigned, Node> n_arg_map; |
319 |
|
// terms to the argument that is carrying it. |
320 |
|
// the arguments in the range of this map must be marked as relevant. |
321 |
10 |
std::unordered_map<Node, unsigned> term_to_arg_carry; |
322 |
|
// map of terms to (unprocessed) arguments where it occurs |
323 |
10 |
std::unordered_map<Node, std::vector<unsigned>> term_to_args; |
324 |
|
|
325 |
|
// initialize |
326 |
55 |
for (unsigned a = 0; a < n.getNumChildren(); a++) |
327 |
|
{ |
328 |
50 |
n_arg_map[a] = n[a]; |
329 |
|
} |
330 |
|
|
331 |
55 |
for (unsigned a = 0; a < n.getNumChildren(); a++) |
332 |
|
{ |
333 |
50 |
bool processed = false; |
334 |
50 |
if (d_arg_props[a].d_relevant) |
335 |
|
{ |
336 |
|
// we can assume all relevant arguments carry their terms |
337 |
1 |
processed = true; |
338 |
2 |
Trace("sygus-process-arg-deps") << " ...processed arg #" << a |
339 |
1 |
<< " (already relevant)." << std::endl; |
340 |
1 |
if (term_to_arg_carry.find(n[a]) == term_to_arg_carry.end()) |
341 |
|
{ |
342 |
2 |
Trace("sygus-process-arg-deps") << " carry " << n[a] |
343 |
1 |
<< " by argument #" << a << std::endl; |
344 |
1 |
term_to_arg_carry[n[a]] = a; |
345 |
|
} |
346 |
|
} |
347 |
|
else |
348 |
|
{ |
349 |
|
// first, check if single occurrence variable |
350 |
|
// check if an irrelevant variable |
351 |
49 |
if (n[a].isVar() && synth_fv.find(n[a]) != synth_fv.end()) |
352 |
|
{ |
353 |
43 |
Assert(single_occ_variables.find(n[a]) != single_occ_variables.end()); |
354 |
|
// may be able to make this more precise? |
355 |
|
// check if a single-occurrence variable |
356 |
43 |
if (single_occ_variables[n[a]]) |
357 |
|
{ |
358 |
|
// if we do not already have a template definition, or the |
359 |
|
// template is a single occurrence variable |
360 |
54 |
if (d_arg_props[a].d_template.isNull() |
361 |
27 |
|| d_arg_props[a].d_var_single_occ) |
362 |
|
{ |
363 |
27 |
processed = true; |
364 |
27 |
Trace("sygus-process-arg-deps") << " ...processed arg #" << a; |
365 |
54 |
Trace("sygus-process-arg-deps") |
366 |
27 |
<< " (single occurrence variable "; |
367 |
27 |
Trace("sygus-process-arg-deps") << n[a] << ")." << std::endl; |
368 |
27 |
d_arg_props[a].d_var_single_occ = true; |
369 |
27 |
d_arg_props[a].d_template = n[a]; |
370 |
|
} |
371 |
|
} |
372 |
|
} |
373 |
120 |
if (!processed && !d_arg_props[a].d_template.isNull() |
374 |
58 |
&& !d_arg_props[a].d_var_single_occ) |
375 |
|
{ |
376 |
|
// argument already has a definition, see if it is maintained |
377 |
9 |
if (checkMatch(d_arg_props[a].d_template, n[a], n_arg_map)) |
378 |
|
{ |
379 |
5 |
processed = true; |
380 |
5 |
Trace("sygus-process-arg-deps") << " ...processed arg #" << a; |
381 |
10 |
Trace("sygus-process-arg-deps") << " (consistent definition " |
382 |
5 |
<< n[a]; |
383 |
10 |
Trace("sygus-process-arg-deps") |
384 |
5 |
<< " with " << d_arg_props[a].d_template << ")." << std::endl; |
385 |
|
} |
386 |
|
} |
387 |
|
} |
388 |
50 |
if (!processed) |
389 |
|
{ |
390 |
|
// otherwise, add it to the list of arguments for this term |
391 |
17 |
term_to_args[n[a]].push_back(a); |
392 |
|
} |
393 |
|
} |
394 |
|
|
395 |
10 |
Trace("sygus-process-arg-deps") << " Look at argument terms..." |
396 |
5 |
<< std::endl; |
397 |
|
|
398 |
|
// list of all arguments |
399 |
10 |
std::vector<Node> arg_list; |
400 |
|
// now look at the terms for unprocessed arguments |
401 |
8 |
for (std::unordered_map<Node, std::vector<unsigned>>::iterator it = |
402 |
5 |
term_to_args.begin(); |
403 |
13 |
it != term_to_args.end(); |
404 |
|
++it) |
405 |
|
{ |
406 |
16 |
Node nn = it->first; |
407 |
8 |
arg_list.push_back(nn); |
408 |
8 |
if (Trace.isOn("sygus-process-arg-deps")) |
409 |
|
{ |
410 |
|
Trace("sygus-process-arg-deps") << " argument " << nn; |
411 |
|
Trace("sygus-process-arg-deps") << " (" << it->second.size() |
412 |
|
<< " positions)"; |
413 |
|
// check the status of this term |
414 |
|
if (nn.isVar() && synth_fv.find(nn) != synth_fv.end()) |
415 |
|
{ |
416 |
|
// is it relevant? |
417 |
|
if (rlv_vars.find(nn) != rlv_vars.end()) |
418 |
|
{ |
419 |
|
Trace("sygus-process-arg-deps") << " is a relevant variable." |
420 |
|
<< std::endl; |
421 |
|
} |
422 |
|
else |
423 |
|
{ |
424 |
|
Trace("sygus-process-arg-deps") << " is an irrelevant variable." |
425 |
|
<< std::endl; |
426 |
|
} |
427 |
|
} |
428 |
|
else |
429 |
|
{ |
430 |
|
// this can be more precise |
431 |
|
Trace("sygus-process-arg-deps") << " is a relevant term." |
432 |
|
<< std::endl; |
433 |
|
} |
434 |
|
} |
435 |
|
} |
436 |
|
|
437 |
5 |
unsigned arg_list_counter = 0; |
438 |
|
// sort arg_list by term size? |
439 |
|
|
440 |
17 |
while (arg_list_counter < arg_list.size()) |
441 |
|
{ |
442 |
12 |
Node infer_def_t; |
443 |
4 |
do |
444 |
|
{ |
445 |
10 |
infer_def_t = Node::null(); |
446 |
|
// see if we can infer a definition |
447 |
6 |
for (std::unordered_map<Node, std::vector<unsigned>>::iterator it = |
448 |
10 |
term_to_args.begin(); |
449 |
16 |
it != term_to_args.end(); |
450 |
|
++it) |
451 |
|
{ |
452 |
16 |
Node def = inferDefinition(it->first, term_to_arg_carry, free_vars); |
453 |
10 |
if (!def.isNull()) |
454 |
|
{ |
455 |
8 |
Trace("sygus-process-arg-deps") << " *** Inferred definition " |
456 |
4 |
<< def << " for " << it->first |
457 |
4 |
<< std::endl; |
458 |
|
// assign to each argument |
459 |
4 |
assignRelevantDef(def, it->second); |
460 |
|
// term_to_arg_carry[it->first] = rid; |
461 |
4 |
infer_def_t = it->first; |
462 |
4 |
break; |
463 |
|
} |
464 |
|
} |
465 |
10 |
if (!infer_def_t.isNull()) |
466 |
|
{ |
467 |
4 |
term_to_args.erase(infer_def_t); |
468 |
|
} |
469 |
10 |
} while (!infer_def_t.isNull()); |
470 |
|
|
471 |
|
// decide to make an argument relevant |
472 |
6 |
bool success = false; |
473 |
22 |
while (arg_list_counter < arg_list.size() && !success) |
474 |
|
{ |
475 |
16 |
Node curr = arg_list[arg_list_counter]; |
476 |
|
std::unordered_map<Node, std::vector<unsigned>>::iterator it = |
477 |
8 |
term_to_args.find(curr); |
478 |
8 |
if (it != term_to_args.end()) |
479 |
|
{ |
480 |
8 |
Trace("sygus-process-arg-deps") << " *** Decide relevant " << curr |
481 |
4 |
<< std::endl; |
482 |
|
// assign relevant to each |
483 |
8 |
Node null_def; |
484 |
4 |
unsigned rid = assignRelevantDef(null_def, it->second); |
485 |
4 |
term_to_arg_carry[curr] = rid; |
486 |
8 |
Trace("sygus-process-arg-deps") |
487 |
4 |
<< " carry " << curr << " by argument #" << rid << std::endl; |
488 |
4 |
term_to_args.erase(curr); |
489 |
4 |
success = true; |
490 |
|
} |
491 |
8 |
arg_list_counter++; |
492 |
|
} |
493 |
|
} |
494 |
|
} |
495 |
5 |
} |
496 |
|
|
497 |
|
bool SynthConjectureProcessFun::isArgRelevant(unsigned i) |
498 |
|
{ |
499 |
|
return d_arg_props[i].d_relevant; |
500 |
|
} |
501 |
|
|
502 |
4 |
void SynthConjectureProcessFun::getIrrelevantArgs( |
503 |
|
std::unordered_set<unsigned>& args) |
504 |
|
{ |
505 |
44 |
for (unsigned i = 0; i < d_arg_vars.size(); i++) |
506 |
|
{ |
507 |
40 |
if (!d_arg_props[i].d_relevant) |
508 |
|
{ |
509 |
34 |
args.insert(i); |
510 |
|
} |
511 |
|
} |
512 |
4 |
} |
513 |
|
|
514 |
1529 |
SynthConjectureProcess::SynthConjectureProcess() {} |
515 |
1529 |
SynthConjectureProcess::~SynthConjectureProcess() {} |
516 |
325 |
Node SynthConjectureProcess::preSimplify(Node q) |
517 |
|
{ |
518 |
325 |
Trace("sygus-process") << "Pre-simplify conjecture : " << q << std::endl; |
519 |
325 |
return q; |
520 |
|
} |
521 |
|
|
522 |
325 |
Node SynthConjectureProcess::postSimplify(Node q) |
523 |
|
{ |
524 |
325 |
Trace("sygus-process") << "Post-simplify conjecture : " << q << std::endl; |
525 |
325 |
Assert(q.getKind() == FORALL); |
526 |
|
|
527 |
653 |
if (options::sygusArgRelevant()) |
528 |
|
{ |
529 |
|
// initialize the information about each function to synthesize |
530 |
7 |
for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++) |
531 |
|
{ |
532 |
8 |
Node f = q[0][i]; |
533 |
4 |
if (f.getType().isFunction()) |
534 |
|
{ |
535 |
4 |
d_sf_info[f].init(f); |
536 |
|
} |
537 |
|
} |
538 |
|
|
539 |
|
// get the base on the conjecture |
540 |
6 |
Node base = q[1]; |
541 |
6 |
std::unordered_set<Node> synth_fv; |
542 |
3 |
if (base.getKind() == NOT && base[0].getKind() == FORALL) |
543 |
|
{ |
544 |
24 |
for (unsigned j = 0, size = base[0][0].getNumChildren(); j < size; j++) |
545 |
|
{ |
546 |
21 |
synth_fv.insert(base[0][0][j]); |
547 |
|
} |
548 |
3 |
base = base[0][1]; |
549 |
|
} |
550 |
6 |
std::vector<Node> conjuncts; |
551 |
3 |
getComponentVector(AND, base, conjuncts); |
552 |
|
|
553 |
|
// process the conjunctions |
554 |
4 |
for (std::map<Node, SynthConjectureProcessFun>::iterator it = |
555 |
3 |
d_sf_info.begin(); |
556 |
7 |
it != d_sf_info.end(); |
557 |
|
++it) |
558 |
|
{ |
559 |
8 |
Node f = it->first; |
560 |
11 |
for (const Node& conj : conjuncts) |
561 |
|
{ |
562 |
7 |
processConjunct(conj, f, synth_fv); |
563 |
|
} |
564 |
|
} |
565 |
|
} |
566 |
|
|
567 |
325 |
return q; |
568 |
|
} |
569 |
|
|
570 |
233 |
void SynthConjectureProcess::initialize(Node n, std::vector<Node>& candidates) |
571 |
|
{ |
572 |
233 |
if (Trace.isOn("sygus-process")) |
573 |
|
{ |
574 |
|
Trace("sygus-process") << "Process conjecture : " << n |
575 |
|
<< " with candidates: " << std::endl; |
576 |
|
for (unsigned i = 0; i < candidates.size(); i++) |
577 |
|
{ |
578 |
|
Trace("sygus-process") << " " << candidates[i] << std::endl; |
579 |
|
} |
580 |
|
} |
581 |
233 |
} |
582 |
|
|
583 |
|
bool SynthConjectureProcess::isArgRelevant(Node f, unsigned i) |
584 |
|
{ |
585 |
|
if (!options::sygusArgRelevant()) |
586 |
|
{ |
587 |
|
return true; |
588 |
|
} |
589 |
|
std::map<Node, SynthConjectureProcessFun>::iterator its = d_sf_info.find(f); |
590 |
|
if (its != d_sf_info.end()) |
591 |
|
{ |
592 |
|
return its->second.isArgRelevant(i); |
593 |
|
} |
594 |
|
Assert(false); |
595 |
|
return true; |
596 |
|
} |
597 |
|
|
598 |
297 |
bool SynthConjectureProcess::getIrrelevantArgs( |
599 |
|
Node f, std::unordered_set<unsigned>& args) |
600 |
|
{ |
601 |
297 |
std::map<Node, SynthConjectureProcessFun>::iterator its = d_sf_info.find(f); |
602 |
297 |
if (its != d_sf_info.end()) |
603 |
|
{ |
604 |
4 |
its->second.getIrrelevantArgs(args); |
605 |
4 |
return true; |
606 |
|
} |
607 |
293 |
return false; |
608 |
|
} |
609 |
|
|
610 |
7 |
void SynthConjectureProcess::processConjunct(Node n, |
611 |
|
Node f, |
612 |
|
std::unordered_set<Node>& synth_fv) |
613 |
|
{ |
614 |
7 |
Trace("sygus-process-arg-deps") << "Process conjunct: " << std::endl; |
615 |
14 |
Trace("sygus-process-arg-deps") << " " << n << " for synth fun " << f |
616 |
7 |
<< "..." << std::endl; |
617 |
|
|
618 |
|
// first, flatten the conjunct |
619 |
|
// make a copy of free variables since we may add new ones |
620 |
14 |
std::unordered_set<Node> synth_fv_n = synth_fv; |
621 |
14 |
std::unordered_map<Node, Node> defs; |
622 |
14 |
Node nf = flatten(n, f, synth_fv_n, defs); |
623 |
|
|
624 |
7 |
Trace("sygus-process-arg-deps") << "Flattened to: " << std::endl; |
625 |
7 |
Trace("sygus-process-arg-deps") << " " << nf << std::endl; |
626 |
|
|
627 |
|
// get free variables in nf |
628 |
14 |
std::unordered_map<Node, std::unordered_set<Node>> free_vars; |
629 |
7 |
getFreeVariables(nf, synth_fv_n, free_vars); |
630 |
|
// get free variables in each application |
631 |
14 |
std::vector<Node> ns; |
632 |
14 |
std::vector<Node> ks; |
633 |
12 |
for (std::unordered_map<Node, Node>::iterator it = defs.begin(); |
634 |
12 |
it != defs.end(); |
635 |
|
++it) |
636 |
|
{ |
637 |
5 |
getFreeVariables(it->second, synth_fv_n, free_vars); |
638 |
5 |
ns.push_back(it->second); |
639 |
5 |
ks.push_back(it->first); |
640 |
|
} |
641 |
|
|
642 |
|
// process the applications of synthesis functions |
643 |
7 |
if (!ns.empty()) |
644 |
|
{ |
645 |
5 |
std::map<Node, SynthConjectureProcessFun>::iterator its = d_sf_info.find(f); |
646 |
5 |
if (its != d_sf_info.end()) |
647 |
|
{ |
648 |
5 |
its->second.processTerms(ns, ks, nf, synth_fv_n, free_vars); |
649 |
|
} |
650 |
|
} |
651 |
7 |
} |
652 |
|
|
653 |
7 |
Node SynthConjectureProcess::SynthConjectureProcess::flatten( |
654 |
|
Node n, |
655 |
|
Node f, |
656 |
|
std::unordered_set<Node>& synth_fv, |
657 |
|
std::unordered_map<Node, Node>& defs) |
658 |
|
{ |
659 |
14 |
std::unordered_map<Node, Node> visited; |
660 |
7 |
std::unordered_map<Node, Node>::iterator it; |
661 |
14 |
std::stack<Node> visit; |
662 |
14 |
Node cur; |
663 |
7 |
visit.push(n); |
664 |
254 |
do |
665 |
|
{ |
666 |
261 |
cur = visit.top(); |
667 |
261 |
visit.pop(); |
668 |
261 |
it = visited.find(cur); |
669 |
|
|
670 |
261 |
if (it == visited.end()) |
671 |
|
{ |
672 |
118 |
visited[cur] = Node::null(); |
673 |
118 |
visit.push(cur); |
674 |
254 |
for (unsigned i = 0; i < cur.getNumChildren(); i++) |
675 |
|
{ |
676 |
136 |
visit.push(cur[i]); |
677 |
|
} |
678 |
|
} |
679 |
143 |
else if (it->second.isNull()) |
680 |
|
{ |
681 |
236 |
Node ret = cur; |
682 |
118 |
bool childChanged = false; |
683 |
236 |
std::vector<Node> children; |
684 |
118 |
if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) |
685 |
|
{ |
686 |
7 |
children.push_back(cur.getOperator()); |
687 |
|
} |
688 |
254 |
for (unsigned i = 0; i < cur.getNumChildren(); i++) |
689 |
|
{ |
690 |
136 |
it = visited.find(cur[i]); |
691 |
136 |
Assert(it != visited.end()); |
692 |
136 |
Assert(!it->second.isNull()); |
693 |
136 |
childChanged = childChanged || cur[i] != it->second; |
694 |
136 |
children.push_back(it->second); |
695 |
|
} |
696 |
118 |
if (childChanged) |
697 |
|
{ |
698 |
19 |
ret = NodeManager::currentNM()->mkNode(cur.getKind(), children); |
699 |
|
} |
700 |
|
// is it the function to synthesize? |
701 |
118 |
if (cur.getKind() == APPLY_UF && cur.getOperator() == f) |
702 |
|
{ |
703 |
|
// if so, flatten |
704 |
10 |
Node k = NodeManager::currentNM()->mkBoundVar("vf", cur.getType()); |
705 |
5 |
defs[k] = ret; |
706 |
5 |
ret = k; |
707 |
5 |
synth_fv.insert(k); |
708 |
|
} |
709 |
|
// post-rewrite |
710 |
118 |
visited[cur] = ret; |
711 |
|
} |
712 |
261 |
} while (!visit.empty()); |
713 |
7 |
Assert(visited.find(n) != visited.end()); |
714 |
7 |
Assert(!visited.find(n)->second.isNull()); |
715 |
14 |
return visited[n]; |
716 |
|
} |
717 |
|
|
718 |
12 |
void SynthConjectureProcess::getFreeVariables( |
719 |
|
Node n, |
720 |
|
std::unordered_set<Node>& synth_fv, |
721 |
|
std::unordered_map<Node, std::unordered_set<Node>>& free_vars) |
722 |
|
{ |
723 |
|
// first must compute free variables in each subterm of n, |
724 |
|
// as well as contains_synth_fun |
725 |
24 |
std::unordered_map<Node, bool> visited; |
726 |
12 |
std::unordered_map<Node, bool>::iterator it; |
727 |
24 |
std::stack<Node> visit; |
728 |
24 |
Node cur; |
729 |
12 |
visit.push(n); |
730 |
266 |
do |
731 |
|
{ |
732 |
278 |
cur = visit.top(); |
733 |
278 |
visit.pop(); |
734 |
278 |
it = visited.find(cur); |
735 |
|
|
736 |
278 |
if (it == visited.end()) |
737 |
|
{ |
738 |
130 |
visited[cur] = false; |
739 |
130 |
visit.push(cur); |
740 |
266 |
for (unsigned i = 0; i < cur.getNumChildren(); i++) |
741 |
|
{ |
742 |
136 |
visit.push(cur[i]); |
743 |
|
} |
744 |
|
} |
745 |
148 |
else if (!it->second) |
746 |
|
{ |
747 |
130 |
free_vars[cur].clear(); |
748 |
130 |
if (synth_fv.find(cur) != synth_fv.end()) |
749 |
|
{ |
750 |
|
// it is a free variable |
751 |
62 |
free_vars[cur].insert(cur); |
752 |
|
} |
753 |
|
else |
754 |
|
{ |
755 |
|
// otherwise, carry the free variables from the children |
756 |
204 |
for (unsigned i = 0; i < cur.getNumChildren(); i++) |
757 |
|
{ |
758 |
272 |
free_vars[cur].insert(free_vars[cur[i]].begin(), |
759 |
272 |
free_vars[cur[i]].end()); |
760 |
|
} |
761 |
|
} |
762 |
130 |
visited[cur] = true; |
763 |
|
} |
764 |
278 |
} while (!visit.empty()); |
765 |
12 |
} |
766 |
|
|
767 |
8474 |
Node SynthConjectureProcess::getSymmetryBreakingPredicate( |
768 |
|
Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth) |
769 |
|
{ |
770 |
8474 |
return Node::null(); |
771 |
|
} |
772 |
|
|
773 |
|
void SynthConjectureProcess::debugPrint(const char* c) {} |
774 |
3 |
void SynthConjectureProcess::getComponentVector(Kind k, |
775 |
|
Node n, |
776 |
|
std::vector<Node>& args) |
777 |
|
{ |
778 |
3 |
if (n.getKind() == k) |
779 |
|
{ |
780 |
6 |
for (unsigned i = 0; i < n.getNumChildren(); i++) |
781 |
|
{ |
782 |
4 |
args.push_back(n[i]); |
783 |
|
} |
784 |
|
} |
785 |
|
else |
786 |
|
{ |
787 |
1 |
args.push_back(n); |
788 |
|
} |
789 |
3 |
} |
790 |
|
|
791 |
|
} // namespace quantifiers |
792 |
|
} // namespace theory |
793 |
28522 |
} // namespace cvc5 |