diff options
Diffstat (limited to 'src/theory/quantifiers/fmf/model_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/fmf/model_engine.cpp | 342 |
1 files changed, 342 insertions, 0 deletions
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp new file mode 100644 index 000000000..3f3c21907 --- /dev/null +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -0,0 +1,342 @@ +/********************* */ +/*! \file model_engine.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of model engine class + **/ + +#include "theory/quantifiers/fmf/model_engine.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/fmf/ambqi_builder.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/fmf/full_model_check.h" +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" +#include "theory/theory_engine.h" +#include "theory/uf/equality_engine.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/theory_uf_strong_solver.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::theory::inst; + +//Model Engine constructor +ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : +QuantifiersModule( qe ), +d_incomplete_check(true), +d_addedLemmas(0), +d_triedLemmas(0), +d_totalLemmas(0) +{ + +} + +ModelEngine::~ModelEngine() { + +} + +bool ModelEngine::needsCheck( Theory::Effort e ) { + return e==Theory::EFFORT_LAST_CALL; +} + +QuantifiersModule::QEffort ModelEngine::needsModel(Theory::Effort e) +{ + if( options::mbqiInterleave() ){ + return QEFFORT_STANDARD; + }else{ + return QEFFORT_MODEL; + } +} + +void ModelEngine::reset_round( Theory::Effort e ) { + d_incomplete_check = true; +} +void ModelEngine::check(Theory::Effort e, QEffort quant_e) +{ + bool doCheck = false; + if( options::mbqiInterleave() ){ + doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); + } + if( !doCheck ){ + doCheck = quant_e == QEFFORT_MODEL; + } + if( doCheck ){ + Assert( !d_quantEngine->inConflict() ); + int addedLemmas = 0; + FirstOrderModel* fm = d_quantEngine->getModel(); + + //the following will test that the model satisfies all asserted universal quantifiers by + // (model-based) exhaustive instantiation. + double clSet = 0; + if( Trace.isOn("model-engine") ){ + Trace("model-engine") << "---Model Engine Round---" << std::endl; + clSet = double(clock())/double(CLOCKS_PER_SEC); + } + + Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; + //let the strong solver verify that the model is minimal + //for debugging, this will if there are terms in the model that the strong solver was not notified of + uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); + if( !ufss || ufss->debugModel( fm ) ){ + Trace("model-engine-debug") << "Check model..." << std::endl; + d_incomplete_check = false; + //print debug + if( Trace.isOn("fmf-model-complete") ){ + Trace("fmf-model-complete") << std::endl; + debugPrint("fmf-model-complete"); + } + //successfully built an acceptable model, now check it + addedLemmas += checkModel(); + }else{ + addedLemmas++; + } + + if( Trace.isOn("model-engine") ){ + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; + } + + if( addedLemmas==0 ){ + Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl; + //CVC4 will answer SAT or unknown + if( Trace.isOn("fmf-consistent") ){ + Trace("fmf-consistent") << std::endl; + debugPrint("fmf-consistent"); + } + } + } +} + +bool ModelEngine::checkComplete() { + return !d_incomplete_check; +} + +bool ModelEngine::checkCompleteFor( Node q ) { + return std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.end(); +} + +void ModelEngine::registerQuantifier( Node f ){ + if( Trace.isOn("fmf-warn") ){ + bool canHandle = true; + for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ + TypeNode tn = f[0][i].getType(); + if( !tn.isSort() ){ + if( !tn.getCardinality().isFinite() ){ + if( tn.isInteger() ){ + if( !options::fmfBound() ){ + canHandle = false; + } + }else{ + canHandle = false; + } + } + } + } + if( !canHandle ){ + Trace("fmf-warn") << "Warning : Model Engine : may not be able to answer SAT because of formula : " << f << std::endl; + } + } +} + +void ModelEngine::assertNode( Node f ){ + +} + +bool ModelEngine::optOneQuantPerRound(){ + return options::fmfOneQuantPerRound(); +} + + +int ModelEngine::checkModel(){ + FirstOrderModel* fm = d_quantEngine->getModel(); + + //flatten the representatives + //Trace("model-engine-debug") << "Flattening representatives...." << std::endl; + // d_quantEngine->getEqualityQuery()->flattenRepresentatives( + // fm->getRepSet()->d_type_reps ); + + //for debugging, setup + for (std::map<TypeNode, std::vector<Node> >::iterator it = + fm->getRepSetPtr()->d_type_reps.begin(); + it != fm->getRepSetPtr()->d_type_reps.end(); + ++it) + { + if( it->first.isSort() ){ + Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; + Trace("model-engine-debug") << " Reps : "; + for( size_t i=0; i<it->second.size(); i++ ){ + Trace("model-engine-debug") << it->second[i] << " "; + } + Trace("model-engine-debug") << std::endl; + Trace("model-engine-debug") << " Term reps : "; + for( size_t i=0; i<it->second.size(); i++ ){ + Node r = d_quantEngine->getInternalRepresentative( it->second[i], Node::null(), 0 ); + Trace("model-engine-debug") << r << " "; + } + Trace("model-engine-debug") << std::endl; + Node mbt = fm->getModelBasisTerm(it->first); + Trace("model-engine-debug") << " Basis term : " << mbt << std::endl; + } + } + + d_triedLemmas = 0; + d_addedLemmas = 0; + d_totalLemmas = 0; + //for statistics + if( Trace.isOn("model-engine") ){ + for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + if( d_quantEngine->getModel()->isQuantifierActive( f ) && d_quantEngine->hasOwnership( f, this ) ){ + int totalInst = 1; + for( unsigned j=0; j<f[0].getNumChildren(); j++ ){ + TypeNode tn = f[0][j].getType(); + if (fm->getRepSet()->hasType(tn)) + { + totalInst = + totalInst * (int)fm->getRepSet()->getNumRepresentatives(tn); + } + } + d_totalLemmas += totalInst; + } + } + } + + Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; + // FMC uses two sub-effort levels + int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); + for( int e=0; e<e_max; e++) { + d_incomplete_quants.clear(); + for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node q = fm->getAssertedQuantifier( i, true ); + Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl; + //determine if we should check this quantifier + if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){ + exhaustiveInstantiate( q, e ); + if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){ + break; + } + }else{ + Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl; + } + } + if( d_addedLemmas>0 ){ + break; + }else{ + Assert( !d_quantEngine->inConflict() ); + } + } + + //print debug information + if( d_quantEngine->inConflict() ){ + Trace("model-engine") << "Conflict, added lemmas = "; + }else{ + Trace("model-engine") << "Added Lemmas = "; + } + Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / "; + Trace("model-engine") << d_totalLemmas << std::endl; + return d_addedLemmas; +} + + + +void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ + //first check if the builder can do the exhaustive instantiation + quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); + unsigned prev_alem = mb->getNumAddedLemmas(); + unsigned prev_tlem = mb->getNumTriedLemmas(); + int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ); + if( retEi!=0 ){ + if( retEi<0 ){ + Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl; + d_incomplete_quants.push_back( f ); + }else{ + Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; + } + d_triedLemmas += mb->getNumTriedLemmas()-prev_tlem; + d_addedLemmas += mb->getNumAddedLemmas()-prev_alem; + d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->getNumAddedLemmas(); + }else{ + if( Trace.isOn("fmf-exh-inst-debug") ){ + Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + Trace("fmf-exh-inst-debug") << d_quantEngine->getTermUtil()->getInstantiationConstant( f, i ) << " "; + } + Trace("fmf-exh-inst-debug") << std::endl; + } + //create a rep set iterator and iterate over the (relevant) domain of the quantifier + QRepBoundExt qrbe(d_quantEngine); + RepSetIterator riter(d_quantEngine->getModel()->getRepSet(), &qrbe); + if( riter.setQuantifier( f ) ){ + Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl; + if( !riter.isIncomplete() ){ + int triedLemmas = 0; + int addedLemmas = 0; + EqualityQuery* qy = d_quantEngine->getEqualityQuery(); + Instantiate* inst = d_quantEngine->getInstantiate(); + while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ + //instantiation was not shown to be true, construct the match + InstMatch m( f ); + for (unsigned i = 0; i < riter.getNumTerms(); i++) + { + m.set(qy, i, riter.getCurrentTerm(i)); + } + Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; + triedLemmas++; + //add as instantiation + if (inst->addInstantiation(f, m, true)) + { + addedLemmas++; + if( d_quantEngine->inConflict() ){ + break; + } + }else{ + Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; + } + riter.increment(); + } + d_addedLemmas += addedLemmas; + d_triedLemmas += triedLemmas; + d_quantEngine->d_statistics.d_instantiations_fmf_exh += addedLemmas; + } + }else{ + Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl; + } + //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round + if( riter.isIncomplete() ){ + d_incomplete_quants.push_back( f ); + } + } +} + +void ModelEngine::debugPrint( const char* c ){ + Trace( c ) << "Quantifiers: " << std::endl; + for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + if( d_quantEngine->hasOwnership( q, this ) ){ + Trace( c ) << " "; + if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){ + Trace( c ) << "*Inactive* "; + }else{ + Trace( c ) << " "; + } + Trace( c ) << q << std::endl; + } + } + //d_quantEngine->getModel()->debugPrint( c ); +} + |