src/theory/quantifiers/fmf/model_engine.cpp

   1 /*********************                                                        */
   2 /*! \file model_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Kshitij Bansal
   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 model engine class
  13  **/
  14
  15 #include "theory/quantifiers/fmf/model_engine.h"
  16
  17 #include "options/quantifiers_options.h"
  18 #include "theory/quantifiers/first_order_model.h"
  19 #include "theory/quantifiers/fmf/full_model_check.h"
  20 #include "theory/quantifiers/instantiate.h"
  21 #include "theory/quantifiers/quant_rep_bound_ext.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 #include "theory/theory_engine.h"
  27 #include "theory/uf/equality_engine.h"
  28
  29 using namespace std;
  30 using namespace CVC4;
  31 using namespace CVC4::kind;
  32 using namespace CVC4::context;
  33 using namespace CVC4::theory;
  34 using namespace CVC4::theory::quantifiers;
  35 using namespace CVC4::theory::inst;
  36
  37 //Model Engine constructor
  38 ModelEngine::ModelEngine(QuantifiersEngine* qe,
  39                          QuantifiersState& qs,
  40                          QuantifiersInferenceManager& qim)
  41     : QuantifiersModule(qs, qim, qe),
  42       d_incomplete_check(true),
  43       d_addedLemmas(0),
  44       d_triedLemmas(0),
  45       d_totalLemmas(0)
  46 {
  47
  48 }
  49
  50 ModelEngine::~ModelEngine() {
  51
  52 }
  53
  54 bool ModelEngine::needsCheck( Theory::Effort e ) {
  55   return e==Theory::EFFORT_LAST_CALL;
  56 }
  57
  58 QuantifiersModule::QEffort ModelEngine::needsModel(Theory::Effort e)
  59 {
  60   if( options::mbqiInterleave() ){
  61     return QEFFORT_STANDARD;
  62   }else{
  63     return QEFFORT_MODEL;
  64   }
  65 }
  66
  67 void ModelEngine::reset_round( Theory::Effort e ) {
  68   d_incomplete_check = true;
  69 }
  70 void ModelEngine::check(Theory::Effort e, QEffort quant_e)
  71 {
  72   bool doCheck = false;
  73   if( options::mbqiInterleave() ){
  74     doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
  75   }
  76   if( !doCheck ){
  77     doCheck = quant_e == QEFFORT_MODEL;
  78   }
  79   if( doCheck ){
  80     Assert(!d_qstate.isInConflict());
  81     int addedLemmas = 0;
  82
  83     //the following will test that the model satisfies all asserted universal quantifiers by
  84     // (model-based) exhaustive instantiation.
  85     double clSet = 0;
  86     if( Trace.isOn("model-engine") ){
  87       Trace("model-engine") << "---Model Engine Round---" << std::endl;
  88       clSet = double(clock())/double(CLOCKS_PER_SEC);
  89     }
  90     Trace("model-engine-debug") << "Check model..." << std::endl;
  91     d_incomplete_check = false;
  92     // print debug
  93     if (Trace.isOn("fmf-model-complete"))
  94     {
  95       Trace("fmf-model-complete") << std::endl;
  96       debugPrint("fmf-model-complete");
  97     }
  98     // successfully built an acceptable model, now check it
  99     addedLemmas += checkModel();
 100
 101     if( Trace.isOn("model-engine") ){
 102       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
 103       Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
 104     }
 105
 106     if( addedLemmas==0 ){
 107       Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl;
 108       //CVC4 will answer SAT or unknown
 109       if( Trace.isOn("fmf-consistent") ){
 110         Trace("fmf-consistent") << std::endl;
 111         debugPrint("fmf-consistent");
 112       }
 113     }
 114   }
 115 }
 116
 117 bool ModelEngine::checkComplete() {
 118   return !d_incomplete_check;
 119 }
 120
 121 bool ModelEngine::checkCompleteFor( Node q ) {
 122   return std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.end();
 123 }
 124
 125 void ModelEngine::registerQuantifier( Node f ){
 126   if( Trace.isOn("fmf-warn") ){
 127     bool canHandle = true;
 128     for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
 129       TypeNode tn = f[0][i].getType();
 130       if( !tn.isSort() ){
 131         if (!tn.isInterpretedFinite())
 132         {
 133           if( tn.isInteger() ){
 134             if( !options::fmfBound() ){
 135               canHandle = false;
 136             }
 137           }else{
 138             canHandle = false;
 139           }
 140         }
 141       }
 142     }
 143     if( !canHandle ){
 144       Trace("fmf-warn") << "Warning : Model Engine : may not be able to answer SAT because of formula : " << f << std::endl;
 145     }
 146   }
 147 }
 148
 149 void ModelEngine::assertNode( Node f ){
 150
 151 }
 152
 153 int ModelEngine::checkModel(){
 154   FirstOrderModel* fm = d_quantEngine->getModel();
 155
 156   //for debugging, setup
 157   for (std::map<TypeNode, std::vector<Node> >::iterator it =
 158            fm->getRepSetPtr()->d_type_reps.begin();
 159        it != fm->getRepSetPtr()->d_type_reps.end();
 160        ++it)
 161   {
 162     if( it->first.isSort() ){
 163       Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
 164       Trace("model-engine-debug") << "        Reps : ";
 165       for( size_t i=0; i<it->second.size(); i++ ){
 166         Trace("model-engine-debug") << it->second[i] << "  ";
 167       }
 168       Trace("model-engine-debug") << std::endl;
 169       Trace("model-engine-debug") << "   Term reps : ";
 170       for( size_t i=0; i<it->second.size(); i++ ){
 171         Node r = d_quantEngine->getInternalRepresentative( it->second[i], Node::null(), 0 );
 172         if (r.isNull())
 173         {
 174           // there was an invalid equivalence class
 175           d_incomplete_check = true;
 176         }
 177         Trace("model-engine-debug") << r << " ";
 178       }
 179       Trace("model-engine-debug") << std::endl;
 180       Node mbt = fm->getModelBasisTerm(it->first);
 181       Trace("model-engine-debug") << "  Basis term : " << mbt << std::endl;
 182     }
 183   }
 184
 185   d_triedLemmas = 0;
 186   d_addedLemmas = 0;
 187   d_totalLemmas = 0;
 188   //for statistics
 189   if( Trace.isOn("model-engine") ){
 190     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
 191       Node f = fm->getAssertedQuantifier( i );
 192       if( d_quantEngine->getModel()->isQuantifierActive( f ) && d_quantEngine->hasOwnership( f, this ) ){
 193         int totalInst = 1;
 194         for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
 195           TypeNode tn = f[0][j].getType();
 196           if (fm->getRepSet()->hasType(tn))
 197           {
 198             totalInst =
 199                 totalInst * (int)fm->getRepSet()->getNumRepresentatives(tn);
 200           }
 201         }
 202         d_totalLemmas += totalInst;
 203       }
 204     }
 205   }
 206
 207   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
 208   // FMC uses two sub-effort levels
 209   int e_max = options::mbqiMode() == options::MbqiMode::FMC
 210                   ? 2
 211                   : (options::mbqiMode() == options::MbqiMode::TRUST ? 0 : 1);
 212   for( int e=0; e<e_max; e++) {
 213     d_incomplete_quants.clear();
 214     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
 215       Node q = fm->getAssertedQuantifier( i, true );
 216       Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
 217       //determine if we should check this quantifier
 218       if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){
 219         exhaustiveInstantiate( q, e );
 220         if (d_qstate.isInConflict())
 221         {
 222           break;
 223         }
 224       }else{
 225         Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl;
 226       }
 227     }
 228     if( d_addedLemmas>0 ){
 229       break;
 230     }else{
 231       Assert(!d_qstate.isInConflict());
 232     }
 233   }
 234
 235   //print debug information
 236   if (d_qstate.isInConflict())
 237   {
 238     Trace("model-engine") << "Conflict, added lemmas = ";
 239   }else{
 240     Trace("model-engine") << "Added Lemmas = ";
 241   }
 242   Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / ";
 243   Trace("model-engine") << d_totalLemmas << std::endl;
 244   return d_addedLemmas;
 245 }
 246
 247
 248
 249 void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
 250   //first check if the builder can do the exhaustive instantiation
 251   quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
 252   unsigned prev_alem = mb->getNumAddedLemmas();
 253   unsigned prev_tlem = mb->getNumTriedLemmas();
 254   int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort );
 255   if( retEi!=0 ){
 256     if( retEi<0 ){
 257       Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
 258       d_incomplete_quants.push_back( f );
 259     }else{
 260       Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
 261     }
 262     d_triedLemmas += mb->getNumTriedLemmas()-prev_tlem;
 263     d_addedLemmas += mb->getNumAddedLemmas()-prev_alem;
 264     d_quantEngine->d_statistics.d_instantiations_fmf_mbqi +=
 265         (mb->getNumAddedLemmas() - prev_alem);
 266   }else{
 267     if( Trace.isOn("fmf-exh-inst-debug") ){
 268       Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
 269       for( size_t i=0; i<f[0].getNumChildren(); i++ ){
 270         Trace("fmf-exh-inst-debug") << d_quantEngine->getTermUtil()->getInstantiationConstant( f, i ) << " ";
 271       }
 272       Trace("fmf-exh-inst-debug") << std::endl;
 273     }
 274     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
 275     QRepBoundExt qrbe(d_quantEngine);
 276     RepSetIterator riter(d_quantEngine->getModel()->getRepSet(), &qrbe);
 277     if( riter.setQuantifier( f ) ){
 278       Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
 279       if( !riter.isIncomplete() ){
 280         int triedLemmas = 0;
 281         int addedLemmas = 0;
 282         EqualityQuery* qy = d_quantEngine->getEqualityQuery();
 283         Instantiate* inst = d_quantEngine->getInstantiate();
 284         while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
 285           //instantiation was not shown to be true, construct the match
 286           InstMatch m( f );
 287           for (unsigned i = 0; i < riter.getNumTerms(); i++)
 288           {
 289             m.set(qy, i, riter.getCurrentTerm(i));
 290           }
 291           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
 292           triedLemmas++;
 293           //add as instantiation
 294           if (inst->addInstantiation(f, m, true))
 295           {
 296             addedLemmas++;
 297             if (d_qstate.isInConflict())
 298             {
 299               break;
 300             }
 301           }else{
 302             Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
 303           }
 304           riter.increment();
 305         }
 306         d_addedLemmas += addedLemmas;
 307         d_triedLemmas += triedLemmas;
 308         d_quantEngine->d_statistics.d_instantiations_fmf_exh += addedLemmas;
 309       }
 310     }else{
 311       Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
 312     }
 313     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
 314     if( riter.isIncomplete() ){
 315       d_incomplete_quants.push_back( f );
 316     }
 317   }
 318 }
 319
 320 void ModelEngine::debugPrint( const char* c ){
 321   Trace( c ) << "Quantifiers: " << std::endl;
 322   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
 323     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
 324     if( d_quantEngine->hasOwnership( q, this ) ){
 325       Trace( c ) << "   ";
 326       if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){
 327         Trace( c ) << "*Inactive* ";
 328       }else{
 329         Trace( c ) << "           ";
 330       }
 331       Trace( c ) << q << std::endl;
 332     }
 333   }
 334   //d_quantEngine->getModel()->debugPrint( c );
 335 }
 336