src/theory/quantifiers/sygus/synth_engine.cpp

   1 /*********************                                                        */
   2 /*! \file synth_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 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 "expr/node_algorithm.h"
  19 #include "options/quantifiers_options.h"
  20 #include "theory/quantifiers/quantifiers_attributes.h"
  21 #include "theory/quantifiers/sygus/term_database_sygus.h"
  22 #include "theory/quantifiers/term_util.h"
  23 #include "theory/quantifiers_engine.h"
  24
  25 using namespace CVC4::kind;
  26 using namespace std;
  27
  28 namespace CVC4 {
  29 namespace theory {
  30 namespace quantifiers {
  31
  32 SynthEngine::SynthEngine(QuantifiersEngine* qe,
  33                          QuantifiersState& qs,
  34                          QuantifiersInferenceManager& qim,
  35                          QuantifiersRegistry& qr)
  36     : QuantifiersModule(qs, qim, qr, qe),
  37       d_tds(qe->getTermDatabaseSygus()),
  38       d_conj(nullptr),
  39       d_sqp(qe)
  40 {
  41   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
  42       new SynthConjecture(d_quantEngine, qs, qim, qr, d_statistics)));
  43   d_conj = d_conjs.back().get();
  44 }
  45
  46 SynthEngine::~SynthEngine() {}
  47
  48 void SynthEngine::presolve()
  49 {
  50   Trace("sygus-engine") << "SynthEngine::presolve" << std::endl;
  51   for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
  52   {
  53     d_conjs[i]->presolve();
  54   }
  55   Trace("sygus-engine") << "SynthEngine::presolve finished" << std::endl;
  56 }
  57
  58 bool SynthEngine::needsCheck(Theory::Effort e)
  59 {
  60   return e >= Theory::EFFORT_LAST_CALL;
  61 }
  62
  63 QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)
  64 {
  65   return QEFFORT_MODEL;
  66 }
  67
  68 void SynthEngine::check(Theory::Effort e, QEffort quant_e)
  69 {
  70   // are we at the proper effort level?
  71   if (quant_e != QEFFORT_MODEL)
  72   {
  73     return;
  74   }
  75
  76   // if we are waiting to assign the conjecture, do it now
  77   bool assigned = !d_waiting_conj.empty();
  78   while (!d_waiting_conj.empty())
  79   {
  80     Node q = d_waiting_conj.back();
  81     d_waiting_conj.pop_back();
  82     Trace("sygus-engine") << "--- Conjecture waiting to assign: " << q
  83                           << std::endl;
  84     assignConjecture(q);
  85   }
  86   if (assigned)
  87   {
  88     // assign conjecture always uses the output channel, either by reducing a
  89     // quantified formula to another, or adding initial lemmas during
  90     // SynthConjecture::assign. Thus, we return here and re-check.
  91     return;
  92   }
  93
  94   Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---"
  95                         << std::endl;
  96   Trace("sygus-engine-debug") << std::endl;
  97   Valuation& valuation = d_qstate.getValuation();
  98   std::vector<SynthConjecture*> activeCheckConj;
  99   for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
 100   {
 101     SynthConjecture* sc = d_conjs[i].get();
 102     bool active = false;
 103     bool value;
 104     if (valuation.hasSatValue(sc->getConjecture(), value))
 105     {
 106       active = value;
 107     }
 108     else
 109     {
 110       Trace("sygus-engine-debug") << "...no value for quantified formula."
 111                                   << std::endl;
 112     }
 113     Trace("sygus-engine-debug")
 114         << "Current conjecture status : active : " << active << std::endl;
 115     if (active && sc->needsCheck())
 116     {
 117       activeCheckConj.push_back(sc);
 118     }
 119   }
 120   std::vector<SynthConjecture*> acnext;
 121   do
 122   {
 123     Trace("sygus-engine-debug") << "Checking " << activeCheckConj.size()
 124                                 << " active conjectures..." << std::endl;
 125     for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++)
 126     {
 127       SynthConjecture* sc = activeCheckConj[i];
 128       if (!checkConjecture(sc))
 129       {
 130         if (!sc->needsRefinement())
 131         {
 132           acnext.push_back(sc);
 133         }
 134       }
 135     }
 136     activeCheckConj.clear();
 137     activeCheckConj = acnext;
 138     acnext.clear();
 139   } while (!activeCheckConj.empty() && !d_qstate.getValuation().needCheck());
 140   Trace("sygus-engine")
 141       << "Finished Counterexample Guided Instantiation engine." << std::endl;
 142 }
 143
 144 void SynthEngine::assignConjecture(Node q)
 145 {
 146   Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl;
 147   if (options::sygusQePreproc())
 148   {
 149     Node lem = d_sqp.preprocess(q);
 150     if (!lem.isNull())
 151     {
 152       Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem
 153                            << std::endl;
 154       d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC);
 155       // we've reduced the original to a preprocessed version, return
 156       return;
 157     }
 158   }
 159   // allocate a new synthesis conjecture if not assigned
 160   if (d_conjs.back()->isAssigned())
 161   {
 162     d_conjs.push_back(std::unique_ptr<SynthConjecture>(new SynthConjecture(
 163         d_quantEngine, d_qstate, d_qim, d_qreg, d_statistics)));
 164   }
 165   d_conjs.back()->assign(q);
 166 }
 167
 168 void SynthEngine::checkOwnership(Node q)
 169 {
 170   // take ownership of quantified formulas with sygus attribute, and function
 171   // definitions when options::sygusRecFun is true.
 172   QuantAttributes& qa = d_qreg.getQuantAttributes();
 173   if (qa.isSygus(q) || (options::sygusRecFun() && qa.isFunDef(q)))
 174   {
 175     d_qreg.setOwner(q, this, 2);
 176   }
 177 }
 178
 179 void SynthEngine::registerQuantifier(Node q)
 180 {
 181   Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
 182                        << std::endl;
 183   if (d_qreg.getOwner(q) != this)
 184   {
 185     return;
 186   }
 187   if (d_qreg.getQuantAttributes().isFunDef(q))
 188   {
 189     Assert(options::sygusRecFun());
 190     // If it is a recursive function definition, add it to the function
 191     // definition evaluator class.
 192     Trace("cegqi") << "Registering function definition : " << q << "\n";
 193     FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
 194     fde->assertDefinition(q);
 195     return;
 196   }
 197   Trace("cegqi") << "Register conjecture : " << q << std::endl;
 198   if (options::sygusQePreproc())
 199   {
 200     d_waiting_conj.push_back(q);
 201   }
 202   else
 203   {
 204     // assign it now
 205     assignConjecture(q);
 206   }
 207 }
 208
 209 bool SynthEngine::checkConjecture(SynthConjecture* conj)
 210 {
 211   if (Trace.isOn("sygus-engine-debug"))
 212   {
 213     conj->debugPrint("sygus-engine-debug");
 214     Trace("sygus-engine-debug") << std::endl;
 215   }
 216
 217   if (!conj->needsRefinement())
 218   {
 219     Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
 220     Trace("sygus-engine-debug")
 221         << "  *** Check candidate phase..." << std::endl;
 222     std::vector<Node> cclems;
 223     bool ret = conj->doCheck(cclems);
 224     bool addedLemma = false;
 225     for (const Node& lem : cclems)
 226     {
 227       if (d_qim.addPendingLemma(lem, InferenceId::UNKNOWN))
 228       {
 229         ++(d_statistics.d_cegqi_lemmas_ce);
 230         addedLemma = true;
 231       }
 232       else
 233       {
 234         // this may happen if we eagerly unfold, simplify to true
 235         Trace("sygus-engine-debug")
 236             << "  ...FAILED to add candidate!" << std::endl;
 237       }
 238     }
 239     if (addedLemma)
 240     {
 241       Trace("sygus-engine-debug")
 242           << "  ...check for counterexample." << std::endl;
 243       return true;
 244     }
 245     if (!conj->needsRefinement())
 246     {
 247       return ret;
 248     }
 249     // otherwise, immediately go to refine candidate
 250   }
 251   Trace("sygus-engine-debug") << "  *** Refine candidate phase..." << std::endl;
 252   return conj->doRefine();
 253 }
 254
 255 void SynthEngine::printSynthSolution(std::ostream& out)
 256 {
 257   Assert(!d_conjs.empty());
 258   for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
 259   {
 260     if (d_conjs[i]->isAssigned())
 261     {
 262       d_conjs[i]->printSynthSolution(out);
 263     }
 264   }
 265 }
 266
 267 bool SynthEngine::getSynthSolutions(
 268     std::map<Node, std::map<Node, Node> >& sol_map)
 269 {
 270   bool ret = true;
 271   for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
 272   {
 273     if (d_conjs[i]->isAssigned())
 274     {
 275       if (!d_conjs[i]->getSynthSolutions(sol_map))
 276       {
 277         // if one conjecture fails, we fail overall
 278         ret = false;
 279         break;
 280       }
 281     }
 282   }
 283   return ret;
 284 }
 285
 286 void SynthEngine::preregisterAssertion(Node n)
 287 {
 288   // check if it sygus conjecture
 289   if (QuantAttributes::checkSygusConjecture(n))
 290   {
 291     // this is a sygus conjecture
 292     Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
 293     d_conj->preregisterConjecture(n);
 294   }
 295 }
 296
 297 }  // namespace quantifiers
 298 }  // namespace theory
 299 } /* namespace CVC4 */