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-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 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_tuple_enumerator.h"
  22 #include "theory/quantifiers/term_util.h"
  23 #include "theory/quantifiers_engine.h"
  24
  25 using namespace CVC4::kind;
  26 using namespace CVC4::context;
  27
  28 namespace CVC4 {
  29 namespace theory {
  30 namespace quantifiers {
  31
  32 InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
  33                                    QuantifiersState& qs,
  34                                    QuantifiersInferenceManager& qim,
  35                                    QuantifiersRegistry& qr,
  36                                    RelevantDomain* rd)
  37     : QuantifiersModule(qs, qim, qr, qe), d_rd(rd), d_fullSaturateLimit(-1)
  38 {
  39 }
  40 void InstStrategyEnum::presolve()
  41 {
  42   d_fullSaturateLimit = options::fullSaturateLimit();
  43 }
  44 bool InstStrategyEnum::needsCheck(Theory::Effort e)
  45 {
  46   if (d_fullSaturateLimit == 0)
  47   {
  48     return false;
  49   }
  50   if (options::fullSaturateInterleave())
  51   {
  52     // if interleaved, we run at the same time as E-matching
  53     if (d_qstate.getInstWhenNeedsCheck(e))
  54     {
  55       return true;
  56     }
  57   }
  58   if (options::fullSaturateQuant())
  59   {
  60     if (e >= Theory::EFFORT_LAST_CALL)
  61     {
  62       return true;
  63     }
  64   }
  65   return false;
  66 }
  67
  68 void InstStrategyEnum::reset_round(Theory::Effort e) {}
  69 void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
  70 {
  71   bool doCheck = false;
  72   bool fullEffort = false;
  73   if (d_fullSaturateLimit != 0)
  74   {
  75     if (options::fullSaturateInterleave())
  76     {
  77       // we only add when interleaved with other strategies
  78       doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
  79     }
  80     if (options::fullSaturateQuant() && !doCheck)
  81     {
  82       if (!d_qstate.getValuation().needCheck())
  83       {
  84         doCheck = quant_e == QEFFORT_LAST_CALL;
  85         fullEffort = true;
  86       }
  87     }
  88   }
  89   if (!doCheck)
  90   {
  91     return;
  92   }
  93   Assert(!d_qstate.isInConflict());
  94   double clSet = 0;
  95   if (Trace.isOn("fs-engine"))
  96   {
  97     clSet = double(clock()) / double(CLOCKS_PER_SEC);
  98     Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---"
  99                        << std::endl;
 100   }
 101   unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
 102   unsigned rend = fullEffort ? 1 : rstart;
 103   unsigned addedLemmas = 0;
 104   // First try in relevant domain of all quantified formulas, if no
 105   // instantiations exist, try arbitrary ground terms.
 106   // Notice that this stratification of effort levels makes it so that some
 107   // quantified formulas may not be instantiated (if they have no instances
 108   // at effort level r=0 but another quantified formula does). We prefer
 109   // this stratification since effort level r=1 may be highly expensive in the
 110   // case where we have a quantified formula with many entailed instances.
 111   FirstOrderModel* fm = d_quantEngine->getModel();
 112   unsigned nquant = fm->getNumAssertedQuantifiers();
 113   std::map<Node, bool> alreadyProc;
 114   for (unsigned r = rstart; r <= rend; r++)
 115   {
 116     if (d_rd || r > 0)
 117     {
 118       if (r == 0)
 119       {
 120         Trace("inst-alg") << "-> Relevant domain instantiate..." << std::endl;
 121         Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl;
 122         d_rd->compute();
 123         Trace("inst-alg-debug") << "...finished" << std::endl;
 124       }
 125       else
 126       {
 127         Trace("inst-alg") << "-> Ground term instantiate..." << std::endl;
 128       }
 129       for (unsigned i = 0; i < nquant; i++)
 130       {
 131         Node q = fm->getAssertedQuantifier(i, true);
 132         bool doProcess = d_qreg.hasOwnership(q, this)
 133                          && fm->isQuantifierActive(q)
 134                          && alreadyProc.find(q) == alreadyProc.end();
 135         if (doProcess)
 136         {
 137           if (process(q, fullEffort, r == 0))
 138           {
 139             // don't need to mark this if we are not stratifying
 140             if (!options::fullSaturateStratify())
 141             {
 142               alreadyProc[q] = true;
 143             }
 144             // added lemma
 145             addedLemmas++;
 146           }
 147           if (d_qstate.isInConflict())
 148           {
 149             break;
 150           }
 151         }
 152       }
 153       if (d_qstate.isInConflict()
 154           || (addedLemmas > 0 && options::fullSaturateStratify()))
 155       {
 156         // we break if we are in conflict, or if we added any lemma at this
 157         // effort level and we stratify effort levels.
 158         break;
 159       }
 160     }
 161   }
 162   if (Trace.isOn("fs-engine"))
 163   {
 164     Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl;
 165     double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
 166     Trace("fs-engine") << "Finished full saturation engine, time = "
 167                        << (clSet2 - clSet) << std::endl;
 168   }
 169   if (d_fullSaturateLimit > 0)
 170   {
 171     d_fullSaturateLimit--;
 172   }
 173 }
 174
 175 bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd)
 176 {
 177   // ignore if constant true (rare case of non-standard quantifier whose body
 178   // is rewritten to true)
 179   if (quantifier[1].isConst() && quantifier[1].getConst<bool>())
 180   {
 181     return false;
 182   }
 183
 184   TermTupleEnumeratorContext ttec;
 185   ttec.d_quantEngine = d_quantEngine;
 186   ttec.d_rd = d_rd;
 187   ttec.d_fullEffort = fullEffort;
 188   ttec.d_increaseSum = options::fullSaturateSum();
 189   ttec.d_isRd = isRd;
 190   std::unique_ptr<TermTupleEnumeratorInterface> enumerator(
 191       mkTermTupleEnumerator(quantifier, &ttec));
 192   std::vector<Node> terms;
 193   std::vector<bool> failMask;
 194   Instantiate* ie = d_qim.getInstantiate();
 195   for (enumerator->init(); enumerator->hasNext();)
 196   {
 197     if (d_qstate.isInConflict())
 198     {
 199       // could be conflicting for an internal reason
 200       return false;
 201     }
 202     enumerator->next(terms);
 203     // try instantiation
 204     failMask.clear();
 205     /* if (ie->addInstantiation(quantifier, terms)) */
 206     if (ie->addInstantiationExpFail(
 207             quantifier, terms, failMask, InferenceId::QUANTIFIERS_INST_ENUM))
 208     {
 209       Trace("inst-alg-rd") << "Success!" << std::endl;
 210       return true;
 211     }
 212     else
 213     {
 214       enumerator->failureReason(failMask);
 215     }
 216   }
 217   return false;
 218   // TODO : term enumerator instantiation?
 219 }
 220
 221 }  // namespace quantifiers
 222 }  // namespace theory
 223 }  // namespace CVC4