1 /********************* */
2 /*! \file synth_engine.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King, 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 Implementation of the quantifiers module for managing all approaches
13 ** to synthesis, in particular, those described in Reynolds et al CAV 2015.
14 **
15 **/
16 #include "theory/quantifiers/sygus/synth_engine.h"
17
18 #include "options/quantifiers_options.h"
19 #include "smt/smt_engine.h"
20 #include "smt/smt_engine_scope.h"
21 #include "smt/smt_statistics_registry.h"
22 #include "theory/quantifiers/quantifiers_attributes.h"
23 #include "theory/quantifiers/sygus/term_database_sygus.h"
24 #include "theory/quantifiers/term_util.h"
25 #include "theory/theory_engine.h"
26
27 using namespace CVC4::kind;
28 using namespace std;
29
30 namespace CVC4 {
31 namespace theory {
32 namespace quantifiers {
33
SynthEngine(QuantifiersEngine * qe,context::Context * c)34 SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
35 : QuantifiersModule(qe)
36 {
37 d_conjs.push_back(
38 std::unique_ptr<SynthConjecture>(new SynthConjecture(d_quantEngine)));
39 d_conj = d_conjs.back().get();
40 }
41
~SynthEngine()42 SynthEngine::~SynthEngine() {}
needsCheck(Theory::Effort e)43 bool SynthEngine::needsCheck(Theory::Effort e)
44 {
45 return e >= Theory::EFFORT_LAST_CALL;
46 }
47
needsModel(Theory::Effort e)48 QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)
49 {
50 return QEFFORT_MODEL;
51 }
52
check(Theory::Effort e,QEffort quant_e)53 void SynthEngine::check(Theory::Effort e, QEffort quant_e)
54 {
55 // are we at the proper effort level?
56 if (quant_e != QEFFORT_MODEL)
57 {
58 return;
59 }
60
61 // if we are waiting to assign the conjecture, do it now
62 bool assigned = !d_waiting_conj.empty();
63 while (!d_waiting_conj.empty())
64 {
65 Node q = d_waiting_conj.back();
66 d_waiting_conj.pop_back();
67 Trace("cegqi-engine") << "--- Conjecture waiting to assign: " << q
68 << std::endl;
69 assignConjecture(q);
70 }
71 if (assigned)
72 {
73 // assign conjecture always uses the output channel, either by reducing a
74 // quantified formula to another, or adding initial lemmas during
75 // SynthConjecture::assign. Thus, we return here and re-check.
76 return;
77 }
78
79 Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---"
80 << std::endl;
81 Trace("cegqi-engine-debug") << std::endl;
82 Valuation& valuation = d_quantEngine->getValuation();
83 std::vector<SynthConjecture*> activeCheckConj;
84 for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
85 {
86 SynthConjecture* sc = d_conjs[i].get();
87 bool active = false;
88 bool value;
89 if (valuation.hasSatValue(sc->getConjecture(), value))
90 {
91 active = value;
92 }
93 else
94 {
95 Trace("cegqi-engine-debug") << "...no value for quantified formula."
96 << std::endl;
97 }
98 Trace("cegqi-engine-debug")
99 << "Current conjecture status : active : " << active << std::endl;
100 if (active && sc->needsCheck())
101 {
102 activeCheckConj.push_back(sc);
103 }
104 }
105 std::vector<SynthConjecture*> acnext;
106 do
107 {
108 Trace("cegqi-engine-debug") << "Checking " << activeCheckConj.size()
109 << " active conjectures..." << std::endl;
110 for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++)
111 {
112 SynthConjecture* sc = activeCheckConj[i];
113 if (!checkConjecture(sc))
114 {
115 if (!sc->needsRefinement())
116 {
117 acnext.push_back(sc);
118 }
119 }
120 }
121 activeCheckConj.clear();
122 activeCheckConj = acnext;
123 acnext.clear();
124 } while (!activeCheckConj.empty()
125 && !d_quantEngine->getTheoryEngine()->needCheck());
126 Trace("cegqi-engine")
127 << "Finished Counterexample Guided Instantiation engine." << std::endl;
128 }
129
assignConjecture(Node q)130 void SynthEngine::assignConjecture(Node q)
131 {
132 Trace("cegqi-engine") << "--- Assign conjecture " << q << std::endl;
133 if (options::sygusQePreproc())
134 {
135 // the following does quantifier elimination as a preprocess step
136 // for "non-ground single invocation synthesis conjectures":
137 // exists f. forall xy. P[ f(x), x, y ]
138 // We run quantifier elimination:
139 // exists y. P[ z, x, y ] ----> Q[ z, x ]
140 // Where we replace the original conjecture with:
141 // exists f. forall x. Q[ f(x), x ]
142 // For more details, see Example 6 of Reynolds et al. SYNT 2017.
143 Node body = q[1];
144 if (body.getKind() == NOT && body[0].getKind() == FORALL)
145 {
146 body = body[0][1];
147 }
148 NodeManager* nm = NodeManager::currentNM();
149 Trace("cegqi-qep") << "Compute single invocation for " << q << "..."
150 << std::endl;
151 quantifiers::SingleInvocationPartition sip;
152 std::vector<Node> funcs;
153 funcs.insert(funcs.end(), q[0].begin(), q[0].end());
154 sip.init(funcs, body);
155 Trace("cegqi-qep") << "...finished, got:" << std::endl;
156 sip.debugPrint("cegqi-qep");
157
158 if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
159 {
160 // create new smt engine to do quantifier elimination
161 SmtEngine smt_qe(nm->toExprManager());
162 smt_qe.setIsInternalSubsolver();
163 smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo());
164 Trace("cegqi-qep") << "Property is non-ground single invocation, run "
165 "QE to obtain single invocation."
166 << std::endl;
167 // partition variables
168 std::vector<Node> all_vars;
169 sip.getAllVariables(all_vars);
170 std::vector<Node> si_vars;
171 sip.getSingleInvocationVariables(si_vars);
172 std::vector<Node> qe_vars;
173 std::vector<Node> nqe_vars;
174 for (unsigned i = 0, size = all_vars.size(); i < size; i++)
175 {
176 Node v = all_vars[i];
177 if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end())
178 {
179 qe_vars.push_back(v);
180 }
181 else
182 {
183 nqe_vars.push_back(v);
184 }
185 }
186 std::vector<Node> orig;
187 std::vector<Node> subs;
188 // skolemize non-qe variables
189 for (unsigned i = 0, size = nqe_vars.size(); i < size; i++)
190 {
191 Node k = nm->mkSkolem(
192 "k", nqe_vars[i].getType(), "qe for non-ground single invocation");
193 orig.push_back(nqe_vars[i]);
194 subs.push_back(k);
195 Trace("cegqi-qep") << " subs : " << nqe_vars[i] << " -> " << k
196 << std::endl;
197 }
198 std::vector<Node> funcs;
199 sip.getFunctions(funcs);
200 for (unsigned i = 0, size = funcs.size(); i < size; i++)
201 {
202 Node f = funcs[i];
203 Node fi = sip.getFunctionInvocationFor(f);
204 Node fv = sip.getFirstOrderVariableForFunction(f);
205 Assert(!fi.isNull());
206 orig.push_back(fi);
207 Node k =
208 nm->mkSkolem("k",
209 fv.getType(),
210 "qe for function in non-ground single invocation");
211 subs.push_back(k);
212 Trace("cegqi-qep") << " subs : " << fi << " -> " << k << std::endl;
213 }
214 Node conj_se_ngsi = sip.getFullSpecification();
215 Trace("cegqi-qep") << "Full specification is " << conj_se_ngsi
216 << std::endl;
217 Node conj_se_ngsi_subs = conj_se_ngsi.substitute(
218 orig.begin(), orig.end(), subs.begin(), subs.end());
219 Assert(!qe_vars.empty());
220 conj_se_ngsi_subs = nm->mkNode(EXISTS,
221 nm->mkNode(BOUND_VAR_LIST, qe_vars),
222 conj_se_ngsi_subs.negate());
223
224 Trace("cegqi-qep") << "Run quantifier elimination on "
225 << conj_se_ngsi_subs << std::endl;
226 Expr qe_res = smt_qe.doQuantifierElimination(
227 conj_se_ngsi_subs.toExpr(), true, false);
228 Trace("cegqi-qep") << "Result : " << qe_res << std::endl;
229
230 // create single invocation conjecture
231 Node qe_res_n = Node::fromExpr(qe_res);
232 qe_res_n = qe_res_n.substitute(
233 subs.begin(), subs.end(), orig.begin(), orig.end());
234 if (!nqe_vars.empty())
235 {
236 qe_res_n =
237 nm->mkNode(EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qe_res_n);
238 }
239 Assert(q.getNumChildren() == 3);
240 qe_res_n = nm->mkNode(FORALL, q[0], qe_res_n, q[2]);
241 Trace("cegqi-qep") << "Converted conjecture after QE : " << qe_res_n
242 << std::endl;
243 qe_res_n = Rewriter::rewrite(qe_res_n);
244 Node nq = qe_res_n;
245 // must assert it is equivalent to the original
246 Node lem = q.eqNode(nq);
247 Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem
248 << std::endl;
249 d_quantEngine->getOutputChannel().lemma(lem);
250 // we've reduced the original to a preprocessed version, return
251 return;
252 }
253 }
254 // allocate a new synthesis conjecture if not assigned
255 if (d_conjs.back()->isAssigned())
256 {
257 d_conjs.push_back(
258 std::unique_ptr<SynthConjecture>(new SynthConjecture(d_quantEngine)));
259 }
260 d_conjs.back()->assign(q);
261 }
262
registerQuantifier(Node q)263 void SynthEngine::registerQuantifier(Node q)
264 {
265 if (d_quantEngine->getOwner(q) == this)
266 {
267 Trace("cegqi") << "Register conjecture : " << q << std::endl;
268 if (options::sygusQePreproc())
269 {
270 d_waiting_conj.push_back(q);
271 }
272 else
273 {
274 // assign it now
275 assignConjecture(q);
276 }
277 }
278 else
279 {
280 Trace("cegqi-debug") << "Register quantifier : " << q << std::endl;
281 }
282 }
283
checkConjecture(SynthConjecture * conj)284 bool SynthEngine::checkConjecture(SynthConjecture* conj)
285 {
286 Node q = conj->getEmbeddedConjecture();
287 Node aq = conj->getConjecture();
288 if (Trace.isOn("cegqi-engine-debug"))
289 {
290 conj->debugPrint("cegqi-engine-debug");
291 Trace("cegqi-engine-debug") << std::endl;
292 }
293
294 if (!conj->needsRefinement())
295 {
296 Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl;
297 if (conj->isSingleInvocation())
298 {
299 std::vector<Node> clems;
300 conj->doSingleInvCheck(clems);
301 if (!clems.empty())
302 {
303 for (const Node& lem : clems)
304 {
305 Trace("cegqi-lemma")
306 << "Cegqi::Lemma : single invocation instantiation : " << lem
307 << std::endl;
308 d_quantEngine->addLemma(lem);
309 }
310 d_statistics.d_cegqi_si_lemmas += clems.size();
311 Trace("cegqi-engine") << " ...try single invocation." << std::endl;
312 }
313 else
314 {
315 // This can happen for non-monotonic instantiation strategies. We
316 // set --cbqi-full to ensure that for most strategies (e.g. BV), we
317 // are using a monotonic strategy.
318 Trace("cegqi-warn")
319 << " ...FAILED to add cbqi instantiation for single invocation!"
320 << std::endl;
321 }
322 return true;
323 }
324
325 Trace("cegqi-engine-debug")
326 << " *** Check candidate phase..." << std::endl;
327 std::vector<Node> cclems;
328 bool ret = conj->doCheck(cclems);
329 bool addedLemma = false;
330 for (const Node& lem : cclems)
331 {
332 Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem
333 << std::endl;
334 if (d_quantEngine->addLemma(lem))
335 {
336 ++(d_statistics.d_cegqi_lemmas_ce);
337 addedLemma = true;
338 }
339 else
340 {
341 // this may happen if we eagerly unfold, simplify to true
342 Trace("cegqi-engine-debug")
343 << " ...FAILED to add candidate!" << std::endl;
344 }
345 }
346 if (addedLemma)
347 {
348 Trace("cegqi-engine-debug")
349 << " ...check for counterexample." << std::endl;
350 return true;
351 }
352 else
353 {
354 if (conj->needsRefinement())
355 {
356 // immediately go to refine candidate
357 return checkConjecture(conj);
358 }
359 }
360 return ret;
361 }
362 else
363 {
364 Trace("cegqi-engine-debug")
365 << " *** Refine candidate phase..." << std::endl;
366 std::vector<Node> rlems;
367 conj->doRefine(rlems);
368 bool addedLemma = false;
369 for (unsigned i = 0; i < rlems.size(); i++)
370 {
371 Node lem = rlems[i];
372 Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem
373 << std::endl;
374 bool res = d_quantEngine->addLemma(lem);
375 if (res)
376 {
377 ++(d_statistics.d_cegqi_lemmas_refine);
378 conj->incrementRefineCount();
379 addedLemma = true;
380 }
381 else
382 {
383 Trace("cegqi-warn") << " ...FAILED to add refinement!" << std::endl;
384 }
385 }
386 if (addedLemma)
387 {
388 Trace("cegqi-engine-debug") << " ...refine candidate." << std::endl;
389 }
390 }
391 return true;
392 }
393
printSynthSolution(std::ostream & out)394 void SynthEngine::printSynthSolution(std::ostream& out)
395 {
396 Assert(!d_conjs.empty());
397 for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
398 {
399 if (d_conjs[i]->isAssigned())
400 {
401 d_conjs[i]->printSynthSolution(out);
402 }
403 }
404 }
405
getSynthSolutions(std::map<Node,Node> & sol_map)406 void SynthEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
407 {
408 for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
409 {
410 if (d_conjs[i]->isAssigned())
411 {
412 d_conjs[i]->getSynthSolutions(sol_map);
413 }
414 }
415 }
416
preregisterAssertion(Node n)417 void SynthEngine::preregisterAssertion(Node n)
418 {
419 // check if it sygus conjecture
420 if (QuantAttributes::checkSygusConjecture(n))
421 {
422 // this is a sygus conjecture
423 Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
424 d_conj->preregisterConjecture(n);
425 }
426 }
427
Statistics()428 SynthEngine::Statistics::Statistics()
429 : d_cegqi_lemmas_ce("SynthEngine::cegqi_lemmas_ce", 0),
430 d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0),
431 d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0),
432 d_solutions("SynthConjecture::solutions", 0),
433 d_filtered_solutions("SynthConjecture::filtered_solutions", 0),
434 d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", 0)
435
436 {
437 smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce);
438 smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine);
439 smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas);
440 smtStatisticsRegistry()->registerStat(&d_solutions);
441 smtStatisticsRegistry()->registerStat(&d_filtered_solutions);
442 smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print);
443 }
444
~Statistics()445 SynthEngine::Statistics::~Statistics()
446 {
447 smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce);
448 smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine);
449 smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas);
450 smtStatisticsRegistry()->unregisterStat(&d_solutions);
451 smtStatisticsRegistry()->unregisterStat(&d_filtered_solutions);
452 smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print);
453 }
454
455 } // namespace quantifiers
456 } // namespace theory
457 } /* namespace CVC4 */
458