src/theory/quantifiers/sygus/cegis.cpp

   1 /*********************                                                        */
   2 /*! \file cegis.cpp
   3  ** \verbatim
   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
  11  **
  12  ** \brief Implementation of cegis
  13  **/
  14
  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"
  25
  26 using namespace std;
  27 using namespace CVC4::kind;
  28 using namespace CVC4::context;
  29
  30 namespace CVC4 {
  31 namespace theory {
  32 namespace quantifiers {
  33
  34 Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p)
  35     : SygusModule(qe, p), d_eval_unfold(nullptr), d_usingSymCons(false)
  36 {
  37   d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold();
  38 }
  39
  40 bool Cegis::initialize(Node conj,
  41                        Node n,
  42                        const std::vector<Node>& candidates,
  43                        std::vector<Node>& lemmas)
  44 {
  45   d_base_body = n;
  46   if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL)
  47   {
  48     for (const Node& v : d_base_body[0][0])
  49     {
  50       d_base_vars.push_back(v);
  51     }
  52     d_base_body = d_base_body[0][1];
  53   }
  54
  55   // assign the cegis sampler if applicable
  56   if (options::cegisSample() != options::CegisSampleMode::NONE)
  57   {
  58     Trace("cegis-sample") << "Initialize sampler for " << d_base_body << "..."
  59                           << std::endl;
  60     TypeNode bt = d_base_body.getType();
  61     d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples());
  62   }
  63   return processInitialize(conj, n, candidates, lemmas);
  64 }
  65
  66 bool Cegis::processInitialize(Node conj,
  67                               Node n,
  68                               const std::vector<Node>& candidates,
  69                               std::vector<Node>& lemmas)
  70 {
  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++)
  79   {
  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)
  86     {
  87       TypeNode ctn = candidates[i].getType();
  88       d_tds->registerSygusType(ctn);
  89       SygusTypeInfo& cti = d_tds->getTypeInfo(ctn);
  90       if (cti.hasSubtermSymbolicCons())
  91       {
  92         // remember that we are using symbolic constructors
  93         d_usingSymCons = true;
  94         Trace("cegis") << " (using symbolic constructors)";
  95       }
  96     }
  97     Trace("cegis") << std::endl;
  98     d_tds->registerEnumerator(candidates[i], candidates[i], d_parent, erole);
  99   }
 100   return true;
 101 }
 102
 103 void Cegis::getTermList(const std::vector<Node>& candidates,
 104                         std::vector<Node>& enums)
 105 {
 106   enums.insert(enums.end(), candidates.begin(), candidates.end());
 107 }
 108
 109 bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
 110                           const std::vector<Node>& candidate_values,
 111                           std::vector<Node>& lems)
 112 {
 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.
 122   bool doGen = true;
 123   for (const Node& v : candidates)
 124   {
 125     // if it is relevant to refinement
 126     if (d_refinement_lemma_vars.find(v) != d_refinement_lemma_vars.end())
 127     {
 128       if (!d_tds->isPassiveEnumerator(v))
 129       {
 130         doGen = false;
 131         break;
 132       }
 133     }
 134   }
 135   NodeManager* nm = NodeManager::currentNM();
 136   bool addedEvalLemmas = false;
 137   // Refinement evaluation should not be done for grammars with symbolic
 138   // constructors.
 139   bool doRefEval = options::sygusRefEval() && !d_usingSymCons;
 140   if (doRefEval)
 141   {
 142     Trace("cegqi-engine") << "  *** Do refinement lemma evaluation"
 143                           << (doGen ? " with conjecture-specific refinement"
 144                                     : "")
 145                           << "..." << std::endl;
 146     // see if any refinement lemma is refuted by evaluation
 147     if (doGen)
 148     {
 149       std::vector<Node> cre_lems;
 150       getRefinementEvalLemmas(candidates, candidate_values, cre_lems);
 151       if (!cre_lems.empty())
 152       {
 153         lems.insert(lems.end(), cre_lems.begin(), cre_lems.end());
 154         addedEvalLemmas = true;
 155         if (Trace.isOn("cegqi-lemma"))
 156         {
 157           for (const Node& lem : cre_lems)
 158           {
 159             Trace("cegqi-lemma")
 160                 << "Cegqi::Lemma : ref evaluation : " << lem << std::endl;
 161           }
 162         }
 163         /* we could, but do not return here. experimentally, it is better to
 164           add the lemmas below as well, in parallel. */
 165       }
 166     }
 167     else
 168     {
 169       // just check whether the refinement lemmas are satisfied, fail if not
 170       if (checkRefinementEvalLemmas(candidates, candidate_values))
 171       {
 172         Trace("cegqi-engine") << "...(actively enumerated) candidate failed "
 173                                  "refinement lemma evaluation."
 174                               << std::endl;
 175         return true;
 176       }
 177     }
 178   }
 179   // we only do evaluation unfolding for passive enumerators
 180   bool doEvalUnfold = (doGen && options::sygusEvalUnfold()) || d_usingSymCons;
 181   if (doEvalUnfold)
 182   {
 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)
 186     {
 187       Trace("cegqi-debug") << "  register " << candidates[i] << " -> "
 188                            << candidate_values[i] << std::endl;
 189       d_eval_unfold->registerModelValue(candidates[i],
 190                                         candidate_values[i],
 191                                         eager_terms,
 192                                         eager_vals,
 193                                         eager_exps);
 194     }
 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)
 198     {
 199       Node lem = nm->mkNode(
 200           OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i]));
 201       lems.push_back(lem);
 202       addedEvalLemmas = true;
 203       Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem
 204                            << std::endl;
 205     }
 206   }
 207   return addedEvalLemmas;
 208 }
 209
 210 Node Cegis::getRefinementLemmaFormula()
 211 {
 212   std::vector<Node> conj;
 213   conj.insert(
 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++)
 217   {
 218     conj.push_back(d_rl_eval_hds[i].eqNode(d_rl_vals[i]));
 219   }
 220   // make the formula
 221   NodeManager* nm = NodeManager::currentNM();
 222   Node ret;
 223   if (conj.empty())
 224   {
 225     ret = nm->mkConst(true);
 226   }
 227   else
 228   {
 229     ret = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj);
 230   }
 231   return ret;
 232 }
 233
 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)
 239 {
 240   if (Trace.isOn("cegis"))
 241   {
 242     Trace("cegis") << "  Enumerators :\n";
 243     for (unsigned i = 0, size = enums.size(); i < size; ++i)
 244     {
 245       Trace("cegis") << "    " << enums[i] << " -> ";
 246       TermDbSygus::toStreamSygus("cegis", enum_values[i]);
 247       Trace("cegis") << "\n";
 248     }
 249   }
 250   // if we are using grammar-based repair
 251   if (d_usingSymCons && options::sygusRepairConst())
 252   {
 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)
 258     {
 259       if (SygusRepairConst::mustRepair(c))
 260       {
 261         mustRepair = true;
 262         break;
 263       }
 264     }
 265     Trace("cegis") << "...must repair is: " << mustRepair << std::endl;
 266     // if the solution contains a subterm that must be repaired
 267     if (mustRepair)
 268     {
 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))
 273       {
 274         return true;
 275       }
 276       Node rl = getRefinementLemmaFormula();
 277       // try to solve for the refinement lemmas only
 278       bool ret =
 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++)
 285       {
 286         d_tds->getExplain()->getExplanationForEquality(
 287             enums[i], enum_values[i], exp);
 288       }
 289       Assert(!exp.empty());
 290       NodeManager* nm = NodeManager::currentNM();
 291       Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
 292       // must guard it
 293       expn = nm->mkNode(OR, d_parent->getGuard().negate(), expn.negate());
 294       lems.push_back(expn);
 295       return ret;
 296     }
 297   }
 298
 299   // evaluate on refinement lemmas
 300   bool addedEvalLemmas = addEvalLemmas(enums, enum_values, lems);
 301
 302   // try to construct candidates
 303   if (!processConstructCandidates(enums,
 304                                   enum_values,
 305                                   candidates,
 306                                   candidate_values,
 307                                   !addedEvalLemmas,
 308                                   lems))
 309   {
 310     return false;
 311   }
 312
 313   if (options::cegisSample() != options::CegisSampleMode::NONE && lems.empty())
 314   {
 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))
 318     {
 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);
 323     }
 324   }
 325   return true;
 326 }
 327
 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,
 332                                        bool satisfiedRl,
 333                                        std::vector<Node>& lems)
 334 {
 335   if (satisfiedRl)
 336   {
 337     candidate_values.insert(
 338         candidate_values.end(), enum_values.begin(), enum_values.end());
 339     return true;
 340   }
 341   return false;
 342 }
 343
 344 void Cegis::addRefinementLemma(Node lem)
 345 {
 346   Trace("cegis-rl") << "Cegis::addRefinementLemma: " << lem << std::endl;
 347   d_refinement_lemmas.push_back(lem);
 348   // apply existing substitution
 349   Node slem = lem;
 350   if (!d_rl_eval_hds.empty())
 351   {
 352     slem = lem.substitute(d_rl_eval_hds.begin(),
 353                           d_rl_eval_hds.end(),
 354                           d_rl_vals.begin(),
 355                           d_rl_vals.end());
 356   }
 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())
 366   {
 367     // add the conjunct, possibly propagating
 368     addRefinementLemmaConjunct(wcounter, waiting);
 369     wcounter++;
 370   }
 371 }
 372
 373 void Cegis::addRefinementLemmaConjunct(unsigned wcounter,
 374                                        std::vector<Node>& waiting)
 375 {
 376   Node lem = waiting[wcounter];
 377   lem = Rewriter::rewrite(lem);
 378   // apply substitution and rewrite if applicable
 379   if (lem.isConst())
 380   {
 381     if (!lem.getConst<bool>())
 382     {
 383       // conjecture is infeasible
 384     }
 385     else
 386     {
 387       return;
 388     }
 389   }
 390   // break into conjunctions
 391   if (lem.getKind() == AND)
 392   {
 393     for (const Node& lc : lem)
 394     {
 395       waiting.push_back(lc);
 396     }
 397     return;
 398   }
 399   // does this correspond to a substitution?
 400   NodeManager* nm = NodeManager::currentNM();
 401   TNode term;
 402   TNode val;
 403   if (lem.getKind() == EQUAL)
 404   {
 405     for (unsigned i = 0; i < 2; i++)
 406     {
 407       if (lem[i].isConst() && d_tds->isEvaluationPoint(lem[1 - i]))
 408       {
 409         term = lem[1 - i];
 410         val = lem[i];
 411         break;
 412       }
 413     }
 414   }
 415   else
 416   {
 417     term = lem.getKind() == NOT ? lem[0] : lem;
 418     // predicate case: the conjunct is a (negated) evaluation point
 419     if (d_tds->isEvaluationPoint(term))
 420     {
 421       val = nm->mkConst(lem.getKind() != NOT);
 422     }
 423   }
 424   if (!val.isNull())
 425   {
 426     if (d_refinement_lemma_unit.find(lem) != d_refinement_lemma_unit.end())
 427     {
 428       // already added
 429       return;
 430     }
 431     Trace("cegis-rl") << "* cegis-rl: propagate: " << term << " -> " << val
 432                       << std::endl;
 433     d_rl_eval_hds.push_back(term);
 434     d_rl_vals.push_back(val);
 435     d_refinement_lemma_unit.insert(lem);
 436
 437     // apply to waiting lemmas beyond this one
 438     for (unsigned i = wcounter + 1, size = waiting.size(); i < size; i++)
 439     {
 440       waiting[i] = waiting[i].substitute(term, val);
 441     }
 442     // apply to all existing refinement lemmas
 443     std::vector<Node> to_rem;
 444     for (const Node& rl : d_refinement_lemma_conj)
 445     {
 446       Node srl = rl.substitute(term, val);
 447       if (srl != rl)
 448       {
 449         Trace("cegis-rl") << "* cegis-rl: replace: " << rl << " -> " << srl
 450                           << std::endl;
 451         waiting.push_back(srl);
 452         to_rem.push_back(rl);
 453       }
 454     }
 455     for (const Node& tr : to_rem)
 456     {
 457       d_refinement_lemma_conj.erase(tr);
 458     }
 459   }
 460   else
 461   {
 462     if (Trace.isOn("cegis-rl"))
 463     {
 464       if (d_refinement_lemma_conj.find(lem) == d_refinement_lemma_conj.end())
 465       {
 466         Trace("cegis-rl") << "cegis-rl: add: " << lem << std::endl;
 467       }
 468     }
 469     d_refinement_lemma_conj.insert(lem);
 470   }
 471 }
 472
 473 void Cegis::registerRefinementLemma(const std::vector<Node>& vars,
 474                                     Node lem,
 475                                     std::vector<Node>& lems)
 476 {
 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.
 483   Node rlem =
 484       NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem);
 485   lems.push_back(rlem);
 486 }
 487
 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)
 492 {
 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."
 497                            << std::endl;
 498   Assert(vs.size() == ms.size());
 499
 500   NodeManager* nm = NodeManager::currentNM();
 501
 502   Node nfalse = nm->mkConst(false);
 503   Node neg_guard = d_parent->getGuard().negate();
 504   bool ret = false;
 505
 506   for (unsigned r = 0; r < 2; r++)
 507   {
 508     std::unordered_set<Node, NodeHashFunction>& rlemmas =
 509         r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj;
 510     for (const Node& lem : rlemmas)
 511     {
 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;
 520       Node cre_lem;
 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>())
 528       {
 529         ret = true;
 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++)
 535         {
 536           vsit.setUpdatedTerm(msu[k]);
 537           msu[k] = vs[k];
 538           // substitute for everything except this
 539           Node sconj =
 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
 546               << std::endl;
 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;
 553         }
 554         if (!mexp.empty())
 555         {
 556           Node en = mexp.size() == 1 ? mexp[0] : nm->mkNode(kind::AND, mexp);
 557           cre_lem = nm->mkNode(kind::OR, en.negate(), neg_guard);
 558         }
 559         else
 560         {
 561           cre_lem = neg_guard;
 562         }
 563         if (std::find(lems.begin(), lems.end(), cre_lem) == lems.end())
 564         {
 565           Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem
 566                                    << std::endl;
 567           lems.push_back(cre_lem);
 568         }
 569       }
 570     }
 571     if (!lems.empty())
 572     {
 573       break;
 574     }
 575   }
 576   return ret;
 577 }
 578
 579 bool Cegis::checkRefinementEvalLemmas(const std::vector<Node>& vs,
 580                                       const std::vector<Node>& ms)
 581 {
 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++)
 588   {
 589     Node f = vs[i];
 590     ExampleEvalCache* eec = d_parent->getExampleEvalCache(f);
 591     if (eec != nullptr)
 592     {
 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++)
 601       {
 602         evalVisited[vsProc[j]] = msProc[j];
 603         Assert(vsProc[j].getType() == msProc[j].getType());
 604       }
 605     }
 606   }
 607
 608   Evaluator* eval = d_tds->getEvaluator();
 609   for (unsigned r = 0; r < 2; r++)
 610   {
 611     std::unordered_set<Node, NodeHashFunction>& rlemmas =
 612         r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj;
 613     for (const Node& lem : rlemmas)
 614     {
 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>())
 619       {
 620         return true;
 621       }
 622     }
 623   }
 624   return false;
 625 }
 626
 627 bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
 628                                      const std::vector<Node>& vals,
 629                                      std::vector<Node>& lems)
 630 {
 631   Trace("cegqi-engine") << "  *** Do sample add refinement..." << std::endl;
 632   if (Trace.isOn("cegis-sample"))
 633   {
 634     Trace("cegis-sample") << "Check sampling for candidate solution"
 635                           << std::endl;
 636     for (unsigned i = 0, size = vals.size(); i < size; i++)
 637     {
 638       Trace("cegis-sample") << "  " << candidates[i] << " -> " << vals[i]
 639                             << std::endl;
 640     }
 641   }
 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;
 649
 650   NodeManager* nm = NodeManager::currentNM();
 651   for (unsigned i = 0, size = d_cegis_sampler.getNumSamplePoints(); i < size;
 652        i++)
 653   {
 654     if (d_cegis_sample_refine.find(i) == d_cegis_sample_refine.end())
 655     {
 656       Node ev = d_cegis_sampler.evaluate(sbody, i);
 657       Trace("cegis-sample-debug") << "...evaluate point #" << i << " to " << ev
 658                                   << std::endl;
 659       Assert(ev.isConst());
 660       Assert(ev.getType().isBoolean());
 661       if (!ev.getConst<bool>())
 662       {
 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);
 672         if (std::find(
 673                 d_refinement_lemmas.begin(), d_refinement_lemmas.end(), rlem)
 674             == d_refinement_lemmas.end())
 675         {
 676           if (Trace.isOn("cegis-sample"))
 677           {
 678             Trace("cegis-sample") << "   false for point #" << i << " : ";
 679             for (const Node& cn : pt)
 680             {
 681               Trace("cegis-sample") << cn << " ";
 682             }
 683             Trace("cegis-sample") << std::endl;
 684           }
 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)
 689           {
 690             Node lem = nm->mkNode(OR, d_parent->getGuard().negate(), rlem);
 691             lems.push_back(lem);
 692           }
 693           return true;
 694         }
 695         else
 696         {
 697           Trace("cegis-sample-debug") << "...duplicate." << std::endl;
 698         }
 699       }
 700     }
 701   }
 702   return false;
 703 }
 704
 705 } /* CVC4::theory::quantifiers namespace */
 706 } /* CVC4::theory namespace */
 707 } /* CVC4 namespace */