1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Haniel Barbosa, 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 |
|
* Implementation of class for cegis with unification techniques. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/sygus/cegis_unif.h" |
17 |
|
|
18 |
|
#include "expr/skolem_manager.h" |
19 |
|
#include "expr/sygus_datatype.h" |
20 |
|
#include "options/quantifiers_options.h" |
21 |
|
#include "printer/printer.h" |
22 |
|
#include "theory/datatypes/sygus_datatype_utils.h" |
23 |
|
#include "theory/quantifiers/sygus/sygus_unif_rl.h" |
24 |
|
#include "theory/quantifiers/sygus/synth_conjecture.h" |
25 |
|
#include "theory/quantifiers/sygus/term_database_sygus.h" |
26 |
|
#include "util/rational.h" |
27 |
|
|
28 |
|
using namespace cvc5::kind; |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
namespace theory { |
32 |
|
namespace quantifiers { |
33 |
|
|
34 |
1193 |
CegisUnif::CegisUnif(Env& env, |
35 |
|
QuantifiersState& qs, |
36 |
|
QuantifiersInferenceManager& qim, |
37 |
|
TermDbSygus* tds, |
38 |
1193 |
SynthConjecture* p) |
39 |
|
: Cegis(env, qs, qim, tds, p), |
40 |
|
d_sygus_unif(env, p), |
41 |
1193 |
d_u_enum_manager(env, qs, qim, tds, p) |
42 |
|
{ |
43 |
1193 |
} |
44 |
|
|
45 |
2382 |
CegisUnif::~CegisUnif() {} |
46 |
11 |
bool CegisUnif::processInitialize(Node conj, |
47 |
|
Node n, |
48 |
|
const std::vector<Node>& candidates) |
49 |
|
{ |
50 |
|
// list of strategy points for unification candidates |
51 |
22 |
std::vector<Node> unif_candidate_pts; |
52 |
|
// map from strategy points to their conditions |
53 |
22 |
std::map<Node, Node> pt_to_cond; |
54 |
|
// strategy lemmas for each strategy point |
55 |
22 |
std::map<Node, std::vector<Node>> strategy_lemmas; |
56 |
|
// Initialize strategies for all functions-to-synthesize |
57 |
|
// The role of non-unification enumerators is to be either the single solution |
58 |
|
// or part of a solution involving multiple enumerators. |
59 |
11 |
EnumeratorRole eroleNonUnif = candidates.size() == 1 |
60 |
11 |
? ROLE_ENUM_SINGLE_SOLUTION |
61 |
11 |
: ROLE_ENUM_MULTI_SOLUTION; |
62 |
25 |
for (const Node& f : candidates) |
63 |
|
{ |
64 |
|
// Init UNIF util for this candidate |
65 |
28 |
d_sygus_unif.initializeCandidate( |
66 |
14 |
d_tds, f, d_cand_to_strat_pt[f], strategy_lemmas); |
67 |
14 |
if (!d_sygus_unif.usingUnif(f)) |
68 |
|
{ |
69 |
3 |
Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl; |
70 |
3 |
d_tds->registerEnumerator(f, f, d_parent, eroleNonUnif); |
71 |
3 |
d_non_unif_candidates.push_back(f); |
72 |
|
} |
73 |
|
else |
74 |
|
{ |
75 |
11 |
d_unif_candidates.push_back(f); |
76 |
22 |
Trace("cegis-unif") << "* unification candidate : " << f |
77 |
11 |
<< " with strategy points:" << std::endl; |
78 |
11 |
std::vector<Node>& enums = d_cand_to_strat_pt[f]; |
79 |
11 |
unif_candidate_pts.insert( |
80 |
22 |
unif_candidate_pts.end(), enums.begin(), enums.end()); |
81 |
|
// map strategy point to its condition in pt_to_cond |
82 |
22 |
for (const Node& e : enums) |
83 |
|
{ |
84 |
22 |
Node cond = d_sygus_unif.getConditionForEvaluationPoint(e); |
85 |
11 |
Assert(!cond.isNull()); |
86 |
22 |
Trace("cegis-unif") |
87 |
11 |
<< " " << e << " with condition : " << cond << std::endl; |
88 |
11 |
pt_to_cond[e] = cond; |
89 |
|
} |
90 |
|
} |
91 |
|
} |
92 |
|
// initialize the enumeration manager |
93 |
11 |
d_u_enum_manager.initialize(unif_candidate_pts, pt_to_cond, strategy_lemmas); |
94 |
22 |
return true; |
95 |
|
} |
96 |
|
|
97 |
323 |
void CegisUnif::getTermList(const std::vector<Node>& candidates, |
98 |
|
std::vector<Node>& enums) |
99 |
|
{ |
100 |
|
// Non-unif candidate are themselves the enumerators |
101 |
323 |
enums.insert( |
102 |
646 |
enums.end(), d_non_unif_candidates.begin(), d_non_unif_candidates.end()); |
103 |
646 |
for (const Node& c : d_unif_candidates) |
104 |
|
{ |
105 |
|
// Collect heads of candidates |
106 |
1789 |
for (const Node& hd : d_sygus_unif.getEvalPointHeads(c)) |
107 |
|
{ |
108 |
2932 |
Trace("cegis-unif-enum-debug") |
109 |
1466 |
<< "......cand " << c << " with enum hd " << hd << "\n"; |
110 |
1466 |
enums.push_back(hd); |
111 |
|
} |
112 |
|
// get unification enumerators |
113 |
646 |
for (const Node& e : d_cand_to_strat_pt[c]) |
114 |
|
{ |
115 |
969 |
for (unsigned index = 0; index < 2; index++) |
116 |
|
{ |
117 |
1292 |
std::vector<Node> uenums; |
118 |
|
// get the current unification enumerators |
119 |
646 |
d_u_enum_manager.getEnumeratorsForStrategyPt(e, uenums, index); |
120 |
|
// get the model value of each enumerator |
121 |
646 |
enums.insert(enums.end(), uenums.begin(), uenums.end()); |
122 |
|
} |
123 |
|
} |
124 |
|
} |
125 |
323 |
} |
126 |
|
|
127 |
280 |
bool CegisUnif::getEnumValues(const std::vector<Node>& enums, |
128 |
|
const std::vector<Node>& enum_values, |
129 |
|
std::map<Node, std::vector<Node>>& unif_cenums, |
130 |
|
std::map<Node, std::vector<Node>>& unif_cvalues) |
131 |
|
{ |
132 |
280 |
NodeManager* nm = NodeManager::currentNM(); |
133 |
560 |
Node cost_lit = d_u_enum_manager.getAssertedLiteral(); |
134 |
560 |
std::map<Node, std::vector<Node>> unif_renums, unif_rvalues; |
135 |
|
// build model value map |
136 |
560 |
std::map<Node, Node> mvMap; |
137 |
2537 |
for (unsigned i = 0, size = enums.size(); i < size; i++) |
138 |
|
{ |
139 |
2257 |
mvMap[enums[i]] = enum_values[i]; |
140 |
|
} |
141 |
280 |
bool addedUnifEnumSymBreakLemma = false; |
142 |
|
// populate maps between unification enumerators and their model values |
143 |
560 |
for (const Node& c : d_unif_candidates) |
144 |
|
{ |
145 |
|
// for each decision tree strategy allocated for c (these are referenced |
146 |
|
// by strategy points in d_cand_to_strat_pt[c]) |
147 |
560 |
for (const Node& e : d_cand_to_strat_pt[c]) |
148 |
|
{ |
149 |
840 |
for (unsigned index = 0; index < 2; index++) |
150 |
|
{ |
151 |
1120 |
std::vector<Node> es, vs; |
152 |
1120 |
Trace("cegis-unif") |
153 |
1120 |
<< " " << (index == 0 ? "Return values" : "Conditions") << " for " |
154 |
560 |
<< e << ":\n"; |
155 |
|
// get the current unification enumerators |
156 |
560 |
d_u_enum_manager.getEnumeratorsForStrategyPt(e, es, index); |
157 |
|
// set enums for condition enumerators |
158 |
560 |
if (index == 1) |
159 |
|
{ |
160 |
280 |
if (usingConditionPool()) |
161 |
|
{ |
162 |
|
Assert(es.size() == 1); |
163 |
|
// whether valueus exhausted |
164 |
|
if (mvMap.find(es[0]) == mvMap.end()) |
165 |
|
{ |
166 |
|
Trace("cegis-unif") << " " << es[0] << " -> N/A\n"; |
167 |
|
es.clear(); |
168 |
|
} |
169 |
|
} |
170 |
280 |
unif_cenums[e] = es; |
171 |
|
} |
172 |
|
// get the model value of each enumerator |
173 |
1510 |
for (const Node& eu : es) |
174 |
|
{ |
175 |
950 |
Assert(mvMap.find(eu) != mvMap.end()); |
176 |
1900 |
Node m_eu = mvMap[eu]; |
177 |
950 |
if (Trace.isOn("cegis-unif")) |
178 |
|
{ |
179 |
|
Trace("cegis-unif") << " " << eu << " -> "; |
180 |
|
TermDbSygus::toStreamSygus("cegis-unif", m_eu); |
181 |
|
Trace("cegis-unif") << "\n"; |
182 |
|
} |
183 |
950 |
vs.push_back(m_eu); |
184 |
|
} |
185 |
|
// set values for condition enumerators of e |
186 |
560 |
if (index == 1) |
187 |
|
{ |
188 |
280 |
unif_cvalues[e] = vs; |
189 |
|
} |
190 |
|
// inter-enumerator symmetry breaking for return values |
191 |
|
else |
192 |
|
{ |
193 |
|
// given a pool of unification enumerators eu_1, ..., eu_n, |
194 |
|
// CegisUnifEnumDecisionStrategy insists that size(eu_1) <= ... <= |
195 |
|
// size(eu_n). We additionally insist that M(eu_i) < M(eu_{i+1}) when |
196 |
|
// size(eu_i) = size(eu_{i+1}), where < is pointer comparison. |
197 |
|
// We enforce this below by adding symmetry breaking lemmas of the |
198 |
|
// form ~( eu_i = M(eu_i) ^ eu_{i+1} = M(eu_{i+1} ) ) |
199 |
|
// when applicable. |
200 |
|
// we only do this for return value enumerators, since condition |
201 |
|
// enumerators cannot be ordered (their order is based on the |
202 |
|
// seperation resolution scheme during model construction). |
203 |
594 |
for (unsigned j = 1, nenum = vs.size(); j < nenum; j++) |
204 |
|
{ |
205 |
646 |
Node prev_val = vs[j - 1]; |
206 |
646 |
Node curr_val = vs[j]; |
207 |
|
// compare the node values |
208 |
332 |
if (curr_val < prev_val) |
209 |
|
{ |
210 |
|
// must have the same size |
211 |
18 |
unsigned prev_size = datatypes::utils::getSygusTermSize(prev_val); |
212 |
18 |
unsigned curr_size = datatypes::utils::getSygusTermSize(curr_val); |
213 |
18 |
Assert(prev_size <= curr_size); |
214 |
18 |
if (curr_size == prev_size) |
215 |
|
{ |
216 |
|
Node slem = |
217 |
72 |
nm->mkNode( |
218 |
72 |
AND, es[j - 1].eqNode(vs[j - 1]), es[j].eqNode(vs[j])) |
219 |
36 |
.negate(); |
220 |
36 |
Trace("cegis-unif") |
221 |
|
<< "CegisUnif::lemma, inter-unif-enumerator " |
222 |
18 |
"symmetry breaking lemma : " |
223 |
18 |
<< slem << "\n"; |
224 |
18 |
d_qim.lemma( |
225 |
|
slem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB); |
226 |
18 |
addedUnifEnumSymBreakLemma = true; |
227 |
18 |
break; |
228 |
|
} |
229 |
|
} |
230 |
|
} |
231 |
|
} |
232 |
|
} |
233 |
|
} |
234 |
|
} |
235 |
560 |
return !addedUnifEnumSymBreakLemma; |
236 |
|
} |
237 |
|
|
238 |
684 |
bool CegisUnif::usingConditionPool() const |
239 |
|
{ |
240 |
684 |
return d_sygus_unif.usingConditionPool(); |
241 |
|
} |
242 |
|
|
243 |
147 |
void CegisUnif::setConditions( |
244 |
|
const std::map<Node, std::vector<Node>>& unif_cenums, |
245 |
|
const std::map<Node, std::vector<Node>>& unif_cvalues) |
246 |
|
{ |
247 |
294 |
Node cost_lit = d_u_enum_manager.getAssertedLiteral(); |
248 |
147 |
NodeManager* nm = NodeManager::currentNM(); |
249 |
|
// set the conditions |
250 |
294 |
for (const Node& c : d_unif_candidates) |
251 |
|
{ |
252 |
294 |
for (const Node& e : d_cand_to_strat_pt[c]) |
253 |
|
{ |
254 |
147 |
Assert(unif_cenums.find(e) != unif_cenums.end()); |
255 |
147 |
Assert(unif_cvalues.find(e) != unif_cvalues.end()); |
256 |
|
std::map<Node, std::vector<Node>>::const_iterator itc = |
257 |
147 |
unif_cenums.find(e); |
258 |
|
std::map<Node, std::vector<Node>>::const_iterator itv = |
259 |
147 |
unif_cvalues.find(e); |
260 |
147 |
d_sygus_unif.setConditions(e, cost_lit, itc->second, itv->second); |
261 |
|
// d_sygus_unif.setConditions(e, cost_lit, unif_cenums[e], |
262 |
|
// unif_cvalues[e]); if condition enumerator had value and it is being |
263 |
|
// passively generated, exclude this value |
264 |
147 |
if (usingConditionPool() && !itc->second.empty()) |
265 |
|
{ |
266 |
|
Node eu = itc->second[0]; |
267 |
|
Assert(d_tds->isEnumerator(eu)); |
268 |
|
Assert(!itv->second.empty()); |
269 |
|
if (d_tds->isPassiveEnumerator(eu)) |
270 |
|
{ |
271 |
|
Node g = d_tds->getActiveGuardForEnumerator(eu); |
272 |
|
Node exp_exc = d_tds->getExplain() |
273 |
|
->getExplanationForEquality(eu, itv->second[0]) |
274 |
|
.negate(); |
275 |
|
Node lem = nm->mkNode(OR, g.negate(), exp_exc); |
276 |
|
d_qim.addPendingLemma( |
277 |
|
lem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_COND_EXCLUDE); |
278 |
|
} |
279 |
|
} |
280 |
|
} |
281 |
|
} |
282 |
147 |
} |
283 |
|
|
284 |
280 |
bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, |
285 |
|
const std::vector<Node>& enum_values, |
286 |
|
const std::vector<Node>& candidates, |
287 |
|
std::vector<Node>& candidate_values, |
288 |
|
bool satisfiedRl) |
289 |
|
{ |
290 |
280 |
if (d_unif_candidates.empty()) |
291 |
|
{ |
292 |
|
Assert(d_non_unif_candidates.size() == candidates.size()); |
293 |
|
return Cegis::processConstructCandidates( |
294 |
|
enums, enum_values, candidates, candidate_values, satisfiedRl); |
295 |
|
} |
296 |
280 |
if (Trace.isOn("cegis-unif")) |
297 |
|
{ |
298 |
|
for (const Node& c : d_unif_candidates) |
299 |
|
{ |
300 |
|
// Collect heads of candidates |
301 |
|
Trace("cegis-unif") << " Evaluation heads for " << c << " :\n"; |
302 |
|
for (const Node& hd : d_sygus_unif.getEvalPointHeads(c)) |
303 |
|
{ |
304 |
|
bool isUnit = false; |
305 |
|
// d_rl_eval_hds accumulates eval apps, so need to look at operators |
306 |
|
for (const Node& hd_unit : d_rl_eval_hds) |
307 |
|
{ |
308 |
|
if (hd == hd_unit[0]) |
309 |
|
{ |
310 |
|
isUnit = true; |
311 |
|
break; |
312 |
|
} |
313 |
|
} |
314 |
|
Trace("cegis-unif") << " " << hd << (isUnit ? "*" : "") << " -> "; |
315 |
|
Assert(std::find(enums.begin(), enums.end(), hd) != enums.end()); |
316 |
|
unsigned i = std::distance(enums.begin(), |
317 |
|
std::find(enums.begin(), enums.end(), hd)); |
318 |
|
Assert(i >= 0 && i < enum_values.size()); |
319 |
|
TermDbSygus::toStreamSygus("cegis-unif", enum_values[i]); |
320 |
|
Trace("cegis-unif") << "\n"; |
321 |
|
} |
322 |
|
} |
323 |
|
} |
324 |
|
// the unification enumerators for conditions and their model values |
325 |
560 |
std::map<Node, std::vector<Node>> unif_cenums; |
326 |
560 |
std::map<Node, std::vector<Node>> unif_cvalues; |
327 |
|
// we only proceed to solution building if we are not introducing symmetry |
328 |
|
// breaking lemmas between return values and if we have not previously |
329 |
|
// introduced return values refinement lemmas |
330 |
560 |
if (!getEnumValues(enums, enum_values, unif_cenums, unif_cvalues) |
331 |
280 |
|| !satisfiedRl) |
332 |
|
{ |
333 |
|
// if condition values are being indepedently enumerated, they should be |
334 |
|
// communicated to the decision tree strategies indepedently of we |
335 |
|
// proceeding to attempt solution building |
336 |
133 |
if (usingConditionPool()) |
337 |
|
{ |
338 |
|
setConditions(unif_cenums, unif_cvalues); |
339 |
|
} |
340 |
266 |
Trace("cegis-unif") << (!satisfiedRl |
341 |
266 |
? "..added refinement lemmas" |
342 |
133 |
: "..added unif enum symmetry breaking") |
343 |
133 |
<< "\n---CegisUnif Engine---\n"; |
344 |
|
// if we didn't satisfy the specification, there is no way to repair |
345 |
133 |
return false; |
346 |
|
} |
347 |
147 |
setConditions(unif_cenums, unif_cvalues); |
348 |
|
// build solutions (for unif candidates a divide-and-conquer approach is used) |
349 |
294 |
std::vector<Node> sols; |
350 |
294 |
std::vector<Node> lemmas; |
351 |
147 |
if (d_sygus_unif.constructSolution(sols, lemmas)) |
352 |
|
{ |
353 |
23 |
candidate_values.insert(candidate_values.end(), sols.begin(), sols.end()); |
354 |
23 |
if (Trace.isOn("cegis-unif")) |
355 |
|
{ |
356 |
|
Trace("cegis-unif") << "* Candidate solutions are:\n"; |
357 |
|
for (const Node& sol : sols) |
358 |
|
{ |
359 |
|
Trace("cegis-unif") |
360 |
|
<< "... " << d_tds->sygusToBuiltin(sol, sol.getType()) << "\n"; |
361 |
|
} |
362 |
|
Trace("cegis-unif") << "---CegisUnif Engine---\n"; |
363 |
|
} |
364 |
23 |
return true; |
365 |
|
} |
366 |
|
|
367 |
|
// TODO tie this to the lemma for getting a new condition value |
368 |
124 |
Assert(usingConditionPool() || !lemmas.empty()); |
369 |
248 |
for (const Node& lem : lemmas) |
370 |
|
{ |
371 |
248 |
Trace("cegis-unif-lemma") |
372 |
124 |
<< "CegisUnif::lemma, separation lemma : " << lem << "\n"; |
373 |
124 |
d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION); |
374 |
|
} |
375 |
124 |
Trace("cegis-unif") << "..failed to separate heads\n---CegisUnif Engine---\n"; |
376 |
124 |
return false; |
377 |
|
} |
378 |
|
|
379 |
15 |
void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars, Node lem) |
380 |
|
{ |
381 |
|
// Notify lemma to unification utility and get its purified form |
382 |
30 |
std::map<Node, std::vector<Node>> eval_pts; |
383 |
30 |
Node plem = d_sygus_unif.addRefLemma(lem, eval_pts); |
384 |
15 |
addRefinementLemma(plem); |
385 |
30 |
Trace("cegis-unif-lemma") |
386 |
15 |
<< "CegisUnif::lemma, refinement lemma : " << plem << "\n"; |
387 |
|
// Notify the enumeration manager if there are new evaluation points |
388 |
30 |
for (const std::pair<const Node, std::vector<Node>>& ep : eval_pts) |
389 |
|
{ |
390 |
15 |
Assert(d_cand_to_strat_pt.find(ep.first) != d_cand_to_strat_pt.end()); |
391 |
|
// Notify each strategy point of the respective candidate |
392 |
30 |
for (const Node& n : d_cand_to_strat_pt[ep.first]) |
393 |
|
{ |
394 |
15 |
d_u_enum_manager.registerEvalPts(ep.second, n); |
395 |
|
} |
396 |
|
} |
397 |
|
// Make the refinement lemma and add it to lems. This lemma is guarded by the |
398 |
|
// parent's guard, which has the semantics "this conjecture has a solution", |
399 |
|
// hence this lemma states: if the parent conjecture has a solution, it |
400 |
|
// satisfies the specification for the given concrete point. |
401 |
|
Node rlem = |
402 |
30 |
NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), plem); |
403 |
15 |
d_qim.addPendingLemma(rlem, |
404 |
|
InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REFINEMENT); |
405 |
15 |
} |
406 |
|
|
407 |
1193 |
CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( |
408 |
|
Env& env, |
409 |
|
QuantifiersState& qs, |
410 |
|
QuantifiersInferenceManager& qim, |
411 |
|
TermDbSygus* tds, |
412 |
1193 |
SynthConjecture* parent) |
413 |
1193 |
: DecisionStrategyFmf(env, qs.getValuation()), |
414 |
|
d_qim(qim), |
415 |
|
d_tds(tds), |
416 |
2386 |
d_parent(parent) |
417 |
|
{ |
418 |
1193 |
d_initialized = false; |
419 |
1193 |
options::SygusUnifPiMode mode = options::sygusUnifPi(); |
420 |
1193 |
d_useCondPool = mode == options::SygusUnifPiMode::CENUM |
421 |
1193 |
|| mode == options::SygusUnifPiMode::CENUM_IGAIN; |
422 |
1193 |
} |
423 |
|
|
424 |
17 |
Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) |
425 |
|
{ |
426 |
17 |
NodeManager* nm = NodeManager::currentNM(); |
427 |
17 |
SkolemManager* sm = nm->getSkolemManager(); |
428 |
17 |
Node newLit = sm->mkDummySkolem("G_cost", nm->booleanType()); |
429 |
17 |
unsigned new_size = n + 1; |
430 |
|
|
431 |
|
// allocate an enumerator for each candidate |
432 |
34 |
for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info) |
433 |
|
{ |
434 |
34 |
Node c = ci.first; |
435 |
34 |
TypeNode ct = c.getType(); |
436 |
34 |
Node eu = sm->mkDummySkolem("eu", ct); |
437 |
34 |
Node ceu; |
438 |
17 |
if (!d_useCondPool && !ci.second.d_enums[0].empty()) |
439 |
|
{ |
440 |
|
// make a new conditional enumerator as well, starting the |
441 |
|
// second type around |
442 |
6 |
ceu = sm->mkDummySkolem("cu", ci.second.d_ce_type); |
443 |
|
} |
444 |
|
// register the new enumerators |
445 |
51 |
for (unsigned index = 0; index < 2; index++) |
446 |
|
{ |
447 |
57 |
Node e = index == 0 ? eu : ceu; |
448 |
34 |
if (e.isNull()) |
449 |
|
{ |
450 |
11 |
continue; |
451 |
|
} |
452 |
23 |
setUpEnumerator(e, ci.second, index); |
453 |
|
} |
454 |
|
} |
455 |
|
// register the evaluation points at the new value |
456 |
34 |
for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info) |
457 |
|
{ |
458 |
34 |
Node c = ci.first; |
459 |
35 |
for (const Node& ei : ci.second.d_eval_points) |
460 |
|
{ |
461 |
36 |
Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei |
462 |
18 |
<< " to new size " << new_size << "\n"; |
463 |
18 |
registerEvalPtAtSize(c, ei, newLit, new_size); |
464 |
|
} |
465 |
|
} |
466 |
|
// enforce fairness between number of enumerators and enumerator size |
467 |
17 |
if (new_size > 1) |
468 |
|
{ |
469 |
|
// construct the "virtual enumerator" |
470 |
6 |
if (d_virtual_enum.isNull()) |
471 |
|
{ |
472 |
|
// we construct the default integer grammar with no variables, e.g.: |
473 |
|
// A -> 1 | A+A |
474 |
10 |
TypeNode intTn = nm->integerType(); |
475 |
|
// use a null variable list |
476 |
10 |
Node bvl; |
477 |
10 |
std::string veName("_virtual_enum_grammar"); |
478 |
10 |
SygusDatatype sdt(veName); |
479 |
10 |
TypeNode u = nm->mkSort(veName, NodeManager::SORT_FLAG_PLACEHOLDER); |
480 |
10 |
std::set<TypeNode> unresolvedTypes; |
481 |
5 |
unresolvedTypes.insert(u); |
482 |
10 |
std::vector<TypeNode> cargsEmpty; |
483 |
10 |
Node cr = nm->mkConst(Rational(1)); |
484 |
5 |
sdt.addConstructor(cr, "1", cargsEmpty); |
485 |
10 |
std::vector<TypeNode> cargsPlus; |
486 |
5 |
cargsPlus.push_back(u); |
487 |
5 |
cargsPlus.push_back(u); |
488 |
5 |
sdt.addConstructor(PLUS, cargsPlus); |
489 |
5 |
sdt.initializeDatatype(nm->integerType(), bvl, false, false); |
490 |
10 |
std::vector<DType> datatypes; |
491 |
5 |
datatypes.push_back(sdt.getDatatype()); |
492 |
|
std::vector<TypeNode> dtypes = nm->mkMutualDatatypeTypes( |
493 |
10 |
datatypes, unresolvedTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER); |
494 |
5 |
d_virtual_enum = sm->mkDummySkolem("_ve", dtypes[0]); |
495 |
10 |
d_tds->registerEnumerator( |
496 |
10 |
d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED); |
497 |
|
} |
498 |
|
// if new_size is a power of two, then isPow2 returns log2(new_size)+1 |
499 |
|
// otherwise, this returns 0. In the case it returns 0, we don't care |
500 |
|
// since the floor( log2( i ) ) = floor( log2( i - 1 ) ) and we do not |
501 |
|
// increase our size bound. |
502 |
6 |
unsigned pow_two = Integer(new_size).isPow2(); |
503 |
6 |
if (pow_two > 0) |
504 |
|
{ |
505 |
10 |
Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum); |
506 |
|
Node fair_lemma = |
507 |
10 |
nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1))); |
508 |
5 |
fair_lemma = nm->mkNode(OR, newLit, fair_lemma); |
509 |
10 |
Trace("cegis-unif-enum-lemma") |
510 |
5 |
<< "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n"; |
511 |
|
// this lemma relates the number of conditions we enumerate and the |
512 |
|
// maximum size of a term that is part of our solution. It is of the |
513 |
|
// form: |
514 |
|
// G_uq_i => size(ve) >= log_2( i-1 ) |
515 |
|
// In other words, if we use i conditions, then we allow terms in our |
516 |
|
// solution whose size is at most log_2(i-1). |
517 |
5 |
d_qim.lemma(fair_lemma, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE); |
518 |
|
} |
519 |
|
} |
520 |
|
|
521 |
17 |
return newLit; |
522 |
|
} |
523 |
|
|
524 |
11 |
void CegisUnifEnumDecisionStrategy::initialize( |
525 |
|
const std::vector<Node>& es, |
526 |
|
const std::map<Node, Node>& e_to_cond, |
527 |
|
const std::map<Node, std::vector<Node>>& strategy_lemmas) |
528 |
|
{ |
529 |
11 |
Assert(!d_initialized); |
530 |
11 |
d_initialized = true; |
531 |
11 |
if (es.empty()) |
532 |
|
{ |
533 |
|
return; |
534 |
|
} |
535 |
|
// initialize type information for candidates |
536 |
11 |
NodeManager* nm = NodeManager::currentNM(); |
537 |
11 |
SkolemManager* sm = nm->getSkolemManager(); |
538 |
22 |
for (const Node& e : es) |
539 |
|
{ |
540 |
11 |
Trace("cegis-unif-enum-debug") << "...adding strategy point " << e << "\n"; |
541 |
|
// currently, we allocate the same enumerators for candidates of the same |
542 |
|
// type |
543 |
11 |
d_ce_info[e].d_pt = e; |
544 |
11 |
std::map<Node, Node>::const_iterator itcc = e_to_cond.find(e); |
545 |
11 |
Assert(itcc != e_to_cond.end()); |
546 |
22 |
Node cond = itcc->second; |
547 |
22 |
Trace("cegis-unif-enum-debug") |
548 |
11 |
<< "...its condition strategy point is " << cond << "\n"; |
549 |
11 |
d_ce_info[e].d_ce_type = cond.getType(); |
550 |
|
// initialize the symmetry breaking lemma templates |
551 |
33 |
for (unsigned index = 0; index < 2; index++) |
552 |
|
{ |
553 |
22 |
Assert(d_ce_info[e].d_sbt_lemma_tmpl[index].first.isNull()); |
554 |
42 |
Node sp = index == 0 ? e : cond; |
555 |
|
std::map<Node, std::vector<Node>>::const_iterator it = |
556 |
22 |
strategy_lemmas.find(sp); |
557 |
22 |
if (it == strategy_lemmas.end()) |
558 |
|
{ |
559 |
2 |
continue; |
560 |
|
} |
561 |
|
// collect lemmas for removing redundant ops for this candidate's type |
562 |
|
Node d_sbt_lemma = |
563 |
40 |
it->second.size() == 1 ? it->second[0] : nm->mkNode(AND, it->second); |
564 |
40 |
Trace("cegis-unif-enum-debug") |
565 |
20 |
<< "...adding lemma template to remove redundant operators for " << sp |
566 |
20 |
<< " --> lambda " << sp << ". " << d_sbt_lemma << "\n"; |
567 |
40 |
d_ce_info[e].d_sbt_lemma_tmpl[index] = |
568 |
60 |
std::pair<Node, Node>(d_sbt_lemma, sp); |
569 |
|
} |
570 |
|
} |
571 |
|
|
572 |
|
// register this strategy |
573 |
11 |
d_qim.getDecisionManager()->registerStrategy( |
574 |
|
DecisionManager::STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, this); |
575 |
|
|
576 |
|
// create single condition enumerator for each decision tree strategy |
577 |
11 |
if (d_useCondPool) |
578 |
|
{ |
579 |
|
// allocate a condition enumerator for each candidate |
580 |
|
for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info) |
581 |
|
{ |
582 |
|
Node ceu = sm->mkDummySkolem("cu", ci.second.d_ce_type); |
583 |
|
setUpEnumerator(ceu, ci.second, 1); |
584 |
|
} |
585 |
|
} |
586 |
|
} |
587 |
|
|
588 |
1206 |
void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt( |
589 |
|
Node e, std::vector<Node>& es, unsigned index) const |
590 |
|
{ |
591 |
|
// the number of active enumerators is related to the current cost value |
592 |
1206 |
unsigned num_enums = 0; |
593 |
1206 |
bool has_num_enums = getAssertedLiteralIndex(num_enums); |
594 |
1206 |
AlwaysAssert(has_num_enums); |
595 |
1206 |
num_enums = num_enums + 1; |
596 |
1206 |
if (index == 1) |
597 |
|
{ |
598 |
|
// we always use (cost-1) conditions, or 1 if in the indepedent case |
599 |
603 |
num_enums = !d_useCondPool ? num_enums - 1 : 1; |
600 |
|
} |
601 |
1206 |
if (num_enums > 0) |
602 |
|
{ |
603 |
1057 |
std::map<Node, StrategyPtInfo>::const_iterator itc = d_ce_info.find(e); |
604 |
1057 |
Assert(itc != d_ce_info.end()); |
605 |
1057 |
Assert(num_enums <= itc->second.d_enums[index].size()); |
606 |
3171 |
es.insert(es.end(), |
607 |
1057 |
itc->second.d_enums[index].begin(), |
608 |
5285 |
itc->second.d_enums[index].begin() + num_enums); |
609 |
|
} |
610 |
1206 |
} |
611 |
|
|
612 |
23 |
void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, |
613 |
|
StrategyPtInfo& si, |
614 |
|
unsigned index) |
615 |
|
{ |
616 |
23 |
NodeManager* nm = NodeManager::currentNM(); |
617 |
|
// instantiate template for removing redundant operators |
618 |
23 |
if (!si.d_sbt_lemma_tmpl[index].first.isNull()) |
619 |
|
{ |
620 |
46 |
Node templ = si.d_sbt_lemma_tmpl[index].first; |
621 |
46 |
TNode templ_var = si.d_sbt_lemma_tmpl[index].second; |
622 |
46 |
Node sym_break_red_ops = templ.substitute(templ_var, e); |
623 |
46 |
Trace("cegis-unif-enum-lemma") |
624 |
23 |
<< "CegisUnifEnum::lemma, remove redundant ops of " << e << " : " |
625 |
23 |
<< sym_break_red_ops << "\n"; |
626 |
23 |
d_qim.lemma(sym_break_red_ops, |
627 |
|
InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS); |
628 |
|
} |
629 |
|
// symmetry breaking between enumerators |
630 |
23 |
if (!si.d_enums[index].empty() && index == 0) |
631 |
|
{ |
632 |
12 |
Node e_prev = si.d_enums[index].back(); |
633 |
12 |
Node size_e = nm->mkNode(DT_SIZE, e); |
634 |
12 |
Node size_e_prev = nm->mkNode(DT_SIZE, e_prev); |
635 |
12 |
Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev); |
636 |
12 |
Trace("cegis-unif-enum-lemma") |
637 |
6 |
<< "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n"; |
638 |
6 |
d_qim.lemma(sym_break, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB); |
639 |
|
} |
640 |
|
// register the enumerator |
641 |
23 |
si.d_enums[index].push_back(e); |
642 |
23 |
EnumeratorRole erole = ROLE_ENUM_CONSTRAINED; |
643 |
|
// if we are using a single independent enumerator for conditions, then we |
644 |
|
// allocate an active guard, and are eligible to use variable-agnostic |
645 |
|
// enumeration. |
646 |
23 |
if (d_useCondPool && index == 1) |
647 |
|
{ |
648 |
|
erole = ROLE_ENUM_POOL; |
649 |
|
} |
650 |
46 |
Trace("cegis-unif-enum") << "* Registering new enumerator " << e |
651 |
23 |
<< " to strategy point " << si.d_pt << "\n"; |
652 |
23 |
d_tds->registerEnumerator(e, si.d_pt, d_parent, erole); |
653 |
23 |
} |
654 |
|
|
655 |
15 |
void CegisUnifEnumDecisionStrategy::registerEvalPts( |
656 |
|
const std::vector<Node>& eis, Node e) |
657 |
|
{ |
658 |
|
// candidates of the same type are managed |
659 |
15 |
std::map<Node, StrategyPtInfo>::iterator it = d_ce_info.find(e); |
660 |
15 |
Assert(it != d_ce_info.end()); |
661 |
30 |
it->second.d_eval_points.insert( |
662 |
30 |
it->second.d_eval_points.end(), eis.begin(), eis.end()); |
663 |
|
// register at all already allocated sizes |
664 |
41 |
for (const Node& ei : eis) |
665 |
|
{ |
666 |
26 |
Assert(ei.getType() == e.getType()); |
667 |
63 |
for (unsigned j = 0, size = d_literals.size(); j < size; j++) |
668 |
|
{ |
669 |
74 |
Trace("cegis-unif-enum") << "...for cand " << e << " adding hd " << ei |
670 |
37 |
<< " at size " << j << "\n"; |
671 |
37 |
registerEvalPtAtSize(e, ei, d_literals[j], j + 1); |
672 |
|
} |
673 |
|
} |
674 |
15 |
} |
675 |
|
|
676 |
55 |
void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e, |
677 |
|
Node ei, |
678 |
|
Node guq_lit, |
679 |
|
unsigned n) |
680 |
|
{ |
681 |
|
// must be equal to one of the first n enums |
682 |
55 |
std::map<Node, StrategyPtInfo>::iterator itc = d_ce_info.find(e); |
683 |
55 |
Assert(itc != d_ce_info.end()); |
684 |
55 |
Assert(itc->second.d_enums[0].size() >= n); |
685 |
110 |
std::vector<Node> disj; |
686 |
55 |
disj.push_back(guq_lit.negate()); |
687 |
145 |
for (unsigned i = 0; i < n; i++) |
688 |
|
{ |
689 |
90 |
disj.push_back(ei.eqNode(itc->second.d_enums[0][i])); |
690 |
|
} |
691 |
110 |
Node lem = NodeManager::currentNM()->mkNode(OR, disj); |
692 |
110 |
Trace("cegis-unif-enum-lemma") |
693 |
55 |
<< "CegisUnifEnum::lemma, domain:" << lem << "\n"; |
694 |
55 |
d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN); |
695 |
55 |
} |
696 |
|
|
697 |
|
} // namespace quantifiers |
698 |
|
} // namespace theory |
699 |
22746 |
} // namespace cvc5 |