1 /********************* */
2 /*! \file sygus_pbe.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Haniel Barbosa, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
11 **
12 ** \brief utility for processing programming by examples synthesis conjectures
13 **
14 **/
15 #include "theory/quantifiers/sygus/sygus_pbe.h"
16
17 #include "expr/datatype.h"
18 #include "options/quantifiers_options.h"
19 #include "theory/datatypes/datatypes_rewriter.h"
20 #include "theory/quantifiers/sygus/synth_conjecture.h"
21 #include "theory/quantifiers/sygus/term_database_sygus.h"
22 #include "theory/quantifiers/term_util.h"
23 #include "util/random.h"
24
25 using namespace CVC4;
26 using namespace CVC4::kind;
27
28 namespace CVC4 {
29 namespace theory {
30 namespace quantifiers {
31
SygusPbe(QuantifiersEngine * qe,SynthConjecture * p)32 SygusPbe::SygusPbe(QuantifiersEngine* qe, SynthConjecture* p)
33 : SygusModule(qe, p)
34 {
35 d_true = NodeManager::currentNM()->mkConst(true);
36 d_false = NodeManager::currentNM()->mkConst(false);
37 d_is_pbe = false;
38 }
39
~SygusPbe()40 SygusPbe::~SygusPbe() {}
41
42 //--------------------------------- collecting finite input/output domain information
43
collectExamples(Node n,std::map<Node,bool> & visited,bool hasPol,bool pol)44 bool SygusPbe::collectExamples(Node n,
45 std::map<Node, bool>& visited,
46 bool hasPol,
47 bool pol)
48 {
49 if( visited.find( n )==visited.end() ){
50 visited[n] = true;
51 Node neval;
52 Node n_output;
53 bool neval_is_evalapp = false;
54 if (n.getKind() == DT_SYGUS_EVAL)
55 {
56 neval = n;
57 if( hasPol ){
58 n_output = pol ? d_true : d_false;
59 }
60 neval_is_evalapp = true;
61 }
62 else if (n.getKind() == EQUAL && hasPol && pol)
63 {
64 for( unsigned r=0; r<2; r++ ){
65 if (n[r].getKind() == DT_SYGUS_EVAL)
66 {
67 neval = n[r];
68 if( n[1-r].isConst() ){
69 n_output = n[1-r];
70 }
71 neval_is_evalapp = true;
72 }
73 }
74 }
75 // is it an evaluation function?
76 if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end())
77 {
78 Trace("sygus-pbe-debug")
79 << "Process head: " << n << " == " << n_output << std::endl;
80 // If n_output is null, then neval does not have a constant value
81 // If n_output is non-null, then neval is constrained to always be
82 // that value.
83 if (!n_output.isNull())
84 {
85 std::map<Node, Node>::iterator itet = d_exampleTermMap.find(neval);
86 if (itet == d_exampleTermMap.end())
87 {
88 d_exampleTermMap[neval] = n_output;
89 }
90 else if (itet->second != n_output)
91 {
92 // We have a conflicting pair f( c ) = d1 ^ f( c ) = d2 for d1 != d2,
93 // the conjecture is infeasible.
94 return false;
95 }
96 }
97 // get the evaluation head
98 Node eh = neval[0];
99 std::map<Node, bool>::iterator itx = d_examples_invalid.find(eh);
100 if (itx == d_examples_invalid.end())
101 {
102 // collect example
103 bool success = true;
104 std::vector<Node> ex;
105 for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++)
106 {
107 if (!neval[j].isConst())
108 {
109 success = false;
110 break;
111 }
112 ex.push_back(neval[j]);
113 }
114 if (success)
115 {
116 d_examples[eh].push_back(ex);
117 d_examples_out[eh].push_back(n_output);
118 d_examples_term[eh].push_back(neval);
119 if (n_output.isNull())
120 {
121 d_examples_out_invalid[eh] = true;
122 }
123 else
124 {
125 Assert(n_output.isConst());
126 }
127 // finished processing this node
128 return true;
129 }
130 d_examples_invalid[eh] = true;
131 d_examples_out_invalid[eh] = true;
132 }
133 }
134 for( unsigned i=0; i<n.getNumChildren(); i++ ){
135 bool newHasPol;
136 bool newPol;
137 QuantPhaseReq::getEntailPolarity(n, i, hasPol, pol, newHasPol, newPol);
138 if (!collectExamples(n[i], visited, newHasPol, newPol))
139 {
140 return false;
141 }
142 }
143 }
144 return true;
145 }
146
initialize(Node n,const std::vector<Node> & candidates,std::vector<Node> & lemmas)147 bool SygusPbe::initialize(Node n,
148 const std::vector<Node>& candidates,
149 std::vector<Node>& lemmas)
150 {
151 Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
152 NodeManager* nm = NodeManager::currentNM();
153
154 for (unsigned i = 0; i < candidates.size(); i++)
155 {
156 Node v = candidates[i];
157 d_examples[v].clear();
158 d_examples_out[v].clear();
159 d_examples_term[v].clear();
160 }
161
162 std::map<Node, bool> visited;
163 // n is negated conjecture
164 if (!collectExamples(n, visited, true, false))
165 {
166 Trace("sygus-pbe") << "...conflicting examples" << std::endl;
167 Node infeasible = d_parent->getGuard().negate();
168 lemmas.push_back(infeasible);
169 return false;
170 }
171
172 for (unsigned i = 0; i < candidates.size(); i++)
173 {
174 Node v = candidates[i];
175 Trace("sygus-pbe") << " examples for " << v << " : ";
176 if (d_examples_invalid.find(v) != d_examples_invalid.end())
177 {
178 Trace("sygus-pbe") << "INVALID" << std::endl;
179 }
180 else
181 {
182 Trace("sygus-pbe") << std::endl;
183 for (unsigned j = 0; j < d_examples[v].size(); j++)
184 {
185 Trace("sygus-pbe") << " ";
186 for (unsigned k = 0; k < d_examples[v][j].size(); k++)
187 {
188 Trace("sygus-pbe") << d_examples[v][j][k] << " ";
189 }
190 if (!d_examples_out[v][j].isNull())
191 {
192 Trace("sygus-pbe") << " -> " << d_examples_out[v][j];
193 }
194 Trace("sygus-pbe") << std::endl;
195 }
196 }
197 }
198
199 if (!options::sygusUnifPbe())
200 {
201 // we are not doing unification
202 return false;
203 }
204
205 // check if all candidates are valid examples
206 d_is_pbe = true;
207 for (const Node& c : candidates)
208 {
209 if (d_examples[c].empty()
210 || d_examples_out_invalid.find(c) != d_examples_out_invalid.end())
211 {
212 d_is_pbe = false;
213 return false;
214 }
215 }
216 for (const Node& c : candidates)
217 {
218 Assert(d_examples.find(c) != d_examples.end());
219 Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
220 << std::endl;
221 std::map<Node, std::vector<Node>> strategy_lemmas;
222 d_sygus_unif[c].initializeCandidate(
223 d_qe, c, d_candidate_to_enum[c], strategy_lemmas);
224 Assert(!d_candidate_to_enum[c].empty());
225 Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
226 << " enumerators for " << c << "..." << std::endl;
227 // collect list per type of strategy points with strategy lemmas
228 std::map<TypeNode, std::vector<Node>> tn_to_strategy_pt;
229 for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas)
230 {
231 TypeNode tnsp = p.first.getType();
232 tn_to_strategy_pt[tnsp].push_back(p.first);
233 }
234 // initialize the enumerators
235 for (const Node& e : d_candidate_to_enum[c])
236 {
237 TypeNode etn = e.getType();
238 d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL, false);
239 d_enum_to_candidate[e] = c;
240 TNode te = e;
241 // initialize static symmetry breaking lemmas for it
242 // we register only one "master" enumerator per type
243 // thus, the strategy lemmas (which are for individual strategy points)
244 // are applicable (disjunctively) to the master enumerator
245 std::map<TypeNode, std::vector<Node>>::iterator itt =
246 tn_to_strategy_pt.find(etn);
247 if (itt != tn_to_strategy_pt.end())
248 {
249 std::vector<Node> disj;
250 for (const Node& sp : itt->second)
251 {
252 std::map<Node, std::vector<Node>>::iterator itsl =
253 strategy_lemmas.find(sp);
254 Assert(itsl != strategy_lemmas.end());
255 if (!itsl->second.empty())
256 {
257 TNode tsp = sp;
258 Node lem = itsl->second.size() == 1 ? itsl->second[0]
259 : nm->mkNode(AND, itsl->second);
260 if (tsp != te)
261 {
262 lem = lem.substitute(tsp, te);
263 }
264 if (std::find(disj.begin(), disj.end(), lem) == disj.end())
265 {
266 disj.push_back(lem);
267 }
268 }
269 }
270 // add its active guard
271 Node ag = d_tds->getActiveGuardForEnumerator(e);
272 Assert(!ag.isNull());
273 disj.push_back(ag.negate());
274 Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj);
275 // Apply extended rewriting on the lemma. This helps utilities like
276 // SygusEnumerator more easily recognize the shape of this lemma, e.g.
277 // ( ~is-ite(x) or ( ~is-ite(x) ^ P ) ) --> ~is-ite(x).
278 lem = d_tds->getExtRewriter()->extendedRewrite(lem);
279 Trace("sygus-pbe") << " static redundant op lemma : " << lem
280 << std::endl;
281 // Register as a symmetry breaking lemma with the term database.
282 // This will either be processed via a lemma on the output channel
283 // of the sygus extension of the datatypes solver, or internally
284 // encoded as a constraint to an active enumerator.
285 d_tds->registerSymBreakLemma(e, lem, etn, 0, false);
286 }
287 }
288 Trace("sygus-pbe") << "Initialize " << d_examples[c].size()
289 << " example points for " << c << "..." << std::endl;
290 // initialize the examples
291 for (unsigned i = 0, nex = d_examples[c].size(); i < nex; i++)
292 {
293 d_sygus_unif[c].addExample(d_examples[c][i], d_examples_out[c][i]);
294 }
295 }
296 return true;
297 }
298
addTerm(Node b,const std::vector<Node> & exOut)299 Node SygusPbe::PbeTrie::addTerm(Node b, const std::vector<Node>& exOut)
300 {
301 PbeTrie* curr = this;
302 for (const Node& eo : exOut)
303 {
304 curr = &(curr->d_children[eo]);
305 }
306 if (!curr->d_children.empty())
307 {
308 return curr->d_children.begin()->first;
309 }
310 curr->d_children.insert(std::pair<Node, PbeTrie>(b, PbeTrie()));
311 return b;
312 }
313
hasExamples(Node e)314 bool SygusPbe::hasExamples(Node e)
315 {
316 if (isPbe()) {
317 e = d_tds->getSynthFunForEnumerator(e);
318 Assert(!e.isNull());
319 std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
320 if (itx == d_examples_invalid.end()) {
321 return d_examples.find(e) != d_examples.end();
322 }
323 }
324 return false;
325 }
326
getNumExamples(Node e)327 unsigned SygusPbe::getNumExamples(Node e)
328 {
329 e = d_tds->getSynthFunForEnumerator(e);
330 Assert(!e.isNull());
331 std::map<Node, std::vector<std::vector<Node> > >::iterator it =
332 d_examples.find(e);
333 if (it != d_examples.end()) {
334 return it->second.size();
335 } else {
336 return 0;
337 }
338 }
339
getExample(Node e,unsigned i,std::vector<Node> & ex)340 void SygusPbe::getExample(Node e, unsigned i, std::vector<Node>& ex)
341 {
342 e = d_tds->getSynthFunForEnumerator(e);
343 Assert(!e.isNull());
344 std::map<Node, std::vector<std::vector<Node> > >::iterator it =
345 d_examples.find(e);
346 if (it != d_examples.end()) {
347 Assert(i < it->second.size());
348 ex.insert(ex.end(), it->second[i].begin(), it->second[i].end());
349 } else {
350 Assert(false);
351 }
352 }
353
getExampleOut(Node e,unsigned i)354 Node SygusPbe::getExampleOut(Node e, unsigned i)
355 {
356 e = d_tds->getSynthFunForEnumerator(e);
357 Assert(!e.isNull());
358 std::map<Node, std::vector<Node> >::iterator it = d_examples_out.find(e);
359 if (it != d_examples_out.end()) {
360 Assert(i < it->second.size());
361 return it->second[i];
362 } else {
363 Assert(false);
364 return Node::null();
365 }
366 }
367
addSearchVal(TypeNode tn,Node e,Node bvr)368 Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr)
369 {
370 Assert(isPbe());
371 Assert(!e.isNull());
372 if (d_tds->isVariableAgnosticEnumerator(e))
373 {
374 // we cannot apply conjecture-specific symmetry breaking on variable
375 // agnostic enumerators
376 return Node::null();
377 }
378 Node ee = d_tds->getSynthFunForEnumerator(e);
379 Assert(!e.isNull());
380 std::map<Node, bool>::iterator itx = d_examples_invalid.find(ee);
381 if (itx == d_examples_invalid.end()) {
382 // compute example values with the I/O utility
383 std::vector<Node> vals;
384 Trace("sygus-pbe-debug")
385 << "Compute examples " << bvr << "..." << std::endl;
386 d_sygus_unif[ee].computeExamples(e, bvr, vals);
387 Assert(vals.size() == d_examples[ee].size());
388 Trace("sygus-pbe-debug") << "...got " << vals << std::endl;
389 Trace("sygus-pbe-debug") << "Add to trie..." << std::endl;
390 Node ret = d_pbe_trie[e][tn].addTerm(bvr, vals);
391 Trace("sygus-pbe-debug") << "...got " << ret << std::endl;
392 if (ret != bvr)
393 {
394 Trace("sygus-pbe-debug") << "...clear example cache" << std::endl;
395 d_sygus_unif[ee].clearExampleCache(e, bvr);
396 }
397 Assert(ret.getType() == bvr.getType());
398 return ret;
399 }
400 return Node::null();
401 }
402
evaluateBuiltin(TypeNode tn,Node bn,Node e,unsigned i)403 Node SygusPbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i)
404 {
405 e = d_tds->getSynthFunForEnumerator(e);
406 Assert(!e.isNull());
407 std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
408 if (itx == d_examples_invalid.end()) {
409 std::map<Node, std::vector<std::vector<Node> > >::iterator it =
410 d_examples.find(e);
411 if (it != d_examples.end()) {
412 Assert(i < it->second.size());
413 return d_tds->evaluateBuiltin(tn, bn, it->second[i]);
414 }
415 }
416 return Rewriter::rewrite(bn);
417 }
418
419 // ------------------------------------------- solution construction from enumeration
420
getTermList(const std::vector<Node> & candidates,std::vector<Node> & terms)421 void SygusPbe::getTermList(const std::vector<Node>& candidates,
422 std::vector<Node>& terms)
423 {
424 for( unsigned i=0; i<candidates.size(); i++ ){
425 Node v = candidates[i];
426 std::map<Node, std::vector<Node> >::iterator it =
427 d_candidate_to_enum.find(v);
428 if (it != d_candidate_to_enum.end())
429 {
430 terms.insert(terms.end(), it->second.begin(), it->second.end());
431 }
432 }
433 }
434
allowPartialModel()435 bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); }
436
constructCandidates(const std::vector<Node> & enums,const std::vector<Node> & enum_values,const std::vector<Node> & candidates,std::vector<Node> & candidate_values,std::vector<Node> & lems)437 bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
438 const std::vector<Node>& enum_values,
439 const std::vector<Node>& candidates,
440 std::vector<Node>& candidate_values,
441 std::vector<Node>& lems)
442 {
443 Assert( enums.size()==enum_values.size() );
444 if( !enums.empty() ){
445 unsigned min_term_size = 0;
446 Trace("sygus-pbe-enum") << "Register new enumerated values : " << std::endl;
447 std::vector<unsigned> szs;
448 for (unsigned i = 0, esize = enums.size(); i < esize; i++)
449 {
450 Trace("sygus-pbe-enum") << " " << enums[i] << " -> ";
451 TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]);
452 Trace("sygus-pbe-enum") << std::endl;
453 if (!enum_values[i].isNull())
454 {
455 unsigned sz = d_tds->getSygusTermSize(enum_values[i]);
456 szs.push_back(sz);
457 if (i == 0 || sz < min_term_size)
458 {
459 min_term_size = sz;
460 }
461 }
462 else
463 {
464 szs.push_back(0);
465 }
466 }
467 // Assume two enumerators of types T1 and T2.
468 // If options::sygusPbeMultiFair() is true,
469 // we ensure that all values of type T1 and size n are enumerated before
470 // any term of type T2 of size n+d, and vice versa, where d is
471 // set by options::sygusPbeMultiFairDiff(). If d is zero, then our
472 // enumeration is such that all terms of T1 or T2 of size n are considered
473 // before any term of size n+1.
474 int diffAllow = options::sygusPbeMultiFairDiff();
475 std::vector<unsigned> enum_consider;
476 for (unsigned i = 0, esize = enums.size(); i < esize; i++)
477 {
478 if (!enum_values[i].isNull())
479 {
480 Assert(szs[i] >= min_term_size);
481 int diff = szs[i] - min_term_size;
482 if (!options::sygusPbeMultiFair() || diff <= diffAllow)
483 {
484 enum_consider.push_back(i);
485 }
486 }
487 }
488
489 // only consider the enumerators that are at minimum size (for fairness)
490 Trace("sygus-pbe-enum") << "...register " << enum_consider.size() << " / " << enums.size() << std::endl;
491 NodeManager* nm = NodeManager::currentNM();
492 for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; i++)
493 {
494 unsigned j = enum_consider[i];
495 Node e = enums[j];
496 Node v = enum_values[j];
497 Assert(d_enum_to_candidate.find(e) != d_enum_to_candidate.end());
498 Node c = d_enum_to_candidate[e];
499 std::vector<Node> enum_lems;
500 d_sygus_unif[c].notifyEnumeration(e, v, enum_lems);
501 if (!enum_lems.empty())
502 {
503 // the lemmas must be guarded by the active guard of the enumerator
504 Node g = d_tds->getActiveGuardForEnumerator(e);
505 Assert(!g.isNull());
506 for (unsigned j = 0, size = enum_lems.size(); j < size; j++)
507 {
508 enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]);
509 }
510 lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
511 }
512 }
513 }
514 for( unsigned i=0; i<candidates.size(); i++ ){
515 Node c = candidates[i];
516 //build decision tree for candidate
517 std::vector<Node> sol;
518 if (d_sygus_unif[c].constructSolution(sol, lems))
519 {
520 Assert(sol.size() == 1);
521 candidate_values.push_back(sol[0]);
522 }
523 else
524 {
525 return false;
526 }
527 }
528 return true;
529 }
530
531 }
532 }
533 }
534