src/theory/quantifiers/ematching/instantiation_engine.cpp

   1 /*********************                                                        */
   2 /*! \file instantiation_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   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 instantiation engine class
  13  **/
  14
  15 #include "theory/quantifiers/ematching/instantiation_engine.h"
  16
  17 #include "options/quantifiers_options.h"
  18 #include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
  19 #include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
  20 #include "theory/quantifiers/ematching/trigger.h"
  21 #include "theory/quantifiers/first_order_model.h"
  22 #include "theory/quantifiers/quantifiers_attributes.h"
  23 #include "theory/quantifiers/term_database.h"
  24 #include "theory/quantifiers/term_util.h"
  25 #include "theory/quantifiers_engine.h"
  26
  27 using namespace std;
  28 using namespace CVC4::kind;
  29 using namespace CVC4::context;
  30 using namespace CVC4::theory::inst;
  31
  32 namespace CVC4 {
  33 namespace theory {
  34 namespace quantifiers {
  35
  36 InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
  37                                          QuantifiersState& qs,
  38                                          QuantifiersInferenceManager& qim,
  39                                          QuantifiersRegistry& qr)
  40     : QuantifiersModule(qs, qim, qr, qe),
  41       d_instStrategies(),
  42       d_isup(),
  43       d_i_ag(),
  44       d_quants(),
  45       d_quant_rel(nullptr)
  46 {
  47   if (options::relevantTriggers())
  48   {
  49     d_quant_rel.reset(new quantifiers::QuantRelevance);
  50   }
  51   if (options::eMatching()) {
  52     // these are the instantiation strategies for E-matching
  53     // user-provided patterns
  54     if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
  55     {
  56       d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs));
  57       d_instStrategies.push_back(d_isup.get());
  58     }
  59
  60     // auto-generated patterns
  61     d_i_ag.reset(
  62         new InstStrategyAutoGenTriggers(d_quantEngine, qs, d_quant_rel.get()));
  63     d_instStrategies.push_back(d_i_ag.get());
  64   }
  65 }
  66
  67 InstantiationEngine::~InstantiationEngine() {}
  68
  69 void InstantiationEngine::presolve() {
  70   for( unsigned i=0; i<d_instStrategies.size(); ++i ){
  71     d_instStrategies[i]->presolve();
  72   }
  73 }
  74
  75 void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
  76   unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
  77   //iterate over an internal effort level e
  78   int e = 0;
  79   int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
  80   bool finished = false;
  81   //while unfinished, try effort level=0,1,2....
  82   while( !finished && e<=eLimit ){
  83     Debug("inst-engine") << "IE: Prepare instantiation (" << e << ")." << std::endl;
  84     finished = true;
  85     //instantiate each quantifier
  86     for( unsigned i=0; i<d_quants.size(); i++ ){
  87       Node q = d_quants[i];
  88       Debug("inst-engine-debug") << "IE: Instantiate " << q << "..." << std::endl;
  89       //int e_use = d_quantEngine->getRelevance( q )==-1 ? e - 1 : e;
  90       int e_use = e;
  91       if( e_use>=0 ){
  92         Trace("inst-engine-debug") << "inst-engine : " << q << std::endl;
  93         //check each instantiation strategy
  94         for( unsigned j=0; j<d_instStrategies.size(); j++ ){
  95           InstStrategy* is = d_instStrategies[j];
  96           Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
  97           InstStrategyStatus quantStatus = is->process(q, effort, e_use);
  98           Trace("inst-engine-debug")
  99               << " -> unfinished= "
 100               << (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
 101               << ", conflict=" << d_qstate.isInConflict() << std::endl;
 102           if (d_qstate.isInConflict())
 103           {
 104             return;
 105           }
 106           else if (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
 107           {
 108             finished = false;
 109           }
 110         }
 111       }
 112     }
 113     //do not consider another level if already added lemma at this level
 114     if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
 115       finished = true;
 116     }
 117     e++;
 118   }
 119 }
 120
 121 bool InstantiationEngine::needsCheck( Theory::Effort e ){
 122   return d_quantEngine->getInstWhenNeedsCheck( e );
 123 }
 124
 125 void InstantiationEngine::reset_round( Theory::Effort e ){
 126   //if not, proceed to instantiation round
 127   //reset the instantiation strategies
 128   for( unsigned i=0; i<d_instStrategies.size(); ++i ){
 129     InstStrategy* is = d_instStrategies[i];
 130     is->processResetInstantiationRound( e );
 131   }
 132 }
 133
 134 void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
 135 {
 136   CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time);
 137   if (quant_e != QEFFORT_STANDARD)
 138   {
 139     return;
 140   }
 141   double clSet = 0;
 142   if (Trace.isOn("inst-engine"))
 143   {
 144     clSet = double(clock()) / double(CLOCKS_PER_SEC);
 145     Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e
 146                          << "---" << std::endl;
 147   }
 148   // collect all active quantified formulas belonging to this
 149   bool quantActive = false;
 150   d_quants.clear();
 151   FirstOrderModel* m = d_quantEngine->getModel();
 152   size_t nquant = m->getNumAssertedQuantifiers();
 153   for (size_t i = 0; i < nquant; i++)
 154   {
 155     Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true);
 156     if (shouldProcess(q) && m->isQuantifierActive(q))
 157     {
 158       quantActive = true;
 159       d_quants.push_back(q);
 160     }
 161   }
 162   Trace("inst-engine-debug")
 163       << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/";
 164   Trace("inst-engine-debug") << nquant << " " << quantActive << std::endl;
 165   if (quantActive)
 166   {
 167     unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
 168     doInstantiationRound(e);
 169     if (d_qstate.isInConflict())
 170     {
 171       Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting);
 172       Trace("inst-engine") << "Conflict, added lemmas = "
 173                            << (d_quantEngine->getNumLemmasWaiting()
 174                                - lastWaiting)
 175                            << std::endl;
 176     }
 177     else if (d_quantEngine->hasAddedLemma())
 178     {
 179       Trace("inst-engine") << "Added lemmas = "
 180                            << (d_quantEngine->getNumLemmasWaiting()
 181                                - lastWaiting)
 182                            << std::endl;
 183     }
 184   }
 185   else
 186   {
 187     d_quants.clear();
 188   }
 189   if (Trace.isOn("inst-engine"))
 190   {
 191     double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
 192     Trace("inst-engine") << "Finished instantiation engine, time = "
 193                          << (clSet2 - clSet) << std::endl;
 194   }
 195 }
 196
 197 bool InstantiationEngine::checkCompleteFor( Node q ) {
 198   //TODO?
 199   return false;
 200 }
 201
 202 void InstantiationEngine::checkOwnership(Node q)
 203 {
 204   if( options::strictTriggers() && q.getNumChildren()==3 ){
 205     //if strict triggers, take ownership of this quantified formula
 206     bool hasPat = false;
 207     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
 208       if( q[2][i].getKind()==INST_PATTERN || q[2][i].getKind()==INST_NO_PATTERN  ){
 209         hasPat = true;
 210         break;
 211       }
 212     }
 213     if( hasPat ){
 214       d_qreg.setOwner(q, this, 1);
 215     }
 216   }
 217 }
 218
 219 void InstantiationEngine::registerQuantifier(Node q)
 220 {
 221   if (!shouldProcess(q))
 222   {
 223     return;
 224   }
 225   if (d_quant_rel)
 226   {
 227     d_quant_rel->registerQuantifier(q);
 228   }
 229   // take into account user patterns
 230   if (q.getNumChildren() == 3)
 231   {
 232     Node subsPat =
 233         d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
 234             q[2], q);
 235     // add patterns
 236     for (const Node& p : subsPat)
 237     {
 238       if (p.getKind() == INST_PATTERN)
 239       {
 240         addUserPattern(q, p);
 241       }
 242       else if (p.getKind() == INST_NO_PATTERN)
 243       {
 244         addUserNoPattern(q, p);
 245       }
 246     }
 247   }
 248 }
 249
 250 void InstantiationEngine::addUserPattern(Node q, Node pat) {
 251   if (d_isup) {
 252     d_isup->addUserPattern(q, pat);
 253   }
 254 }
 255
 256 void InstantiationEngine::addUserNoPattern(Node q, Node pat) {
 257   if (d_i_ag) {
 258     d_i_ag->addUserNoPattern(q, pat);
 259   }
 260 }
 261
 262 bool InstantiationEngine::shouldProcess(Node q)
 263 {
 264   if (!d_qreg.hasOwnership(q, this))
 265   {
 266     return false;
 267   }
 268   // also ignore internal quantifiers
 269   QuantAttributes* qattr = d_quantEngine->getQuantAttributes();
 270   if (qattr->isInternal(q))
 271   {
 272     return false;
 273   }
 274   return true;
 275 }
 276
 277 }  // namespace quantifiers
 278 }  // namespace theory
 279 }  // namespace CVC4