src/theory/quantifiers/sygus/synth_conjecture.cpp

   1 /*********************                                                        */
   2 /*! \file synth_conjecture.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner, Haniel Barbosa
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 class that encapsulates techniques for a single
  13  ** (SyGuS) synthesis conjecture.
  14  **/
  15 #include "theory/quantifiers/sygus/synth_conjecture.h"
  16
  17 #include "options/base_options.h"
  18 #include "options/datatypes_options.h"
  19 #include "options/quantifiers_options.h"
  20 #include "printer/printer.h"
  21 #include "smt/smt_engine_scope.h"
  22 #include "smt/smt_statistics_registry.h"
  23 #include "theory/datatypes/sygus_datatype_utils.h"
  24 #include "theory/quantifiers/first_order_model.h"
  25 #include "theory/quantifiers/instantiate.h"
  26 #include "theory/quantifiers/quantifiers_attributes.h"
  27 #include "theory/quantifiers/sygus/enum_stream_substitution.h"
  28 #include "theory/quantifiers/sygus/sygus_enumerator.h"
  29 #include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
  30 #include "theory/quantifiers/sygus/synth_engine.h"
  31 #include "theory/quantifiers/sygus/term_database_sygus.h"
  32 #include "theory/quantifiers/term_util.h"
  33 #include "theory/quantifiers_engine.h"
  34 #include "theory/smt_engine_subsolver.h"
  35
  36 using namespace CVC4::kind;
  37 using namespace std;
  38
  39 namespace CVC4 {
  40 namespace theory {
  41 namespace quantifiers {
  42
  43 SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
  44                                  QuantifiersState& qs,
  45                                  QuantifiersInferenceManager& qim,
  46                                  SygusStatistics& s)
  47     : d_qe(qe),
  48       d_qstate(qs),
  49       d_qim(qim),
  50       d_stats(s),
  51       d_tds(qe->getTermDatabaseSygus()),
  52       d_hasSolution(false),
  53       d_ceg_si(new CegSingleInv(qe)),
  54       d_templInfer(new SygusTemplateInfer),
  55       d_ceg_proc(new SynthConjectureProcess(qe)),
  56       d_ceg_gc(new CegGrammarConstructor(qe, this)),
  57       d_sygus_rconst(new SygusRepairConst(qe)),
  58       d_exampleInfer(new ExampleInfer(d_tds)),
  59       d_ceg_pbe(new SygusPbe(qe, this)),
  60       d_ceg_cegis(new Cegis(qe, this)),
  61       d_ceg_cegisUnif(new CegisUnif(qe, qs, this)),
  62       d_sygus_ccore(new CegisCoreConnective(qe, this)),
  63       d_master(nullptr),
  64       d_set_ce_sk_vars(false),
  65       d_repair_index(0),
  66       d_refine_count(0),
  67       d_guarded_stream_exc(false)
  68 {
  69   if (options::sygusSymBreakPbe() || options::sygusUnifPbe())
  70   {
  71     d_modules.push_back(d_ceg_pbe.get());
  72   }
  73   if (options::sygusUnifPi() != options::SygusUnifPiMode::NONE)
  74   {
  75     d_modules.push_back(d_ceg_cegisUnif.get());
  76   }
  77   if (options::sygusCoreConnective())
  78   {
  79     d_modules.push_back(d_sygus_ccore.get());
  80   }
  81   d_modules.push_back(d_ceg_cegis.get());
  82 }
  83
  84 SynthConjecture::~SynthConjecture() {}
  85
  86 void SynthConjecture::presolve()
  87 {
  88   // we don't have a solution yet
  89   d_hasSolution = false;
  90 }
  91
  92 void SynthConjecture::assign(Node q)
  93 {
  94   Assert(d_embed_quant.isNull());
  95   Assert(q.getKind() == FORALL);
  96   Trace("cegqi") << "SynthConjecture : assign : " << q << std::endl;
  97   d_quant = q;
  98   NodeManager* nm = NodeManager::currentNM();
  99
 100   // initialize the guard
 101   d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
 102   d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
 103   d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard);
 104   AlwaysAssert(!d_feasible_guard.isNull());
 105
 106   // pre-simplify the quantified formula based on the process utility
 107   d_simp_quant = d_ceg_proc->preSimplify(d_quant);
 108
 109   // compute its attributes
 110   QAttributes qa;
 111   QuantAttributes::computeQuantAttributes(q, qa);
 112
 113   std::map<Node, Node> templates;
 114   std::map<Node, Node> templates_arg;
 115   // register with single invocation if applicable
 116   if (qa.d_sygus)
 117   {
 118     d_ceg_si->initialize(d_simp_quant);
 119     d_simp_quant = d_ceg_si->getSimplifiedConjecture();
 120     if (!d_ceg_si->isSingleInvocation())
 121     {
 122       d_templInfer->initialize(d_simp_quant);
 123     }
 124     // carry the templates
 125     for (const Node& v : q[0])
 126     {
 127       Node templ = d_templInfer->getTemplate(v);
 128       if (!templ.isNull())
 129       {
 130         templates[v] = templ;
 131         templates_arg[v] = d_templInfer->getTemplateArg(v);
 132       }
 133     }
 134   }
 135
 136   // post-simplify the quantified formula based on the process utility
 137   d_simp_quant = d_ceg_proc->postSimplify(d_simp_quant);
 138
 139   // finished simplifying the quantified formula at this point
 140
 141   // convert to deep embedding and finalize single invocation here
 142   d_embed_quant = d_ceg_gc->process(d_simp_quant, templates, templates_arg);
 143   Trace("cegqi") << "SynthConjecture : converted to embedding : "
 144                  << d_embed_quant << std::endl;
 145
 146   Node sc = qa.d_sygusSideCondition;
 147   if (!sc.isNull())
 148   {
 149     // convert to deep embedding
 150     d_embedSideCondition = d_ceg_gc->convertToEmbedding(sc);
 151     Trace("cegqi") << "SynthConjecture : side condition : "
 152                    << d_embedSideCondition << std::endl;
 153   }
 154
 155   // we now finalize the single invocation module, based on the syntax
 156   // restrictions
 157   if (qa.d_sygus)
 158   {
 159     d_ceg_si->finishInit(d_ceg_gc->isSyntaxRestricted());
 160   }
 161
 162   Assert(d_candidates.empty());
 163   std::vector<Node> vars;
 164   for (unsigned i = 0; i < d_embed_quant[0].getNumChildren(); i++)
 165   {
 166     vars.push_back(d_embed_quant[0][i]);
 167     Node e =
 168         NodeManager::currentNM()->mkSkolem("e", d_embed_quant[0][i].getType());
 169     d_candidates.push_back(e);
 170   }
 171   Trace("cegqi") << "Base quantified formula is : " << d_embed_quant
 172                  << std::endl;
 173   // construct base instantiation
 174   d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation(
 175       d_embed_quant, vars, d_candidates));
 176   if (!d_embedSideCondition.isNull())
 177   {
 178     d_embedSideCondition = d_embedSideCondition.substitute(
 179         vars.begin(), vars.end(), d_candidates.begin(), d_candidates.end());
 180   }
 181   Trace("cegqi") << "Base instantiation is :      " << d_base_inst << std::endl;
 182
 183   // initialize the sygus constant repair utility
 184   if (options::sygusRepairConst())
 185   {
 186     d_sygus_rconst->initialize(d_base_inst.negate(), d_candidates);
 187     if (options::sygusConstRepairAbort())
 188     {
 189       if (!d_sygus_rconst->isActive())
 190       {
 191         // no constant repair is possible: abort
 192         std::stringstream ss;
 193         ss << "Grammar does not allow repair constants." << std::endl;
 194         throw LogicException(ss.str());
 195       }
 196     }
 197   }
 198   // initialize the example inference utility
 199   if (!d_exampleInfer->initialize(d_base_inst, d_candidates))
 200   {
 201     // there is a contradictory example pair, the conjecture is infeasible.
 202     Node infLem = d_feasible_guard.negate();
 203     d_qe->getOutputChannel().lemma(infLem);
 204     // we don't need to continue initialization in this case
 205     return;
 206   }
 207
 208   // register this term with sygus database and other utilities that impact
 209   // the enumerative sygus search
 210   std::vector<Node> guarded_lemmas;
 211   if (!isSingleInvocation())
 212   {
 213     d_ceg_proc->initialize(d_base_inst, d_candidates);
 214     for (unsigned i = 0, size = d_modules.size(); i < size; i++)
 215     {
 216       if (d_modules[i]->initialize(
 217               d_simp_quant, d_base_inst, d_candidates, guarded_lemmas))
 218       {
 219         d_master = d_modules[i];
 220         break;
 221       }
 222     }
 223     Assert(d_master != nullptr);
 224   }
 225
 226   Assert(d_qe->getQuantAttributes()->isSygus(q));
 227   // if the base instantiation is an existential, store its variables
 228   if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL)
 229   {
 230     for (const Node& v : d_base_inst[0][0])
 231     {
 232       d_inner_vars.push_back(v);
 233     }
 234   }
 235
 236   // register the strategy
 237   d_feasible_strategy.reset(
 238       new DecisionStrategySingleton("sygus_feasible",
 239                                     d_feasible_guard,
 240                                     d_qstate.getSatContext(),
 241                                     d_qe->getValuation()));
 242   d_qe->getDecisionManager()->registerStrategy(
 243       DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get());
 244   // this must be called, both to ensure that the feasible guard is
 245   // decided on with true polariy, but also to ensure that output channel
 246   // has been used on this call to check.
 247   d_qe->getOutputChannel().requirePhase(d_feasible_guard, true);
 248
 249   Node gneg = d_feasible_guard.negate();
 250   for (unsigned i = 0; i < guarded_lemmas.size(); i++)
 251   {
 252     Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]);
 253     Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem
 254                          << std::endl;
 255     d_qe->getOutputChannel().lemma(lem);
 256   }
 257
 258   Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation()
 259                  << std::endl;
 260 }
 261
 262 Node SynthConjecture::getGuard() const { return d_feasible_guard; }
 263
 264 bool SynthConjecture::isSingleInvocation() const
 265 {
 266   return d_ceg_si->isSingleInvocation();
 267 }
 268
 269 bool SynthConjecture::needsCheck()
 270 {
 271   bool value;
 272   Assert(!d_feasible_guard.isNull());
 273   // non or fully single invocation : look at guard only
 274   if (d_qe->getValuation().hasSatValue(d_feasible_guard, value))
 275   {
 276     if (!value)
 277     {
 278       Trace("sygus-engine-debug") << "Conjecture is infeasible." << std::endl;
 279       return false;
 280     }
 281     else
 282     {
 283       Trace("sygus-engine-debug") << "Feasible guard " << d_feasible_guard
 284                                   << " assigned true." << std::endl;
 285     }
 286   }
 287   else
 288   {
 289     Trace("cegqi-warn") << "WARNING: Guard " << d_feasible_guard
 290                         << " is not assigned!" << std::endl;
 291     Assert(false);
 292   }
 293   return true;
 294 }
 295
 296 bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
 297 bool SynthConjecture::doCheck(std::vector<Node>& lems)
 298 {
 299   if (isSingleInvocation())
 300   {
 301     // We now try to solve with the single invocation solver, which may or may
 302     // not succeed in solving the conjecture. In either case,  we are done and
 303     // return true.
 304     if (d_ceg_si->solve())
 305     {
 306       d_hasSolution = true;
 307       // the conjecture has a solution, so its negation holds
 308       lems.push_back(d_quant.negate());
 309     }
 310     return true;
 311   }
 312   Assert(d_master != nullptr);
 313   Assert(!d_hasSolution);
 314
 315   // get the list of terms that the master strategy is interested in
 316   std::vector<Node> terms;
 317   d_master->getTermList(d_candidates, terms);
 318
 319   Assert(!d_candidates.empty());
 320
 321   Trace("cegqi-check") << "CegConjuncture : check, build candidates..."
 322                        << std::endl;
 323   std::vector<Node> candidate_values;
 324   bool constructed_cand = false;
 325
 326   // If a module is not trying to repair constants in solutions and the option
 327   // sygusRepairConst  is true, we use a default scheme for trying to repair
 328   // constants here.
 329   bool doRepairConst =
 330       options::sygusRepairConst() && !d_master->usingRepairConst();
 331   if (doRepairConst)
 332   {
 333     // have we tried to repair the previous solution?
 334     // if not, call the repair constant utility
 335     unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size();
 336     if (d_repair_index < ninst)
 337     {
 338       std::vector<Node> fail_cvs;
 339       for (const Node& cprog : d_candidates)
 340       {
 341         Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
 342         fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
 343       }
 344       if (Trace.isOn("sygus-engine"))
 345       {
 346         Trace("sygus-engine") << "CegConjuncture : repair previous solution ";
 347         for (const Node& fc : fail_cvs)
 348         {
 349           std::stringstream ss;
 350           TermDbSygus::toStreamSygus(ss, fc);
 351           Trace("sygus-engine") << ss.str() << " ";
 352         }
 353         Trace("sygus-engine") << std::endl;
 354       }
 355       d_repair_index++;
 356       if (d_sygus_rconst->repairSolution(
 357               d_candidates, fail_cvs, candidate_values, true))
 358       {
 359         constructed_cand = true;
 360       }
 361     }
 362   }
 363
 364   bool printDebug = options::debugSygus();
 365   if (!constructed_cand)
 366   {
 367     // get the model value of the relevant terms from the master module
 368     std::vector<Node> enum_values;
 369     bool activeIncomplete = false;
 370     bool fullModel = getEnumeratedValues(terms, enum_values, activeIncomplete);
 371
 372     // if the master requires a full model and the model is partial, we fail
 373     if (!d_master->allowPartialModel() && !fullModel)
 374     {
 375       // we retain the values in d_ev_active_gen_waiting
 376       Trace("sygus-engine-debug") << "...partial model, fail." << std::endl;
 377       // if we are partial due to an active enumerator, we may still succeed
 378       // on the next call
 379       return !activeIncomplete;
 380     }
 381     // the waiting values are passed to the module below, clear
 382     d_ev_active_gen_waiting.clear();
 383
 384     Assert(terms.size() == enum_values.size());
 385     bool emptyModel = true;
 386     for (unsigned i = 0, size = terms.size(); i < size; i++)
 387     {
 388       if (!enum_values[i].isNull())
 389       {
 390         emptyModel = false;
 391       }
 392     }
 393     if (emptyModel)
 394     {
 395       Trace("sygus-engine-debug") << "...empty model, fail." << std::endl;
 396       return !activeIncomplete;
 397     }
 398     // Must separately compute whether trace is on due to compilation of
 399     // Trace.isOn.
 400     bool traceIsOn = Trace.isOn("sygus-engine");
 401     if (printDebug || traceIsOn)
 402     {
 403       Trace("sygus-engine") << "  * Value is : ";
 404       std::stringstream sygusEnumOut;
 405       for (unsigned i = 0, size = terms.size(); i < size; i++)
 406       {
 407         Node nv = enum_values[i];
 408         Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv;
 409         TypeNode tn = onv.getType();
 410         std::stringstream ss;
 411         TermDbSygus::toStreamSygus(ss, onv);
 412         if (printDebug)
 413         {
 414           sygusEnumOut << " " << ss.str();
 415         }
 416         Trace("sygus-engine") << terms[i] << " -> ";
 417         if (nv.isNull())
 418         {
 419           Trace("sygus-engine") << "[EXC: " << ss.str() << "] ";
 420         }
 421         else
 422         {
 423           Trace("sygus-engine") << ss.str() << " ";
 424           if (Trace.isOn("sygus-engine-rr"))
 425           {
 426             Node bv = d_tds->sygusToBuiltin(nv, tn);
 427             bv = Rewriter::rewrite(bv);
 428             Trace("sygus-engine-rr") << " -> " << bv << std::endl;
 429           }
 430         }
 431       }
 432       Trace("sygus-engine") << std::endl;
 433       if (printDebug)
 434       {
 435         Options& sopts = smt::currentSmtEngine()->getOptions();
 436         std::ostream& out = *sopts.getOut();
 437         out << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
 438       }
 439     }
 440     Assert(candidate_values.empty());
 441     constructed_cand = d_master->constructCandidates(
 442         terms, enum_values, d_candidates, candidate_values, lems);
 443     // now clear the evaluation caches
 444     for (std::pair<const Node, std::unique_ptr<ExampleEvalCache> >& ecp :
 445          d_exampleEvalCache)
 446     {
 447       ExampleEvalCache* eec = ecp.second.get();
 448       if (eec != nullptr)
 449       {
 450         eec->clearEvaluationAll();
 451       }
 452     }
 453   }
 454
 455   NodeManager* nm = NodeManager::currentNM();
 456
 457   // check the side condition if we constructed a candidate
 458   if (constructed_cand)
 459   {
 460     if (!checkSideCondition(candidate_values))
 461     {
 462       excludeCurrentSolution(terms, candidate_values);
 463       Trace("sygus-engine") << "...failed side condition" << std::endl;
 464       return false;
 465     }
 466   }
 467
 468   // must get a counterexample to the value of the current candidate
 469   Node inst;
 470   if (constructed_cand)
 471   {
 472     if (Trace.isOn("cegqi-check"))
 473     {
 474       Trace("cegqi-check") << "CegConjuncture : check candidate : "
 475                            << std::endl;
 476       for (unsigned i = 0, size = candidate_values.size(); i < size; i++)
 477       {
 478         Trace("cegqi-check") << "  " << i << " : " << d_candidates[i] << " -> "
 479                              << candidate_values[i] << std::endl;
 480       }
 481     }
 482     Assert(candidate_values.size() == d_candidates.size());
 483     inst = d_base_inst.substitute(d_candidates.begin(),
 484                                   d_candidates.end(),
 485                                   candidate_values.begin(),
 486                                   candidate_values.end());
 487   }
 488   else
 489   {
 490     inst = d_base_inst;
 491   }
 492
 493   if (!constructed_cand)
 494   {
 495     return false;
 496   }
 497
 498   // if we trust the sampling we ran, we terminate now
 499   if (options::cegisSample() == options::CegisSampleMode::TRUST)
 500   {
 501     // we have that the current candidate passed a sample test
 502     // since we trust sampling in this mode, we assert there is no
 503     // counterexample to the conjecture here.
 504     lems.push_back(d_quant.negate());
 505     recordSolution(candidate_values);
 506     return true;
 507   }
 508   Assert(!d_set_ce_sk_vars);
 509
 510   // immediately skolemize inner existentials
 511   Node query;
 512   // introduce the skolem variables
 513   std::vector<Node> sks;
 514   std::vector<Node> vars;
 515   if (constructed_cand)
 516   {
 517     if (printDebug)
 518     {
 519       Options& sopts = smt::currentSmtEngine()->getOptions();
 520       std::ostream& out = *sopts.getOut();
 521       out << "(sygus-candidate ";
 522       Assert(d_quant[0].getNumChildren() == candidate_values.size());
 523       for (unsigned i = 0, ncands = candidate_values.size(); i < ncands; i++)
 524       {
 525         Node v = candidate_values[i];
 526         std::stringstream ss;
 527         TermDbSygus::toStreamSygus(ss, v);
 528         out << "(" << d_quant[0][i] << " " << ss.str() << ")";
 529       }
 530       out << ")" << std::endl;
 531     }
 532     if (inst.getKind() == NOT && inst[0].getKind() == FORALL)
 533     {
 534       for (const Node& v : inst[0][0])
 535       {
 536         Node sk = nm->mkSkolem("rsk", v.getType());
 537         sks.push_back(sk);
 538         vars.push_back(v);
 539         Trace("cegqi-check-debug")
 540             << "  introduce skolem " << sk << " for " << v << "\n";
 541       }
 542       query = inst[0][1].substitute(
 543           vars.begin(), vars.end(), sks.begin(), sks.end());
 544       query = query.negate();
 545     }
 546     else
 547     {
 548       // use the instance itself
 549       query = inst;
 550     }
 551   }
 552   d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end());
 553   d_set_ce_sk_vars = true;
 554
 555   if (query.isNull())
 556   {
 557     // no lemma to check
 558     return false;
 559   }
 560
 561   // simplify the lemma based on the term database sygus utility
 562   query = d_tds->rewriteNode(query);
 563   // eagerly unfold applications of evaluation function
 564   Trace("cegqi-debug") << "pre-unfold counterexample : " << query << std::endl;
 565   // Record the solution, which may be falsified below. We require recording
 566   // here since the result of the satisfiability test may be unknown.
 567   recordSolution(candidate_values);
 568
 569   if (!query.isConst() || query.getConst<bool>())
 570   {
 571     Trace("sygus-engine") << "  *** Verify with subcall..." << std::endl;
 572     Result r =
 573         checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs);
 574     Trace("sygus-engine") << "  ...got " << r << std::endl;
 575     if (r.asSatisfiabilityResult().isSat() == Result::SAT)
 576     {
 577       if (Trace.isOn("sygus-engine"))
 578       {
 579         Trace("sygus-engine") << "  * Verification lemma failed for:\n   ";
 580         for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++)
 581         {
 582           Trace("sygus-engine")
 583               << d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " ";
 584         }
 585         Trace("sygus-engine") << std::endl;
 586       }
 587       if (Configuration::isAssertionBuild())
 588       {
 589         // the values for the query should be a complete model
 590         Node squery = query.substitute(d_ce_sk_vars.begin(),
 591                                        d_ce_sk_vars.end(),
 592                                        d_ce_sk_var_mvs.begin(),
 593                                        d_ce_sk_var_mvs.end());
 594         Trace("cegqi-debug") << "...squery : " << squery << std::endl;
 595         squery = Rewriter::rewrite(squery);
 596         Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
 597         Assert(options::sygusRecFun()
 598                || (squery.isConst() && squery.getConst<bool>()));
 599       }
 600       return false;
 601     }
 602     else if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
 603     {
 604       // In the rare case that the subcall is unknown, we simply exclude the
 605       // solution, without adding a counterexample point. This should only
 606       // happen if the quantifier free logic is undecidable.
 607       excludeCurrentSolution(terms, candidate_values);
 608       // We should set incomplete, since a "sat" answer should not be
 609       // interpreted as "infeasible", which would make a difference in the rare
 610       // case where e.g. we had a finite grammar and exhausted the grammar.
 611       d_qe->getOutputChannel().setIncomplete();
 612       return false;
 613     }
 614     // otherwise we are unsat, and we will process the solution below
 615   }
 616   // now mark that we have a solution
 617   d_hasSolution = true;
 618   if (options::sygusStream())
 619   {
 620     // immediately print the current solution
 621     printAndContinueStream(terms, candidate_values);
 622     // streaming means now we immediately are looking for a new solution
 623     d_hasSolution = false;
 624     return false;
 625   }
 626   // Use lemma to terminate with "unsat", this is justified by the verification
 627   // check above, which confirms the synthesis conjecture is solved.
 628   lems.push_back(d_quant.negate());
 629   return true;
 630 }
 631
 632 bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const
 633 {
 634   if (!d_embedSideCondition.isNull())
 635   {
 636     Node sc = d_embedSideCondition.substitute(
 637         d_candidates.begin(), d_candidates.end(), cvals.begin(), cvals.end());
 638     Trace("sygus-engine") << "Check side condition..." << std::endl;
 639     Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
 640     Result r = checkWithSubsolver(sc);
 641     Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
 642     if (r == Result::UNSAT)
 643     {
 644       return false;
 645     }
 646     Trace("sygus-engine") << "...passed side condition" << std::endl;
 647   }
 648   return true;
 649 }
 650
 651 bool SynthConjecture::doRefine()
 652 {
 653   std::vector<Node> lems;
 654   Assert(d_set_ce_sk_vars);
 655
 656   // first, make skolem substitution
 657   Trace("cegqi-refine") << "doRefine : construct skolem substitution..."
 658                         << std::endl;
 659   std::vector<Node> sk_vars;
 660   std::vector<Node> sk_subs;
 661   // collect the substitution over all disjuncts
 662   if (!d_ce_sk_vars.empty())
 663   {
 664     Trace("cegqi-refine") << "Get model values for skolems..." << std::endl;
 665     Assert(d_inner_vars.size() == d_ce_sk_vars.size());
 666     if (d_ce_sk_var_mvs.empty())
 667     {
 668       std::vector<Node> model_values;
 669       for (const Node& v : d_ce_sk_vars)
 670       {
 671         Node mv = getModelValue(v);
 672         Trace("cegqi-refine") << "  " << v << " -> " << mv << std::endl;
 673         model_values.push_back(mv);
 674       }
 675       sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end());
 676     }
 677     else
 678     {
 679       Assert(d_ce_sk_var_mvs.size() == d_ce_sk_vars.size());
 680       sk_subs.insert(
 681           sk_subs.end(), d_ce_sk_var_mvs.begin(), d_ce_sk_var_mvs.end());
 682     }
 683     sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end());
 684   }
 685   else
 686   {
 687     Assert(d_inner_vars.empty());
 688   }
 689
 690   std::vector<Node> lem_c;
 691   Trace("cegqi-refine") << "doRefine : Construct refinement lemma..."
 692                         << std::endl;
 693   Trace("cegqi-refine-debug")
 694       << "  For counterexample skolems : " << d_ce_sk_vars << std::endl;
 695   Node base_lem;
 696   if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL)
 697   {
 698     base_lem = d_base_inst[0][1];
 699   }
 700   else
 701   {
 702     base_lem = d_base_inst.negate();
 703   }
 704
 705   Assert(sk_vars.size() == sk_subs.size());
 706
 707   Trace("cegqi-refine") << "doRefine : substitute..." << std::endl;
 708   base_lem = base_lem.substitute(
 709       sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end());
 710   Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl;
 711   base_lem = d_tds->rewriteNode(base_lem);
 712   Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
 713                         << "..." << std::endl;
 714   d_master->registerRefinementLemma(sk_vars, base_lem, lems);
 715   Trace("cegqi-refine") << "doRefine : finished" << std::endl;
 716   d_set_ce_sk_vars = false;
 717   d_ce_sk_vars.clear();
 718   d_ce_sk_var_mvs.clear();
 719
 720   // now send the lemmas
 721   bool addedLemma = false;
 722   for (const Node& lem : lems)
 723   {
 724     Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem
 725                          << std::endl;
 726     bool res = d_qim.addPendingLemma(lem);
 727     if (res)
 728     {
 729       ++(d_stats.d_cegqi_lemmas_refine);
 730       d_refine_count++;
 731       addedLemma = true;
 732     }
 733     else
 734     {
 735       Trace("cegqi-warn") << "  ...FAILED to add refinement!" << std::endl;
 736     }
 737   }
 738   if (addedLemma)
 739   {
 740     Trace("sygus-engine-debug") << "  ...refine candidate." << std::endl;
 741   }
 742   else
 743   {
 744     Trace("sygus-engine-debug") << "  ...(warning) failed to refine candidate, "
 745                                    "manually exclude candidate."
 746                                 << std::endl;
 747     std::vector<Node> cvals;
 748     for (const Node& c : d_candidates)
 749     {
 750       cvals.push_back(d_cinfo[c].d_inst.back());
 751     }
 752     // something went wrong, exclude the current candidate
 753     excludeCurrentSolution(d_candidates, cvals);
 754     // Note this happens when evaluation is incapable of disproving a candidate
 755     // for counterexample point c, but satisfiability checking happened to find
 756     // the the same point c is indeed a true counterexample. It is sound
 757     // to exclude the candidate in this case.
 758   }
 759   return addedLemma;
 760 }
 761
 762 void SynthConjecture::preregisterConjecture(Node q)
 763 {
 764   d_ceg_si->preregisterConjecture(q);
 765 }
 766
 767 bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
 768                                           std::vector<Node>& v,
 769                                           bool& activeIncomplete)
 770 {
 771   std::vector<Node> ncheck = n;
 772   n.clear();
 773   bool ret = true;
 774   for (unsigned i = 0, size = ncheck.size(); i < size; i++)
 775   {
 776     Node e = ncheck[i];
 777     // if it is not active, we return null
 778     Node g = d_tds->getActiveGuardForEnumerator(e);
 779     if (!g.isNull())
 780     {
 781       Node gstatus = d_qe->getValuation().getSatValue(g);
 782       if (gstatus.isNull() || !gstatus.getConst<bool>())
 783       {
 784         Trace("sygus-engine-debug")
 785             << "Enumerator " << e << " is inactive." << std::endl;
 786         continue;
 787       }
 788     }
 789     Node nv = getEnumeratedValue(e, activeIncomplete);
 790     n.push_back(e);
 791     v.push_back(nv);
 792     ret = ret && !nv.isNull();
 793   }
 794   return ret;
 795 }
 796
 797 Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
 798 {
 799   bool isEnum = d_tds->isEnumerator(e);
 800
 801   if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute()))
 802   {
 803     // if the current model value of e was not registered by the datatypes
 804     // sygus solver, or was excluded by symmetry breaking, then it does not
 805     // have a proper model value that we should consider, thus we return null.
 806     Trace("sygus-engine-debug")
 807         << "Enumerator " << e << " does not have proper model value."
 808         << std::endl;
 809     return Node::null();
 810   }
 811
 812   if (!isEnum || d_tds->isPassiveEnumerator(e))
 813   {
 814     return getModelValue(e);
 815   }
 816
 817   // management of actively generated enumerators goes here
 818
 819   // initialize the enumerated value generator for e
 820   std::map<Node, std::unique_ptr<EnumValGenerator> >::iterator iteg =
 821       d_evg.find(e);
 822   if (iteg == d_evg.end())
 823   {
 824     if (d_tds->isVariableAgnosticEnumerator(e))
 825     {
 826       d_evg[e].reset(new EnumStreamConcrete(d_tds));
 827     }
 828     else
 829     {
 830       // Actively-generated enumerators are currently either variable agnostic
 831       // or basic. The auto mode always prefers the optimized enumerator over
 832       // the basic one.
 833       Assert(d_tds->isBasicEnumerator(e));
 834       if (options::sygusActiveGenMode()
 835           == options::SygusActiveGenMode::ENUM_BASIC)
 836       {
 837         d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
 838       }
 839       else
 840       {
 841         Assert(options::sygusActiveGenMode()
 842                    == options::SygusActiveGenMode::ENUM
 843                || options::sygusActiveGenMode()
 844                       == options::SygusActiveGenMode::AUTO);
 845         d_evg[e].reset(new SygusEnumerator(d_tds, this, d_stats));
 846       }
 847     }
 848     Trace("sygus-active-gen")
 849         << "Active-gen: initialize for " << e << std::endl;
 850     d_evg[e]->initialize(e);
 851     d_ev_curr_active_gen[e] = Node::null();
 852     iteg = d_evg.find(e);
 853     Trace("sygus-active-gen-debug") << "...finish" << std::endl;
 854   }
 855   // if we have a waiting value, return it
 856   std::map<Node, Node>::iterator itw = d_ev_active_gen_waiting.find(e);
 857   if (itw != d_ev_active_gen_waiting.end())
 858   {
 859     Trace("sygus-active-gen-debug")
 860         << "Active-gen: return waiting " << itw->second << std::endl;
 861     return itw->second;
 862   }
 863   // Check if there is an (abstract) value absE we were actively generating
 864   // values based on.
 865   Node absE = d_ev_curr_active_gen[e];
 866   bool firstTime = false;
 867   if (absE.isNull())
 868   {
 869     // None currently exist. The next abstract value is the model value for e.
 870     absE = getModelValue(e);
 871     if (Trace.isOn("sygus-active-gen"))
 872     {
 873       Trace("sygus-active-gen") << "Active-gen: new abstract value : ";
 874       TermDbSygus::toStreamSygus("sygus-active-gen", e);
 875       Trace("sygus-active-gen") << " -> ";
 876       TermDbSygus::toStreamSygus("sygus-active-gen", absE);
 877       Trace("sygus-active-gen") << std::endl;
 878     }
 879     d_ev_curr_active_gen[e] = absE;
 880     iteg->second->addValue(absE);
 881     firstTime = true;
 882   }
 883   bool inc = true;
 884   if (!firstTime)
 885   {
 886     inc = iteg->second->increment();
 887   }
 888   Node v;
 889   if (inc)
 890   {
 891     v = iteg->second->getCurrent();
 892   }
 893   Trace("sygus-active-gen-debug") << "...generated " << v
 894                                   << ", with increment success : " << inc
 895                                   << std::endl;
 896   if (!inc)
 897   {
 898     // No more concrete values generated from absE.
 899     NodeManager* nm = NodeManager::currentNM();
 900     d_ev_curr_active_gen[e] = Node::null();
 901     std::vector<Node> exp;
 902     // If we are a basic enumerator, a single abstract value maps to *all*
 903     // concrete values of its type, thus we don't depend on the current
 904     // solution.
 905     if (!d_tds->isBasicEnumerator(e))
 906     {
 907       // We must block e = absE
 908       d_tds->getExplain()->getExplanationForEquality(e, absE, exp);
 909       for (unsigned i = 0, size = exp.size(); i < size; i++)
 910       {
 911         exp[i] = exp[i].negate();
 912       }
 913     }
 914     Node g = d_tds->getActiveGuardForEnumerator(e);
 915     if (!g.isNull())
 916     {
 917       if (d_ev_active_gen_first_val.find(e) == d_ev_active_gen_first_val.end())
 918       {
 919         exp.push_back(g.negate());
 920         d_ev_active_gen_first_val[e] = absE;
 921       }
 922     }
 923     else
 924     {
 925       Assert(false);
 926     }
 927     Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp);
 928     Trace("cegqi-lemma") << "Cegqi::Lemma : actively-generated enumerator "
 929                             "exclude current solution : "
 930                          << lem << std::endl;
 931     if (Trace.isOn("sygus-active-gen-debug"))
 932     {
 933       Trace("sygus-active-gen-debug") << "Active-gen: block ";
 934       TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE);
 935       Trace("sygus-active-gen-debug") << std::endl;
 936     }
 937     d_qe->getOutputChannel().lemma(lem);
 938   }
 939   else
 940   {
 941     // We are waiting to send e -> v to the module that requested it.
 942     if (v.isNull())
 943     {
 944       activeIncomplete = true;
 945     }
 946     else
 947     {
 948       d_ev_active_gen_waiting[e] = v;
 949     }
 950     if (Trace.isOn("sygus-active-gen"))
 951     {
 952       Trace("sygus-active-gen") << "Active-gen : " << e << " : ";
 953       TermDbSygus::toStreamSygus("sygus-active-gen", absE);
 954       Trace("sygus-active-gen") << " -> ";
 955       TermDbSygus::toStreamSygus("sygus-active-gen", v);
 956       Trace("sygus-active-gen") << std::endl;
 957     }
 958   }
 959
 960   return v;
 961 }
 962
 963 Node SynthConjecture::getModelValue(Node n)
 964 {
 965   Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
 966   return d_qe->getModel()->getValue(n);
 967 }
 968
 969 void SynthConjecture::debugPrint(const char* c)
 970 {
 971   Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl;
 972   Trace(c) << "  * Candidate programs : " << d_candidates << std::endl;
 973   Trace(c) << "  * Counterexample skolems : " << d_ce_sk_vars << std::endl;
 974 }
 975
 976 void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
 977                                              const std::vector<Node>& values)
 978 {
 979   Assert(d_master != nullptr);
 980   // we have generated a solution, print it
 981   // get the current output stream
 982   Options& sopts = smt::currentSmtEngine()->getOptions();
 983   printSynthSolution(*sopts.getOut());
 984   excludeCurrentSolution(enums, values);
 985 }
 986
 987 void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& enums,
 988                                              const std::vector<Node>& values)
 989 {
 990   Trace("cegqi-debug") << "Exclude current solution: " << enums << " / "
 991                        << values << std::endl;
 992   // We will not refine the current candidate solution since it is a solution
 993   // thus, we clear information regarding the current refinement
 994   d_set_ce_sk_vars = false;
 995   d_ce_sk_vars.clear();
 996   d_ce_sk_var_mvs.clear();
 997   // However, we need to exclude the current solution using an explicit
 998   // blocking clause, so that we proceed to the next solution. We do this only
 999   // for passively-generated enumerators (TermDbSygus::isPassiveEnumerator).
1000   std::vector<Node> exp;
1001   for (unsigned i = 0, tsize = enums.size(); i < tsize; i++)
1002   {
1003     Node cprog = enums[i];
1004     Assert(d_tds->isEnumerator(cprog));
1005     if (d_tds->isPassiveEnumerator(cprog))
1006     {
1007       Node cval = values[i];
1008       // add to explanation of exclusion
1009       d_tds->getExplain()->getExplanationForEquality(cprog, cval, exp);
1010     }
1011   }
1012   if (!exp.empty())
1013   {
1014     if (!d_guarded_stream_exc)
1015     {
1016       d_guarded_stream_exc = true;
1017       exp.push_back(d_feasible_guard);
1018     }
1019     Node exc_lem = exp.size() == 1
1020                        ? exp[0]
1021                        : NodeManager::currentNM()->mkNode(kind::AND, exp);
1022     exc_lem = exc_lem.negate();
1023     Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : "
1024                          << exc_lem << std::endl;
1025     d_qe->getOutputChannel().lemma(exc_lem);
1026   }
1027 }
1028
1029 void SynthConjecture::printSynthSolution(std::ostream& out)
1030 {
1031   Trace("cegqi-sol-debug") << "Printing synth solution..." << std::endl;
1032   Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren());
1033   std::vector<Node> sols;
1034   std::vector<int> statuses;
1035   if (!getSynthSolutionsInternal(sols, statuses))
1036   {
1037     return;
1038   }
1039   NodeManager* nm = NodeManager::currentNM();
1040   for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
1041   {
1042     Node sol = sols[i];
1043     if (!sol.isNull())
1044     {
1045       Node prog = d_embed_quant[0][i];
1046       int status = statuses[i];
1047       TypeNode tn = prog.getType();
1048       const DType& dt = tn.getDType();
1049       std::stringstream ss;
1050       ss << prog;
1051       std::string f(ss.str());
1052       f.erase(f.begin());
1053       ++(d_stats.d_solutions);
1054
1055       bool is_unique_term = true;
1056
1057       if (status != 0
1058           && (options::sygusRewSynth() || options::sygusQueryGen()
1059               || options::sygusFilterSolMode()
1060                      != options::SygusFilterSolMode::NONE))
1061       {
1062         Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl;
1063         std::map<Node, ExpressionMinerManager>::iterator its =
1064             d_exprm.find(prog);
1065         if (its == d_exprm.end())
1066         {
1067           d_exprm[prog].initializeSygus(
1068               d_qe, d_candidates[i], options::sygusSamples(), true);
1069           if (options::sygusRewSynth())
1070           {
1071             d_exprm[prog].enableRewriteRuleSynth();
1072           }
1073           if (options::sygusQueryGen())
1074           {
1075             d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh());
1076           }
1077           if (options::sygusFilterSolMode()
1078               != options::SygusFilterSolMode::NONE)
1079           {
1080             if (options::sygusFilterSolMode()
1081                 == options::SygusFilterSolMode::STRONG)
1082             {
1083               d_exprm[prog].enableFilterStrongSolutions();
1084             }
1085             else if (options::sygusFilterSolMode()
1086                      == options::SygusFilterSolMode::WEAK)
1087             {
1088               d_exprm[prog].enableFilterWeakSolutions();
1089             }
1090           }
1091           its = d_exprm.find(prog);
1092         }
1093         bool rew_print = false;
1094         is_unique_term = d_exprm[prog].addTerm(sol, out, rew_print);
1095         if (rew_print)
1096         {
1097           ++(d_stats.d_candidate_rewrites_print);
1098         }
1099         if (!is_unique_term)
1100         {
1101           ++(d_stats.d_filtered_solutions);
1102         }
1103       }
1104       if (is_unique_term)
1105       {
1106         out << "(define-fun " << f << " ";
1107         // Only include variables that are truly bound variables of the
1108         // function-to-synthesize. This means we exclude variables that encode
1109         // external terms. This ensures that --sygus-stream prints
1110         // solutions with no arguments on the predicate for responses to
1111         // the get-abduct command.
1112         // pvs stores the variables that will be printed in the argument list
1113         // below.
1114         std::vector<Node> pvs;
1115         Node vl = dt.getSygusVarList();
1116         if (!vl.isNull())
1117         {
1118           Assert(vl.getKind() == BOUND_VAR_LIST);
1119           SygusVarToTermAttribute sta;
1120           for (const Node& v : vl)
1121           {
1122             if (!v.hasAttribute(sta))
1123             {
1124               pvs.push_back(v);
1125             }
1126           }
1127         }
1128         if (pvs.empty())
1129         {
1130           out << "() ";
1131         }
1132         else
1133         {
1134           vl = nm->mkNode(BOUND_VAR_LIST, pvs);
1135           out << vl << " ";
1136         }
1137         out << dt.getSygusType() << " ";
1138         if (status == 0)
1139         {
1140           out << sol;
1141         }
1142         else
1143         {
1144           Node bsol = datatypes::utils::sygusToBuiltin(sol, true);
1145           out << bsol;
1146         }
1147         out << ")" << std::endl;
1148       }
1149     }
1150   }
1151 }
1152
1153 bool SynthConjecture::getSynthSolutions(
1154     std::map<Node, std::map<Node, Node> >& sol_map)
1155 {
1156   NodeManager* nm = NodeManager::currentNM();
1157   std::vector<Node> sols;
1158   std::vector<int> statuses;
1159   Trace("cegqi-debug") << "getSynthSolutions..." << std::endl;
1160   if (!getSynthSolutionsInternal(sols, statuses))
1161   {
1162     Trace("cegqi-debug") << "...failed internal" << std::endl;
1163     return false;
1164   }
1165   // we add it to the solution map, indexed by this conjecture
1166   std::map<Node, Node>& smc = sol_map[d_quant];
1167   for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
1168   {
1169     Node sol = sols[i];
1170     int status = statuses[i];
1171     Trace("cegqi-debug") << "...got " << i << ": " << sol
1172                          << ", status=" << status << std::endl;
1173     // get the builtin solution
1174     Node bsol = sol;
1175     if (status != 0)
1176     {
1177       // Convert sygus to builtin here.
1178       // We must use the external representation to ensure bsol matches the
1179       // grammar.
1180       bsol = datatypes::utils::sygusToBuiltin(sol, true);
1181     }
1182     // convert to lambda
1183     TypeNode tn = d_embed_quant[0][i].getType();
1184     const DType& dt = tn.getDType();
1185     Node fvar = d_quant[0][i];
1186     Node bvl = dt.getSygusVarList();
1187     if (!bvl.isNull())
1188     {
1189       // since we don't have function subtyping, this assertion should only
1190       // check the return type
1191       Assert(fvar.getType().isFunction());
1192       Assert(fvar.getType().getRangeType().isComparableTo(bsol.getType()));
1193       bsol = nm->mkNode(LAMBDA, bvl, bsol);
1194     }
1195     else
1196     {
1197       Assert(fvar.getType().isComparableTo(bsol.getType()));
1198     }
1199     // store in map
1200     smc[fvar] = bsol;
1201     Trace("cegqi-debug") << "...return " << bsol << std::endl;
1202   }
1203   return true;
1204 }
1205
1206 void SynthConjecture::recordSolution(std::vector<Node>& vs)
1207 {
1208   Assert(vs.size() == d_candidates.size());
1209   d_cinfo.clear();
1210   for (unsigned i = 0; i < vs.size(); i++)
1211   {
1212     d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]);
1213   }
1214 }
1215
1216 bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
1217                                                 std::vector<int>& statuses)
1218 {
1219   if (!d_hasSolution)
1220   {
1221     return false;
1222   }
1223   for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
1224   {
1225     Node prog = d_embed_quant[0][i];
1226     Trace("cegqi-debug") << "  get solution for " << prog << std::endl;
1227     TypeNode tn = prog.getType();
1228     Assert(tn.isDatatype());
1229     // get the solution
1230     Node sol;
1231     int status = -1;
1232     if (isSingleInvocation())
1233     {
1234       Assert(d_ceg_si != NULL);
1235       sol = d_ceg_si->getSolution(i, tn, status, true);
1236       if (sol.isNull())
1237       {
1238         return false;
1239       }
1240       sol = sol.getKind() == LAMBDA ? sol[1] : sol;
1241     }
1242     else
1243     {
1244       Node cprog = d_candidates[i];
1245       if (!d_cinfo[cprog].d_inst.empty())
1246       {
1247         // the solution is just the last instantiated term
1248         sol = d_cinfo[cprog].d_inst.back();
1249         status = 1;
1250
1251         // check if there was a template
1252         Node sf = d_quant[0][i];
1253         Node templ = d_templInfer->getTemplate(sf);
1254         if (!templ.isNull())
1255         {
1256           Trace("cegqi-inv-debug")
1257               << sf << " used template : " << templ << std::endl;
1258           // if it was not embedded into the grammar
1259           if (!options::sygusTemplEmbedGrammar())
1260           {
1261             TNode templa = d_templInfer->getTemplateArg(sf);
1262             // make the builtin version of the full solution
1263             sol = d_tds->sygusToBuiltin(sol, sol.getType());
1264             Trace("cegqi-inv") << "Builtin version of solution is : " << sol
1265                                << ", type : " << sol.getType() << std::endl;
1266             TNode tsol = sol;
1267             sol = templ.substitute(templa, tsol);
1268             Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
1269             sol = Rewriter::rewrite(sol);
1270             Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
1271             // now, reconstruct to the syntax
1272             sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true);
1273             sol = sol.getKind() == LAMBDA ? sol[1] : sol;
1274             Trace("cegqi-inv-debug")
1275                 << "Reconstructed to syntax : " << sol << std::endl;
1276           }
1277           else
1278           {
1279             Trace("cegqi-inv-debug")
1280                 << "...was embedding into grammar." << std::endl;
1281           }
1282         }
1283         else
1284         {
1285           Trace("cegqi-inv-debug")
1286               << sf << " did not use template" << std::endl;
1287         }
1288       }
1289       else
1290       {
1291         Trace("cegqi-warn") << "WARNING : No recorded instantiations for "
1292                                "syntax-guided solution!"
1293                             << std::endl;
1294       }
1295     }
1296     sols.push_back(sol);
1297     statuses.push_back(status);
1298   }
1299   return true;
1300 }
1301
1302 Node SynthConjecture::getSymmetryBreakingPredicate(
1303     Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
1304 {
1305   std::vector<Node> sb_lemmas;
1306
1307   // based on simple preprocessing
1308   Node ppred =
1309       d_ceg_proc->getSymmetryBreakingPredicate(x, e, tn, tindex, depth);
1310   if (!ppred.isNull())
1311   {
1312     sb_lemmas.push_back(ppred);
1313   }
1314
1315   // other static conjecture-dependent symmetry breaking goes here
1316
1317   if (!sb_lemmas.empty())
1318   {
1319     return sb_lemmas.size() == 1
1320                ? sb_lemmas[0]
1321                : NodeManager::currentNM()->mkNode(kind::AND, sb_lemmas);
1322   }
1323   else
1324   {
1325     return Node::null();
1326   }
1327 }
1328
1329 ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e)
1330 {
1331   std::map<Node, std::unique_ptr<ExampleEvalCache> >::iterator it =
1332       d_exampleEvalCache.find(e);
1333   if (it != d_exampleEvalCache.end())
1334   {
1335     return it->second.get();
1336   }
1337   Node f = d_tds->getSynthFunForEnumerator(e);
1338   // if f does not have examples, we don't construct the utility
1339   if (!d_exampleInfer->hasExamples(f) || d_exampleInfer->getNumExamples(f) == 0)
1340   {
1341     d_exampleEvalCache[e].reset(nullptr);
1342     return nullptr;
1343   }
1344   d_exampleEvalCache[e].reset(new ExampleEvalCache(d_tds, this, f, e));
1345   return d_exampleEvalCache[e].get();
1346 }
1347
1348 }  // namespace quantifiers
1349 }  // namespace theory
1350 } /* namespace CVC4 */