src/theory/quantifiers/model_engine.cpp

   1 /*********************                                                        */
   2 /*! \file model_engine.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Andrew Reynolds
   6  ** Minor contributors (to current version): Francois Bobot
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Implementation of model engine class
  13  **/
  14
  15 #include "theory/quantifiers/model_engine.h"
  16 #include "theory/theory_engine.h"
  17 #include "theory/uf/equality_engine.h"
  18 #include "theory/uf/theory_uf.h"
  19 #include "theory/uf/theory_uf_strong_solver.h"
  20 #include "theory/quantifiers/options.h"
  21 #include "theory/quantifiers/first_order_model.h"
  22 #include "theory/quantifiers/term_database.h"
  23 #include "theory/quantifiers/quantifiers_attributes.h"
  24 #include "theory/quantifiers/full_model_check.h"
  25 #include "theory/quantifiers/qinterval_builder.h"
  26 #include "theory/quantifiers/ambqi_builder.h"
  27
  28 using namespace std;
  29 using namespace CVC4;
  30 using namespace CVC4::kind;
  31 using namespace CVC4::context;
  32 using namespace CVC4::theory;
  33 using namespace CVC4::theory::quantifiers;
  34 using namespace CVC4::theory::inst;
  35
  36 //Model Engine constructor
  37 ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
  38 QuantifiersModule( qe ),
  39 d_incomplete_check(false),
  40 d_addedLemmas(0),
  41 d_triedLemmas(0),
  42 d_totalLemmas(0)
  43 {
  44
  45   Trace("model-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
  46   if( options::mbqiMode()==MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
  47       options::mbqiMode()==MBQI_TRUST || options::fmfBoundInt() ){
  48     Trace("model-engine-debug") << "...make fmc builder." << std::endl;
  49     d_builder = new fmcheck::FullModelChecker( c, qe );
  50   }else if( options::mbqiMode()==MBQI_INTERVAL ){
  51     Trace("model-engine-debug") << "...make interval builder." << std::endl;
  52     d_builder = new QIntervalBuilder( c, qe );
  53   }else if( options::mbqiMode()==MBQI_ABS ){
  54     Trace("model-engine-debug") << "...make abs mbqi builder." << std::endl;
  55     d_builder = new AbsMbqiBuilder( c, qe );
  56   }else if( options::mbqiMode()==MBQI_INST_GEN ){
  57     Trace("model-engine-debug") << "...make inst-gen builder." << std::endl;
  58     d_builder = new QModelBuilderInstGen( c, qe );
  59   }else{
  60     Trace("model-engine-debug") << "...make default model builder." << std::endl;
  61     d_builder = new QModelBuilderDefault( c, qe );
  62   }
  63 }
  64
  65 ModelEngine::~ModelEngine() {
  66   delete d_builder;
  67 }
  68
  69 void ModelEngine::check( Theory::Effort e ){
  70   if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){
  71     int addedLemmas = 0;
  72     bool needsBuild = true;
  73     FirstOrderModel* fm = d_quantEngine->getModel();
  74     if( fm->getNumAssertedQuantifiers()>0 ){
  75       //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
  76       //quantifiers are initialized, we begin an instantiation round
  77       double clSet = 0;
  78       if( Trace.isOn("model-engine") ){
  79         clSet = double(clock())/double(CLOCKS_PER_SEC);
  80       }
  81       ++(d_statistics.d_inst_rounds);
  82       bool buildAtFullModel = d_builder->optBuildAtFullModel();
  83       needsBuild = !buildAtFullModel;
  84       //two effort levels: first try exhaustive instantiation without axioms, then with.
  85       int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
  86       for( int effort=startEffort; effort<2; effort++ ){
  87         // for effort = 0, we only instantiate non-axioms
  88         // for effort = 1, we instantiate everything
  89         if( addedLemmas==0 ){
  90           Trace("model-engine") << "---Model Engine Round---" << std::endl;
  91           //initialize the model
  92           Trace("model-engine-debug") << "Build model..." << std::endl;
  93           d_builder->d_considerAxioms = effort>=1;
  94           d_builder->d_addedLemmas = 0;
  95           d_builder->buildModel( fm, buildAtFullModel );
  96           addedLemmas += (int)d_builder->d_addedLemmas;
  97           //if builder has lemmas, add and return
  98           if( addedLemmas==0 ){
  99             Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
 100             //let the strong solver verify that the model is minimal
 101             //for debugging, this will if there are terms in the model that the strong solver was not notified of
 102             if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){
 103               Trace("model-engine-debug") << "Check model..." << std::endl;
 104               d_incomplete_check = false;
 105               //print debug
 106               Debug("fmf-model-complete") << std::endl;
 107               debugPrint("fmf-model-complete");
 108               //successfully built an acceptable model, now check it
 109               addedLemmas += checkModel();
 110             }else{
 111               addedLemmas++;
 112             }
 113           }
 114         }
 115         if( addedLemmas==0 ){
 116           //if we have not added lemmas yet and axiomInstMode=trust, then we are done
 117           if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){
 118             //we must return unknown if an axiom is asserted
 119             if( effort==0 ){
 120               d_incomplete_check = true;
 121             }
 122             break;
 123           }
 124         }
 125       }
 126       if( Trace.isOn("model-engine") ){
 127         double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
 128         Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
 129       }
 130     }else{
 131       Trace("model-engine-debug") << "No quantified formulas asserted." << std::endl;
 132     }
 133     if( addedLemmas==0 ){
 134       Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
 135       //CVC4 will answer SAT or unknown
 136       Trace("fmf-consistent") << std::endl;
 137       debugPrint("fmf-consistent");
 138       if( options::produceModels() && needsBuild ){
 139         // finish building the model
 140         d_builder->buildModel( fm, true );
 141       }
 142       //if the check was incomplete, we must set incomplete flag
 143       if( d_incomplete_check ){
 144         d_quantEngine->getOutputChannel().setIncomplete();
 145       }
 146     }else{
 147       //otherwise, the search will continue
 148       d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
 149     }
 150   }
 151 }
 152
 153 void ModelEngine::registerQuantifier( Node f ){
 154   if( Trace.isOn("fmf-warn") ){
 155     bool canHandle = true;
 156     for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
 157       TypeNode tn = f[0][i].getType();
 158       if( !tn.isSort() ){
 159         if( !tn.getCardinality().isFinite() ){
 160           if( tn.isInteger() ){
 161             if( !options::fmfBoundInt() ){
 162               canHandle = false;
 163             }
 164           }else{
 165             canHandle = false;
 166           }
 167         }
 168       }
 169     }
 170     if( !canHandle ){
 171       Trace("fmf-warn") << "Warning : Model Engine : may not be able to answer SAT because of formula : " << f << std::endl;
 172     }
 173   }
 174 }
 175
 176 void ModelEngine::assertNode( Node f ){
 177
 178 }
 179
 180 bool ModelEngine::optOneQuantPerRound(){
 181   return options::fmfOneQuantPerRound();
 182 }
 183
 184
 185 int ModelEngine::checkModel(){
 186   FirstOrderModel* fm = d_quantEngine->getModel();
 187
 188   //flatten the representatives
 189   //Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
 190   //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps );
 191
 192   //for debugging
 193   if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){
 194     for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
 195          it != fm->d_rep_set.d_type_reps.end(); ++it ){
 196       if( it->first.isSort() ){
 197         Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
 198         if( Trace.isOn("model-engine-debug") ){
 199           Trace("model-engine-debug") << "   ";
 200           Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
 201           for( size_t i=0; i<it->second.size(); i++ ){
 202             //Trace("model-engine-debug") << it->second[i] << "  ";
 203             Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
 204             Trace("model-engine-debug") << r << " ";
 205           }
 206           Trace("model-engine-debug") << std::endl;
 207           Trace("model-engine-debug") << "  Model basis term : " << mbt << std::endl;
 208         }
 209       }
 210     }
 211   }
 212
 213   d_triedLemmas = 0;
 214   d_addedLemmas = 0;
 215   d_totalLemmas = 0;
 216   //for statistics
 217   for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
 218     Node f = fm->getAssertedQuantifier( i );
 219     int totalInst = 1;
 220     for( size_t i=0; i<f[0].getNumChildren(); i++ ){
 221       TypeNode tn = f[0][i].getType();
 222       if( fm->d_rep_set.hasType( tn ) ){
 223         totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
 224       }
 225     }
 226     d_totalLemmas += totalInst;
 227   }
 228
 229   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
 230   int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 );
 231   for( int e=0; e<e_max; e++) {
 232     if (d_addedLemmas==0) {
 233       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
 234         Node f = fm->getAssertedQuantifier( i );
 235         //determine if we should check this quantifier
 236         if( d_builder->isQuantifierActive( f ) ){
 237           exhaustiveInstantiate( f, e );
 238           if( Trace.isOn("model-engine-warn") ){
 239             if( d_addedLemmas>10000 ){
 240               Debug("fmf-exit") << std::endl;
 241               debugPrint("fmf-exit");
 242               exit( 0 );
 243             }
 244           }
 245           if( optOneQuantPerRound() && d_addedLemmas>0 ){
 246             break;
 247           }
 248         }else{
 249           Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl;
 250         }
 251       }
 252     }
 253   }
 254   //print debug information
 255   Trace("model-engine-debug") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl;
 256   Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
 257   Trace("model-engine") << d_totalLemmas << std::endl;
 258   return d_addedLemmas;
 259 }
 260
 261 void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
 262   //first check if the builder can do the exhaustive instantiation
 263   d_builder->d_triedLemmas = 0;
 264   d_builder->d_addedLemmas = 0;
 265   d_builder->d_incomplete_check = false;
 266   if( d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
 267     Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl;
 268     d_triedLemmas += d_builder->d_triedLemmas;
 269     d_addedLemmas += d_builder->d_addedLemmas;
 270     d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check;
 271     d_statistics.d_mbqi_inst_lemmas += d_builder->d_addedLemmas;
 272   }else{
 273     Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
 274     Debug("inst-fmf-ei") << "   Instantiation Constants: ";
 275     for( size_t i=0; i<f[0].getNumChildren(); i++ ){
 276       Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
 277     }
 278     Debug("inst-fmf-ei") << std::endl;
 279     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
 280     RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
 281     if( riter.setQuantifier( f ) ){
 282       Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
 283       int triedLemmas = 0;
 284       int addedLemmas = 0;
 285       while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
 286         //instantiation was not shown to be true, construct the match
 287         InstMatch m( f );
 288         for( int i=0; i<riter.getNumTerms(); i++ ){
 289           m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) );
 290         }
 291         Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
 292         triedLemmas++;
 293         //add as instantiation
 294         if( d_quantEngine->addInstantiation( f, m ) ){
 295           addedLemmas++;
 296         }else{
 297           Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
 298         }
 299         riter.increment();
 300       }
 301       d_addedLemmas += addedLemmas;
 302       d_triedLemmas += triedLemmas;
 303       d_statistics.d_exh_inst_lemmas += addedLemmas;
 304     }
 305     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
 306     d_incomplete_check = d_incomplete_check || riter.d_incomplete;
 307   }
 308 }
 309
 310 void ModelEngine::debugPrint( const char* c ){
 311   Trace( c ) << "Quantifiers: " << std::endl;
 312   for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
 313     Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
 314     Trace( c ) << "   ";
 315     if( !d_builder->isQuantifierActive( f ) ){
 316       Trace( c ) << "*Inactive* ";
 317     }else{
 318       Trace( c ) << "           ";
 319     }
 320     Trace( c ) << f << std::endl;
 321   }
 322   //d_quantEngine->getModel()->debugPrint( c );
 323 }
 324
 325 ModelEngine::Statistics::Statistics():
 326   d_inst_rounds("ModelEngine::Inst_Rounds", 0),
 327   d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ),
 328   d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 )
 329 {
 330   StatisticsRegistry::registerStat(&d_inst_rounds);
 331   StatisticsRegistry::registerStat(&d_exh_inst_lemmas);
 332   StatisticsRegistry::registerStat(&d_mbqi_inst_lemmas);
 333 }
 334
 335 ModelEngine::Statistics::~Statistics(){
 336   StatisticsRegistry::unregisterStat(&d_inst_rounds);
 337   StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas);
 338   StatisticsRegistry::unregisterStat(&d_mbqi_inst_lemmas);
 339 }
 340
 341