src/theory/quantifiers/inst_strategy_enumerative.cpp

   1 /*********************                                                        */
   2 /*! \file inst_strategy_enumerative.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters
   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 an enumerative instantiation strategy.
  13  **/
  14
  15 #include "theory/quantifiers/inst_strategy_enumerative.h"
  16
  17 #include "options/quantifiers_options.h"
  18 #include "theory/quantifiers/instantiate.h"
  19 #include "theory/quantifiers/relevant_domain.h"
  20 #include "theory/quantifiers/term_database.h"
  21 #include "theory/quantifiers/term_util.h"
  22 #include "theory/quantifiers_engine.h"
  23
  24 namespace CVC4 {
  25
  26 using namespace kind;
  27 using namespace context;
  28
  29 namespace theory {
  30
  31 using namespace inst;
  32
  33 namespace quantifiers {
  34
  35 InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
  36                                    QuantifiersState& qs,
  37                                    QuantifiersInferenceManager& qim,
  38                                    RelevantDomain* rd)
  39     : QuantifiersModule(qs, qim, qe), d_rd(rd), d_fullSaturateLimit(-1)
  40 {
  41 }
  42 void InstStrategyEnum::presolve()
  43 {
  44   d_fullSaturateLimit = options::fullSaturateLimit();
  45 }
  46 bool InstStrategyEnum::needsCheck(Theory::Effort e)
  47 {
  48   if (d_fullSaturateLimit == 0)
  49   {
  50     return false;
  51   }
  52   if (options::fullSaturateInterleave())
  53   {
  54     if (d_quantEngine->getInstWhenNeedsCheck(e))
  55     {
  56       return true;
  57     }
  58   }
  59   if (options::fullSaturateQuant())
  60   {
  61     if (e >= Theory::EFFORT_LAST_CALL)
  62     {
  63       return true;
  64     }
  65   }
  66   return false;
  67 }
  68
  69 void InstStrategyEnum::reset_round(Theory::Effort e) {}
  70 void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
  71 {
  72   bool doCheck = false;
  73   bool fullEffort = false;
  74   if (d_fullSaturateLimit != 0)
  75   {
  76     if (options::fullSaturateInterleave())
  77     {
  78       // we only add when interleaved with other strategies
  79       doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
  80     }
  81     if (options::fullSaturateQuant() && !doCheck)
  82     {
  83       if (!d_quantEngine->theoryEngineNeedsCheck())
  84       {
  85         doCheck = quant_e == QEFFORT_LAST_CALL;
  86         fullEffort = true;
  87       }
  88     }
  89   }
  90   if (!doCheck)
  91   {
  92     return;
  93   }
  94   Assert(!d_quantEngine->inConflict());
  95   double clSet = 0;
  96   if (Trace.isOn("fs-engine"))
  97   {
  98     clSet = double(clock()) / double(CLOCKS_PER_SEC);
  99     Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---"
 100                        << std::endl;
 101   }
 102   unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
 103   unsigned rend = fullEffort ? 1 : rstart;
 104   unsigned addedLemmas = 0;
 105   // First try in relevant domain of all quantified formulas, if no
 106   // instantiations exist, try arbitrary ground terms.
 107   // Notice that this stratification of effort levels makes it so that some
 108   // quantified formulas may not be instantiated (if they have no instances
 109   // at effort level r=0 but another quantified formula does). We prefer
 110   // this stratification since effort level r=1 may be highly expensive in the
 111   // case where we have a quantified formula with many entailed instances.
 112   FirstOrderModel* fm = d_quantEngine->getModel();
 113   unsigned nquant = fm->getNumAssertedQuantifiers();
 114   std::map<Node, bool> alreadyProc;
 115   for (unsigned r = rstart; r <= rend; r++)
 116   {
 117     if (d_rd || r > 0)
 118     {
 119       if (r == 0)
 120       {
 121         Trace("inst-alg") << "-> Relevant domain instantiate..." << std::endl;
 122         Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl;
 123         d_rd->compute();
 124         Trace("inst-alg-debug") << "...finished" << std::endl;
 125       }
 126       else
 127       {
 128         Trace("inst-alg") << "-> Ground term instantiate..." << std::endl;
 129       }
 130       for (unsigned i = 0; i < nquant; i++)
 131       {
 132         Node q = fm->getAssertedQuantifier(i, true);
 133         bool doProcess = d_quantEngine->hasOwnership(q, this)
 134                          && fm->isQuantifierActive(q)
 135                          && alreadyProc.find(q) == alreadyProc.end();
 136         if (doProcess)
 137         {
 138           if (process(q, fullEffort, r == 0))
 139           {
 140             // don't need to mark this if we are not stratifying
 141             if (!options::fullSaturateStratify())
 142             {
 143               alreadyProc[q] = true;
 144             }
 145             // added lemma
 146             addedLemmas++;
 147           }
 148           if (d_quantEngine->inConflict())
 149           {
 150             break;
 151           }
 152         }
 153       }
 154       if (d_quantEngine->inConflict()
 155           || (addedLemmas > 0 && options::fullSaturateStratify()))
 156       {
 157         // we break if we are in conflict, or if we added any lemma at this
 158         // effort level and we stratify effort levels.
 159         break;
 160       }
 161     }
 162   }
 163   if (Trace.isOn("fs-engine"))
 164   {
 165     Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl;
 166     double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
 167     Trace("fs-engine") << "Finished full saturation engine, time = "
 168                        << (clSet2 - clSet) << std::endl;
 169   }
 170   if (d_fullSaturateLimit > 0)
 171   {
 172     d_fullSaturateLimit--;
 173   }
 174 }
 175
 176 bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
 177 {
 178   // ignore if constant true (rare case of non-standard quantifier whose body is
 179   // rewritten to true)
 180   if (f[1].isConst() && f[1].getConst<bool>())
 181   {
 182     return false;
 183   }
 184   unsigned final_max_i = 0;
 185   std::vector<unsigned> maxs;
 186   std::vector<bool> max_zero;
 187   bool has_zero = false;
 188   std::map<TypeNode, std::vector<Node> > term_db_list;
 189   std::vector<TypeNode> ftypes;
 190   TermDb* tdb = d_quantEngine->getTermDatabase();
 191   EqualityQuery* qy = d_quantEngine->getEqualityQuery();
 192   // iterate over substitutions for variables
 193   for (unsigned i = 0; i < f[0].getNumChildren(); i++)
 194   {
 195     TypeNode tn = f[0][i].getType();
 196     ftypes.push_back(tn);
 197     unsigned ts;
 198     if (isRd)
 199     {
 200       ts = d_rd->getRDomain(f, i)->d_terms.size();
 201     }
 202     else
 203     {
 204       ts = tdb->getNumTypeGroundTerms(tn);
 205       std::map<TypeNode, std::vector<Node> >::iterator ittd =
 206           term_db_list.find(tn);
 207       if (ittd == term_db_list.end())
 208       {
 209         std::map<Node, Node> reps_found;
 210         for (unsigned j = 0; j < ts; j++)
 211         {
 212           Node gt = tdb->getTypeGroundTerm(ftypes[i], j);
 213           if (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(gt))
 214           {
 215             Node rep = qy->getRepresentative(gt);
 216             if (reps_found.find(rep) == reps_found.end())
 217             {
 218               reps_found[rep] = gt;
 219               term_db_list[tn].push_back(gt);
 220             }
 221           }
 222         }
 223         ts = term_db_list[tn].size();
 224       }
 225       else
 226       {
 227         ts = ittd->second.size();
 228       }
 229     }
 230     // consider a default value if at full effort
 231     max_zero.push_back(fullEffort && ts == 0);
 232     ts = (fullEffort && ts == 0) ? 1 : ts;
 233     Trace("inst-alg-rd") << "Variable " << i << " has " << ts
 234                          << " in relevant domain." << std::endl;
 235     if (ts == 0)
 236     {
 237       has_zero = true;
 238       break;
 239     }
 240     maxs.push_back(ts);
 241     if (ts > final_max_i)
 242     {
 243       final_max_i = ts;
 244     }
 245   }
 246   if (!has_zero)
 247   {
 248     Trace("inst-alg-rd") << "Will do " << final_max_i
 249                          << " stages of instantiation." << std::endl;
 250     unsigned max_i = 0;
 251     bool success;
 252     Instantiate* ie = d_quantEngine->getInstantiate();
 253     while (max_i <= final_max_i)
 254     {
 255       Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
 256       std::vector<unsigned> childIndex;
 257       int index = 0;
 258       do
 259       {
 260         while (index >= 0 && index < (int)f[0].getNumChildren())
 261         {
 262           if (index == static_cast<int>(childIndex.size()))
 263           {
 264             childIndex.push_back(-1);
 265           }
 266           else
 267           {
 268             Assert(index == static_cast<int>(childIndex.size()) - 1);
 269             unsigned nv = childIndex[index] + 1;
 270             if (nv < maxs[index] && nv <= max_i)
 271             {
 272               childIndex[index] = nv;
 273               index++;
 274             }
 275             else
 276             {
 277               childIndex.pop_back();
 278               index--;
 279             }
 280           }
 281         }
 282         success = index >= 0;
 283         if (success)
 284         {
 285           if (Trace.isOn("inst-alg-rd"))
 286           {
 287             Trace("inst-alg-rd") << "Try instantiation { ";
 288             for (unsigned i : childIndex)
 289             {
 290               Trace("inst-alg-rd") << i << " ";
 291             }
 292             Trace("inst-alg-rd") << "}" << std::endl;
 293           }
 294           // try instantiation
 295           std::vector<Node> terms;
 296           for (unsigned i = 0, nchild = f[0].getNumChildren(); i < nchild; i++)
 297           {
 298             if (max_zero[i])
 299             {
 300               // no terms available, will report incomplete instantiation
 301               terms.push_back(Node::null());
 302               Trace("inst-alg-rd") << "  null" << std::endl;
 303             }
 304             else if (isRd)
 305             {
 306               terms.push_back(d_rd->getRDomain(f, i)->d_terms[childIndex[i]]);
 307               Trace("inst-alg-rd")
 308                   << "  (rd) " << d_rd->getRDomain(f, i)->d_terms[childIndex[i]]
 309                   << std::endl;
 310             }
 311             else
 312             {
 313               Assert(childIndex[i] < term_db_list[ftypes[i]].size());
 314               terms.push_back(term_db_list[ftypes[i]][childIndex[i]]);
 315               Trace("inst-alg-rd")
 316                   << "  " << term_db_list[ftypes[i]][childIndex[i]]
 317                   << std::endl;
 318             }
 319             Assert(terms[i].isNull()
 320                    || terms[i].getType().isComparableTo(ftypes[i]))
 321                 << "Incompatible type " << f << ", " << terms[i].getType()
 322                 << ", " << ftypes[i] << std::endl;
 323           }
 324           if (ie->addInstantiation(f, terms))
 325           {
 326             Trace("inst-alg-rd") << "Success!" << std::endl;
 327             ++(d_quantEngine->d_statistics.d_instantiations_guess);
 328             return true;
 329           }
 330           else
 331           {
 332             index--;
 333           }
 334           if (d_quantEngine->inConflict())
 335           {
 336             // could be conflicting for an internal reason (such as term
 337             // indices computed in above calls)
 338             return false;
 339           }
 340         }
 341       } while (success);
 342       max_i++;
 343     }
 344   }
 345   // TODO : term enumerator instantiation?
 346   return false;
 347 }
 348
 349 } /* CVC4::theory::quantifiers namespace */
 350 } /* CVC4::theory namespace */
 351 } /* CVC4 namespace */