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