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                                    TermRegistry& tr,
  37                                    RelevantDomain* rd)
  38     : QuantifiersModule(qs, qim, qr, tr, qe), d_rd(rd), d_fullSaturateLimit(-1)
  39 {
  40 }
  41 void InstStrategyEnum::presolve()
  42 {
  43   d_fullSaturateLimit = options::fullSaturateLimit();
  44 }
  45 bool InstStrategyEnum::needsCheck(Theory::Effort e)
  46 {
  47   if (d_fullSaturateLimit == 0)
  48   {
  49     return false;
  50   }
  51   if (options::fullSaturateInterleave())
  52   {
  53     // if interleaved, we run at the same time as E-matching
  54     if (d_qstate.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_qim.hasPendingLemma();
  80     }
  81     if (options::fullSaturateQuant() && !doCheck)
  82     {
  83       if (!d_qstate.getValuation().needCheck())
  84       {
  85         doCheck = quant_e == QEFFORT_LAST_CALL;
  86         fullEffort = true;
  87       }
  88     }
  89   }
  90   if (!doCheck)
  91   {
  92     return;
  93   }
  94   Assert(!d_qstate.isInConflict());
  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_qreg.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_qstate.isInConflict())
 149           {
 150             break;
 151           }
 152         }
 153       }
 154       if (d_qstate.isInConflict()
 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 quantifier, bool fullEffort, bool isRd)
 177 {
 178   // ignore if constant true (rare case of non-standard quantifier whose body
 179   // is rewritten to true)
 180   if (quantifier[1].isConst() && quantifier[1].getConst<bool>())
 181   {
 182     return false;
 183   }
 184
 185   TermTupleEnumeratorContext ttec;
 186   ttec.d_quantEngine = d_quantEngine;
 187   ttec.d_rd = d_rd;
 188   ttec.d_fullEffort = fullEffort;
 189   ttec.d_increaseSum = options::fullSaturateSum();
 190   ttec.d_isRd = isRd;
 191   std::unique_ptr<TermTupleEnumeratorInterface> enumerator(
 192       mkTermTupleEnumerator(quantifier, &ttec));
 193   std::vector<Node> terms;
 194   std::vector<bool> failMask;
 195   Instantiate* ie = d_qim.getInstantiate();
 196   for (enumerator->init(); enumerator->hasNext();)
 197   {
 198     if (d_qstate.isInConflict())
 199     {
 200       // could be conflicting for an internal reason
 201       return false;
 202     }
 203     enumerator->next(terms);
 204     // try instantiation
 205     failMask.clear();
 206     /* if (ie->addInstantiation(quantifier, terms)) */
 207     if (ie->addInstantiationExpFail(
 208             quantifier, terms, failMask, InferenceId::QUANTIFIERS_INST_ENUM))
 209     {
 210       Trace("inst-alg-rd") << "Success!" << std::endl;
 211       return true;
 212     }
 213     else
 214     {
 215       enumerator->failureReason(failMask);
 216     }
 217   }
 218   return false;
 219   // TODO : term enumerator instantiation?
 220 }
 221
 222 }  // namespace quantifiers
 223 }  // namespace theory
 224 }  // namespace CVC4