1 /********************* */
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Haniel Barbosa
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
12 ** \brief Implementation of cegis
15 #include "theory/quantifiers/sygus/cegis.h"
16 #include "expr/node_algorithm.h"
17 #include "options/base_options.h"
18 #include "options/quantifiers_options.h"
19 #include "printer/printer.h"
20 #include "theory/quantifiers/sygus/example_min_eval.h"
21 #include "theory/quantifiers/sygus/synth_conjecture.h"
22 #include "theory/quantifiers/sygus/term_database_sygus.h"
23 #include "theory/quantifiers_engine.h"
24 #include "theory/theory_engine.h"
27 using namespace CVC4::kind
;
28 using namespace CVC4::context
;
32 namespace quantifiers
{
34 Cegis::Cegis(QuantifiersEngine
* qe
, SynthConjecture
* p
)
35 : SygusModule(qe
, p
), d_eval_unfold(nullptr), d_usingSymCons(false)
37 d_eval_unfold
= qe
->getTermDatabaseSygus()->getEvalUnfold();
40 bool Cegis::initialize(Node conj
,
42 const std::vector
<Node
>& candidates
,
43 std::vector
<Node
>& lemmas
)
46 if (d_base_body
.getKind() == NOT
&& d_base_body
[0].getKind() == FORALL
)
48 for (const Node
& v
: d_base_body
[0][0])
50 d_base_vars
.push_back(v
);
52 d_base_body
= d_base_body
[0][1];
55 // assign the cegis sampler if applicable
56 if (options::cegisSample() != options::CegisSampleMode::NONE
)
58 Trace("cegis-sample") << "Initialize sampler for " << d_base_body
<< "..."
60 TypeNode bt
= d_base_body
.getType();
61 d_cegis_sampler
.initialize(bt
, d_base_vars
, options::sygusSamples());
63 return processInitialize(conj
, n
, candidates
, lemmas
);
66 bool Cegis::processInitialize(Node conj
,
68 const std::vector
<Node
>& candidates
,
69 std::vector
<Node
>& lemmas
)
71 Trace("cegis") << "Initialize cegis..." << std::endl
;
72 unsigned csize
= candidates
.size();
73 // The role of enumerators is to be either the single solution or part of
74 // a solution involving multiple enumerators.
75 EnumeratorRole erole
=
76 csize
== 1 ? ROLE_ENUM_SINGLE_SOLUTION
: ROLE_ENUM_MULTI_SOLUTION
;
77 // initialize an enumerator for each candidate
78 for (unsigned i
= 0; i
< csize
; i
++)
80 Trace("cegis") << "...register enumerator " << candidates
[i
];
81 // We use symbolic constants if we are doing repair constants or if the
82 // grammar construction was not simple.
83 if (options::sygusRepairConst()
84 || options::sygusGrammarConsMode()
85 != options::SygusGrammarConsMode::SIMPLE
)
87 TypeNode ctn
= candidates
[i
].getType();
88 d_tds
->registerSygusType(ctn
);
89 SygusTypeInfo
& cti
= d_tds
->getTypeInfo(ctn
);
90 if (cti
.hasSubtermSymbolicCons())
92 // remember that we are using symbolic constructors
93 d_usingSymCons
= true;
94 Trace("cegis") << " (using symbolic constructors)";
97 Trace("cegis") << std::endl
;
98 d_tds
->registerEnumerator(candidates
[i
], candidates
[i
], d_parent
, erole
);
103 void Cegis::getTermList(const std::vector
<Node
>& candidates
,
104 std::vector
<Node
>& enums
)
106 enums
.insert(enums
.end(), candidates
.begin(), candidates
.end());
109 bool Cegis::addEvalLemmas(const std::vector
<Node
>& candidates
,
110 const std::vector
<Node
>& candidate_values
,
111 std::vector
<Node
>& lems
)
113 // First, decide if this call will apply "conjecture-specific refinement".
114 // In other words, in some settings, the following method will identify and
115 // block a class of solutions {candidates -> S} that generalizes the current
116 // one (given by {candidates -> candidate_values}), such that for each
117 // candidate_values' in S, we have that {candidates -> candidate_values'} is
118 // also not a solution for the given conjecture. We may not
119 // apply this form of refinement if any (relevant) enumerator in candidates is
120 // "actively generated" (see TermDbSygs::isPassiveEnumerator), since its
121 // model values are themselves interpreted as classes of solutions.
123 for (const Node
& v
: candidates
)
125 // if it is relevant to refinement
126 if (d_refinement_lemma_vars
.find(v
) != d_refinement_lemma_vars
.end())
128 if (!d_tds
->isPassiveEnumerator(v
))
135 NodeManager
* nm
= NodeManager::currentNM();
136 bool addedEvalLemmas
= false;
137 // Refinement evaluation should not be done for grammars with symbolic
139 bool doRefEval
= options::sygusRefEval() && !d_usingSymCons
;
142 Trace("cegqi-engine") << " *** Do refinement lemma evaluation"
143 << (doGen
? " with conjecture-specific refinement"
145 << "..." << std::endl
;
146 // see if any refinement lemma is refuted by evaluation
149 std::vector
<Node
> cre_lems
;
150 getRefinementEvalLemmas(candidates
, candidate_values
, cre_lems
);
151 if (!cre_lems
.empty())
153 lems
.insert(lems
.end(), cre_lems
.begin(), cre_lems
.end());
154 addedEvalLemmas
= true;
155 if (Trace
.isOn("cegqi-lemma"))
157 for (const Node
& lem
: cre_lems
)
160 << "Cegqi::Lemma : ref evaluation : " << lem
<< std::endl
;
163 /* we could, but do not return here. experimentally, it is better to
164 add the lemmas below as well, in parallel. */
169 // just check whether the refinement lemmas are satisfied, fail if not
170 if (checkRefinementEvalLemmas(candidates
, candidate_values
))
172 Trace("cegqi-engine") << "...(actively enumerated) candidate failed "
173 "refinement lemma evaluation."
179 // we only do evaluation unfolding for passive enumerators
180 bool doEvalUnfold
= (doGen
&& options::sygusEvalUnfold()) || d_usingSymCons
;
183 Trace("cegqi-engine") << " *** Do evaluation unfolding..." << std::endl
;
184 std::vector
<Node
> eager_terms
, eager_vals
, eager_exps
;
185 for (unsigned i
= 0, size
= candidates
.size(); i
< size
; ++i
)
187 Trace("cegqi-debug") << " register " << candidates
[i
] << " -> "
188 << candidate_values
[i
] << std::endl
;
189 d_eval_unfold
->registerModelValue(candidates
[i
],
195 Trace("cegqi-debug") << "...produced " << eager_terms
.size()
196 << " evaluation unfold lemmas.\n";
197 for (unsigned i
= 0, size
= eager_terms
.size(); i
< size
; ++i
)
199 Node lem
= nm
->mkNode(
200 OR
, eager_exps
[i
].negate(), eager_terms
[i
].eqNode(eager_vals
[i
]));
202 addedEvalLemmas
= true;
203 Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem
207 return addedEvalLemmas
;
210 Node
Cegis::getRefinementLemmaFormula()
212 std::vector
<Node
> conj
;
214 conj
.end(), d_refinement_lemmas
.begin(), d_refinement_lemmas
.end());
215 // get the propagated values
216 for (unsigned i
= 0, nprops
= d_rl_eval_hds
.size(); i
< nprops
; i
++)
218 conj
.push_back(d_rl_eval_hds
[i
].eqNode(d_rl_vals
[i
]));
221 NodeManager
* nm
= NodeManager::currentNM();
225 ret
= nm
->mkConst(true);
229 ret
= conj
.size() == 1 ? conj
[0] : nm
->mkNode(AND
, conj
);
234 bool Cegis::constructCandidates(const std::vector
<Node
>& enums
,
235 const std::vector
<Node
>& enum_values
,
236 const std::vector
<Node
>& candidates
,
237 std::vector
<Node
>& candidate_values
,
238 std::vector
<Node
>& lems
)
240 if (Trace
.isOn("cegis"))
242 Trace("cegis") << " Enumerators :\n";
243 for (unsigned i
= 0, size
= enums
.size(); i
< size
; ++i
)
245 Trace("cegis") << " " << enums
[i
] << " -> ";
246 TermDbSygus::toStreamSygus("cegis", enum_values
[i
]);
247 Trace("cegis") << "\n";
250 // if we are using grammar-based repair
251 if (d_usingSymCons
&& options::sygusRepairConst())
253 SygusRepairConst
* src
= d_parent
->getRepairConst();
254 Assert(src
!= nullptr);
255 // check if any enum_values have symbolic terms that must be repaired
256 bool mustRepair
= false;
257 for (const Node
& c
: enum_values
)
259 if (SygusRepairConst::mustRepair(c
))
265 Trace("cegis") << "...must repair is: " << mustRepair
<< std::endl
;
266 // if the solution contains a subterm that must be repaired
269 std::vector
<Node
> fail_cvs
= enum_values
;
270 Assert(candidates
.size() == fail_cvs
.size());
271 // try to solve entire problem?
272 if (src
->repairSolution(candidates
, fail_cvs
, candidate_values
))
276 Node rl
= getRefinementLemmaFormula();
277 // try to solve for the refinement lemmas only
279 src
->repairSolution(rl
, candidates
, fail_cvs
, candidate_values
);
280 // Even if ret is true, we will exclude the skeleton as well; this means
281 // that we have one chance to repair each skeleton. It is possible however
282 // that we might want to repair the same skeleton multiple times.
283 std::vector
<Node
> exp
;
284 for (unsigned i
= 0, size
= enums
.size(); i
< size
; i
++)
286 d_tds
->getExplain()->getExplanationForEquality(
287 enums
[i
], enum_values
[i
], exp
);
289 Assert(!exp
.empty());
290 NodeManager
* nm
= NodeManager::currentNM();
291 Node expn
= exp
.size() == 1 ? exp
[0] : nm
->mkNode(AND
, exp
);
293 expn
= nm
->mkNode(OR
, d_parent
->getGuard().negate(), expn
.negate());
294 lems
.push_back(expn
);
299 // evaluate on refinement lemmas
300 bool addedEvalLemmas
= addEvalLemmas(enums
, enum_values
, lems
);
302 // try to construct candidates
303 if (!processConstructCandidates(enums
,
313 if (options::cegisSample() != options::CegisSampleMode::NONE
&& lems
.empty())
315 // if we didn't add a lemma, trying sampling to add a refinement lemma
316 // that immediately refutes the candidate we just constructed
317 if (sampleAddRefinementLemma(candidates
, candidate_values
, lems
))
319 candidate_values
.clear();
320 // restart (should be guaranteed to add evaluation lemmas on this call)
321 return constructCandidates(
322 enums
, enum_values
, candidates
, candidate_values
, lems
);
328 bool Cegis::processConstructCandidates(const std::vector
<Node
>& enums
,
329 const std::vector
<Node
>& enum_values
,
330 const std::vector
<Node
>& candidates
,
331 std::vector
<Node
>& candidate_values
,
333 std::vector
<Node
>& lems
)
337 candidate_values
.insert(
338 candidate_values
.end(), enum_values
.begin(), enum_values
.end());
344 void Cegis::addRefinementLemma(Node lem
)
346 Trace("cegis-rl") << "Cegis::addRefinementLemma: " << lem
<< std::endl
;
347 d_refinement_lemmas
.push_back(lem
);
348 // apply existing substitution
350 if (!d_rl_eval_hds
.empty())
352 slem
= lem
.substitute(d_rl_eval_hds
.begin(),
357 // rewrite with extended rewriter
358 slem
= d_tds
->getExtRewriter()->extendedRewrite(slem
);
359 // collect all variables in slem
360 expr::getSymbols(slem
, d_refinement_lemma_vars
);
361 std::vector
<Node
> waiting
;
362 waiting
.push_back(lem
);
363 unsigned wcounter
= 0;
364 // while we are not done adding lemmas
365 while (wcounter
< waiting
.size())
367 // add the conjunct, possibly propagating
368 addRefinementLemmaConjunct(wcounter
, waiting
);
373 void Cegis::addRefinementLemmaConjunct(unsigned wcounter
,
374 std::vector
<Node
>& waiting
)
376 Node lem
= waiting
[wcounter
];
377 lem
= Rewriter::rewrite(lem
);
378 // apply substitution and rewrite if applicable
381 if (!lem
.getConst
<bool>())
383 // conjecture is infeasible
390 // break into conjunctions
391 if (lem
.getKind() == AND
)
393 for (const Node
& lc
: lem
)
395 waiting
.push_back(lc
);
399 // does this correspond to a substitution?
400 NodeManager
* nm
= NodeManager::currentNM();
403 if (lem
.getKind() == EQUAL
)
405 for (unsigned i
= 0; i
< 2; i
++)
407 if (lem
[i
].isConst() && d_tds
->isEvaluationPoint(lem
[1 - i
]))
417 term
= lem
.getKind() == NOT
? lem
[0] : lem
;
418 // predicate case: the conjunct is a (negated) evaluation point
419 if (d_tds
->isEvaluationPoint(term
))
421 val
= nm
->mkConst(lem
.getKind() != NOT
);
426 if (d_refinement_lemma_unit
.find(lem
) != d_refinement_lemma_unit
.end())
431 Trace("cegis-rl") << "* cegis-rl: propagate: " << term
<< " -> " << val
433 d_rl_eval_hds
.push_back(term
);
434 d_rl_vals
.push_back(val
);
435 d_refinement_lemma_unit
.insert(lem
);
437 // apply to waiting lemmas beyond this one
438 for (unsigned i
= wcounter
+ 1, size
= waiting
.size(); i
< size
; i
++)
440 waiting
[i
] = waiting
[i
].substitute(term
, val
);
442 // apply to all existing refinement lemmas
443 std::vector
<Node
> to_rem
;
444 for (const Node
& rl
: d_refinement_lemma_conj
)
446 Node srl
= rl
.substitute(term
, val
);
449 Trace("cegis-rl") << "* cegis-rl: replace: " << rl
<< " -> " << srl
451 waiting
.push_back(srl
);
452 to_rem
.push_back(rl
);
455 for (const Node
& tr
: to_rem
)
457 d_refinement_lemma_conj
.erase(tr
);
462 if (Trace
.isOn("cegis-rl"))
464 if (d_refinement_lemma_conj
.find(lem
) == d_refinement_lemma_conj
.end())
466 Trace("cegis-rl") << "cegis-rl: add: " << lem
<< std::endl
;
469 d_refinement_lemma_conj
.insert(lem
);
473 void Cegis::registerRefinementLemma(const std::vector
<Node
>& vars
,
475 std::vector
<Node
>& lems
)
477 addRefinementLemma(lem
);
478 // Make the refinement lemma and add it to lems.
479 // This lemma is guarded by the parent's guard, which has the semantics
480 // "this conjecture has a solution", hence this lemma states:
481 // if the parent conjecture has a solution, it satisfies the specification
482 // for the given concrete point.
484 NodeManager::currentNM()->mkNode(OR
, d_parent
->getGuard().negate(), lem
);
485 lems
.push_back(rlem
);
488 bool Cegis::usingRepairConst() { return true; }
489 bool Cegis::getRefinementEvalLemmas(const std::vector
<Node
>& vs
,
490 const std::vector
<Node
>& ms
,
491 std::vector
<Node
>& lems
)
493 Trace("sygus-cref-eval") << "Cref eval : conjecture has "
494 << d_refinement_lemma_unit
.size() << " unit and "
495 << d_refinement_lemma_conj
.size()
496 << " non-unit refinement lemma conjunctions."
498 Assert(vs
.size() == ms
.size());
500 NodeManager
* nm
= NodeManager::currentNM();
502 Node nfalse
= nm
->mkConst(false);
503 Node neg_guard
= d_parent
->getGuard().negate();
506 for (unsigned r
= 0; r
< 2; r
++)
508 std::unordered_set
<Node
, NodeHashFunction
>& rlemmas
=
509 r
== 0 ? d_refinement_lemma_unit
: d_refinement_lemma_conj
;
510 for (const Node
& lem
: rlemmas
)
512 Assert(!lem
.isNull());
513 std::map
<Node
, Node
> visited
;
514 std::map
<Node
, std::vector
<Node
> > exp
;
515 EvalSygusInvarianceTest vsit
;
516 Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lem
517 << " against current model." << std::endl
;
518 Trace("sygus-cref-eval2") << "Check refinement lemma conjunct " << lem
519 << " against current model." << std::endl
;
521 Node lemcs
= lem
.substitute(vs
.begin(), vs
.end(), ms
.begin(), ms
.end());
522 Trace("sygus-cref-eval2")
523 << "...under substitution it is : " << lemcs
<< std::endl
;
524 Node lemcsu
= vsit
.doEvaluateWithUnfolding(d_tds
, lemcs
);
525 Trace("sygus-cref-eval2")
526 << "...after unfolding is : " << lemcsu
<< std::endl
;
527 if (lemcsu
.isConst() && !lemcsu
.getConst
<bool>())
530 std::vector
<Node
> msu
;
531 std::vector
<Node
> mexp
;
532 msu
.insert(msu
.end(), ms
.begin(), ms
.end());
533 std::map
<TypeNode
, int> var_count
;
534 for (unsigned k
= 0; k
< vs
.size(); k
++)
536 vsit
.setUpdatedTerm(msu
[k
]);
538 // substitute for everything except this
540 lem
.substitute(vs
.begin(), vs
.end(), msu
.begin(), msu
.end());
541 vsit
.init(sconj
, vs
[k
], nfalse
);
542 // get minimal explanation for this
543 Node ut
= vsit
.getUpdatedTerm();
544 Trace("sygus-cref-eval2-debug")
545 << " compute min explain of : " << vs
[k
] << " = " << ut
547 d_tds
->getExplain()->getExplanationFor(
548 vs
[k
], ut
, mexp
, vsit
, var_count
, false);
549 Trace("sygus-cref-eval2-debug") << "exp now: " << mexp
<< std::endl
;
550 msu
[k
] = vsit
.getUpdatedTerm();
551 Trace("sygus-cref-eval2-debug")
552 << "updated term : " << msu
[k
] << std::endl
;
556 Node en
= mexp
.size() == 1 ? mexp
[0] : nm
->mkNode(kind::AND
, mexp
);
557 cre_lem
= nm
->mkNode(kind::OR
, en
.negate(), neg_guard
);
563 if (std::find(lems
.begin(), lems
.end(), cre_lem
) == lems
.end())
565 Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem
567 lems
.push_back(cre_lem
);
579 bool Cegis::checkRefinementEvalLemmas(const std::vector
<Node
>& vs
,
580 const std::vector
<Node
>& ms
)
582 // Maybe we already evaluated some terms in refinement lemmas.
583 // In particular, the example eval cache for f may have some evaluations
584 // cached, which we add to evalVisited and pass to the evaluator below.
585 std::unordered_map
<Node
, Node
, NodeHashFunction
> evalVisited
;
586 ExampleInfer
* ei
= d_parent
->getExampleInfer();
587 for (unsigned i
= 0, vsize
= vs
.size(); i
< vsize
; i
++)
590 ExampleEvalCache
* eec
= d_parent
->getExampleEvalCache(f
);
593 // get the results we obtained through the example evaluation utility
594 std::vector
<Node
> vsProc
;
595 std::vector
<Node
> msProc
;
596 Node bmsi
= d_tds
->sygusToBuiltin(ms
[i
]);
597 ei
->getExampleTerms(f
, vsProc
);
598 eec
->evaluateVec(bmsi
, msProc
);
599 Assert(vsProc
.size() == msProc
.size());
600 for (unsigned j
= 0, psize
= vsProc
.size(); j
< psize
; j
++)
602 evalVisited
[vsProc
[j
]] = msProc
[j
];
603 Assert(vsProc
[j
].getType() == msProc
[j
].getType());
608 Evaluator
* eval
= d_tds
->getEvaluator();
609 for (unsigned r
= 0; r
< 2; r
++)
611 std::unordered_set
<Node
, NodeHashFunction
>& rlemmas
=
612 r
== 0 ? d_refinement_lemma_unit
: d_refinement_lemma_conj
;
613 for (const Node
& lem
: rlemmas
)
615 // We may have computed the evaluation of some function applications
616 // via example-based symmetry breaking, stored in evalVisited.
617 Node lemcsu
= eval
->eval(lem
, vs
, ms
, evalVisited
);
618 if (lemcsu
.isConst() && !lemcsu
.getConst
<bool>())
627 bool Cegis::sampleAddRefinementLemma(const std::vector
<Node
>& candidates
,
628 const std::vector
<Node
>& vals
,
629 std::vector
<Node
>& lems
)
631 Trace("cegqi-engine") << " *** Do sample add refinement..." << std::endl
;
632 if (Trace
.isOn("cegis-sample"))
634 Trace("cegis-sample") << "Check sampling for candidate solution"
636 for (unsigned i
= 0, size
= vals
.size(); i
< size
; i
++)
638 Trace("cegis-sample") << " " << candidates
[i
] << " -> " << vals
[i
]
642 Assert(vals
.size() == candidates
.size());
643 Node sbody
= d_base_body
.substitute(
644 candidates
.begin(), candidates
.end(), vals
.begin(), vals
.end());
645 Trace("cegis-sample-debug2") << "Sample " << sbody
<< std::endl
;
646 // do eager rewriting
647 sbody
= Rewriter::rewrite(sbody
);
648 Trace("cegis-sample") << "Sample (after rewriting): " << sbody
<< std::endl
;
650 NodeManager
* nm
= NodeManager::currentNM();
651 for (unsigned i
= 0, size
= d_cegis_sampler
.getNumSamplePoints(); i
< size
;
654 if (d_cegis_sample_refine
.find(i
) == d_cegis_sample_refine
.end())
656 Node ev
= d_cegis_sampler
.evaluate(sbody
, i
);
657 Trace("cegis-sample-debug") << "...evaluate point #" << i
<< " to " << ev
659 Assert(ev
.isConst());
660 Assert(ev
.getType().isBoolean());
661 if (!ev
.getConst
<bool>())
663 Trace("cegis-sample-debug") << "...false for point #" << i
<< std::endl
;
664 // mark this as a CEGIS point (no longer sampled)
665 d_cegis_sample_refine
.insert(i
);
666 std::vector
<Node
> pt
;
667 d_cegis_sampler
.getSamplePoint(i
, pt
);
668 Assert(d_base_vars
.size() == pt
.size());
669 Node rlem
= d_base_body
.substitute(
670 d_base_vars
.begin(), d_base_vars
.end(), pt
.begin(), pt
.end());
671 rlem
= Rewriter::rewrite(rlem
);
673 d_refinement_lemmas
.begin(), d_refinement_lemmas
.end(), rlem
)
674 == d_refinement_lemmas
.end())
676 if (Trace
.isOn("cegis-sample"))
678 Trace("cegis-sample") << " false for point #" << i
<< " : ";
679 for (const Node
& cn
: pt
)
681 Trace("cegis-sample") << cn
<< " ";
683 Trace("cegis-sample") << std::endl
;
685 Trace("cegqi-engine") << " *** Refine by sampling" << std::endl
;
686 addRefinementLemma(rlem
);
687 // if trust, we are not interested in sending out refinement lemmas
688 if (options::cegisSample() != options::CegisSampleMode::TRUST
)
690 Node lem
= nm
->mkNode(OR
, d_parent
->getGuard().negate(), rlem
);
697 Trace("cegis-sample-debug") << "...duplicate." << std::endl
;
705 } /* CVC4::theory::quantifiers namespace */
706 } /* CVC4::theory namespace */
707 } /* CVC4 namespace */