From 3a2aed30267a33ff78006aec6a5b36aad96feb09 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 18 Nov 2014 17:39:05 +0100 Subject: [PATCH] Add local theory extensions instantiation strategy (incomplete). Refactor how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist. --- src/smt/smt_engine.cpp | 57 ++++++---- src/theory/datatypes/theory_datatypes.cpp | 8 +- src/theory/datatypes/theory_datatypes.h | 2 + .../quantifiers/candidate_generator.cpp | 22 ++-- src/theory/quantifiers/candidate_generator.h | 2 + .../quantifiers/inst_match_generator.cpp | 2 +- src/theory/quantifiers/inst_match_generator.h | 2 +- .../quantifiers/inst_strategy_e_matching.cpp | 91 ++++++++++++++-- .../quantifiers/inst_strategy_e_matching.h | 25 ++++- .../quantifiers/instantiation_engine.cpp | 100 +++++++++++------- src/theory/quantifiers/instantiation_engine.h | 36 +++---- src/theory/quantifiers/options | 9 +- src/theory/quantifiers/term_database.cpp | 26 +++-- src/theory/quantifiers/term_database.h | 2 + src/theory/quantifiers/trigger.cpp | 59 ++++++----- src/theory/quantifiers/trigger.h | 4 +- test/regress/regress0/datatypes/Makefile.am | 3 +- .../datatypes/cdt-non-canon-stream.smt2 | 11 ++ 18 files changed, 316 insertions(+), 145 deletions(-) create mode 100644 test/regress/regress0/datatypes/cdt-non-canon-stream.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c87753d8d..a80177429 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1268,25 +1268,22 @@ void SmtEngine::setDefaults() { options::decisionMode.set(decMode); options::decisionStopOnly.set(stoponly); } - - //for finite model finding - if( ! options::instWhenMode.wasSetByUser()){ - //instantiate only on last call - if( options::fmfInstEngine() ){ - Trace("smt") << "setting inst when mode to LAST_CALL" << endl; - options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); + //local theory extensions + if( options::localTheoryExt() ){ + //no E-matching? + if( !options::instMaxLevel.wasSetByUser() ){ + options::instMaxLevel.set( 0 ); } } if( d_logic.hasCardinalityConstraints() ){ //must have finite model finding on options::finiteModelFind.set( true ); } - if( options::recurseCbqi() ){ - options::cbqi.set( true ); - } if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) { options::fmfBoundInt.set( true ); } + //now have determined whether fmfBoundInt is on/off + //apply fmfBoundInt options if( options::fmfBoundInt() ){ //must have finite model finding on options::finiteModelFind.set( true ); @@ -1301,6 +1298,35 @@ void SmtEngine::setDefaults() { if( options::ufssSymBreak() ){ options::sortInference.set( true ); } + if( options::fmfFunWellDefined() ){ + if( !options::finiteModelFind.wasSetByUser() ){ + options::finiteModelFind.set( true ); + } + } + + //now, have determined whether finite model find is on/off + //apply finite model finding options + if( options::finiteModelFind() ){ + if( !options::eMatching.wasSetByUser() ){ + options::eMatching.set( options::fmfInstEngine() ); + } + if( !options::quantConflictFind.wasSetByUser() ){ + options::quantConflictFind.set( false ); + } + //for finite model finding + if( ! options::instWhenMode.wasSetByUser()){ + //instantiate only on last call + if( options::eMatching() ){ + Trace("smt") << "setting inst when mode to LAST_CALL" << endl; + options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); + } + } + } + + //implied options... + if( options::recurseCbqi() ){ + options::cbqi.set( true ); + } if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } @@ -1342,16 +1368,7 @@ void SmtEngine::setDefaults() { options::conjectureGen.set( false ); } } - if( options::fmfFunWellDefined() ){ - if( !options::finiteModelFind.wasSetByUser() ){ - options::finiteModelFind.set( true ); - } - } - if( options::finiteModelFind() ){ - if( !options::quantConflictFind.wasSetByUser() ){ - options::quantConflictFind.set( false ); - } - } + //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index dd56ebba9..a70343702 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -123,6 +123,7 @@ void TheoryDatatypes::check(Effort e) { if (done() && !fullEffort(e)) { return; } + d_addedLemma = false; TimerStat::CodeTimer checkTimer(d_checkTime); @@ -150,14 +151,15 @@ void TheoryDatatypes::check(Effort e) { flushPendingFacts(); } - if( e == EFFORT_FULL && !d_conflict && !d_valuation.needCheck() ) { + if( e == EFFORT_FULL && !d_conflict && !d_addedLemma && !d_valuation.needCheck() ) { //check for cycles + Assert( d_pending.empty() && d_pending_merge.empty() ); bool addedFact; do { checkCycles(); addedFact = !d_pending.empty() || !d_pending_merge.empty(); flushPendingFacts(); - if( d_conflict ){ + if( d_conflict || d_addedLemma ){ return; } }while( addedFact ); @@ -305,6 +307,7 @@ void TheoryDatatypes::flushPendingFacts(){ } Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl; d_out->lemma( lem ); + d_addedLemma = true; }else{ assertFact( fact, exp ); } @@ -1506,6 +1509,7 @@ void TheoryDatatypes::checkCycles() { } //process codatatypes if( cdt_eqc.size()>1 && options::cdtBisimilar() ){ + printModelDebug("dt-cdt-debug"); Trace("dt-cdt-debug") << "Process " << cdt_eqc.size() << " co-datatypes" << std::endl; std::vector< std::vector< Node > > part_out; std::vector< TNode > exp; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 84d894098..30b0140a9 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -160,6 +160,8 @@ private: //BoolMap d_consEqc; /** Are we in conflict */ context::CDO d_conflict; + /** Added lemma ? */ + bool d_addedLemma; /** The conflict node */ Node d_conflictNode; /** cache for which terms we have called collectTerms(...) on */ diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index a10181c51..cfaa6d1ad 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -192,19 +192,29 @@ void CandidateGeneratorQEAll::resetInstantiationRound() { void CandidateGeneratorQEAll::reset( Node eqc ) { d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); + d_firstTime = true; } Node CandidateGeneratorQEAll::getNextCandidate() { while( !d_eq.isFinished() ){ Node n = (*d_eq); - if( options::instMaxLevel()!=-1 ){ - n = d_qe->getEqualityQuery()->getInternalRepresentative( n, d_f, d_index ); - } ++d_eq; - if( n.getType().isSubtypeOf( d_match_pattern.getType() ) ){ - //an equivalence class with the same type as the pattern, return it - return n; + if( n.getType().isSubtypeOf( d_match_pattern_type ) ){ + if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){ + if( options::instMaxLevel()!=-1 ){ + n = d_qe->getEqualityQuery()->getInternalRepresentative( n, d_f, d_index ); + } + d_firstTime = false; + //an equivalence class with the same type as the pattern, return it + return n; + } } } + if( d_firstTime ){ + Assert( d_qe->getTermDatabase()->d_type_map[d_match_pattern_type].empty() ); + //must return something + d_firstTime = false; + return d_qe->getTermDatabase()->getFreeVariableForType( d_match_pattern_type ); + } return Node::null(); } diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index 011e2924d..7a959a70d 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -150,6 +150,8 @@ private: // quantifier/index for the variable we are matching Node d_f; unsigned d_index; + //first time + bool d_firstTime; public: CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ); ~CandidateGeneratorQEAll(){} diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 4a5197fc8..cd24f9ac2 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -456,7 +456,7 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersE } /** constructors */ -InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) : +InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe ) : d_f( f ){ Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl; std::map< Node, std::vector< Node > > var_contains; diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 850affe56..1be67caed 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -184,7 +184,7 @@ private: void calculateMatches( QuantifiersEngine* qe ); public: /** constructors */ - InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 ); + InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe ); /** destructor */ ~InstMatchGeneratorMulti(){} /** reset instantiation round (call this whenever equivalence classes have changed) */ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 8a0ec3c09..8918a6dac 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -28,6 +28,14 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; using namespace CVC4::theory::quantifiers; +//priority levels : +//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers) +//2 : user patterns (when user-pat=resort ), auto gen patterns (for user pattern quantifiers, when user-pat=use) +//3 : local theory extensions +//4 : +//5 : full saturate quantifiers + + //#define MULTI_TRIGGER_FULL_EFFORT_HALF #define MULTI_MULTI_TRIGGERS @@ -220,15 +228,16 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor d_patTerms[0][f].clear(); d_patTerms[1][f].clear(); std::vector< Node > patTermsF; + //well-defined function: can assume LHS is only trigger + Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); if( d_quantEngine->getTermDatabase()->isQAttrFunDef( f ) && options::quantFunWellDefined() ){ - Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); Assert( bd.getKind()==EQUAL || bd.getKind()==IFF ); Assert( bd[0].getKind()==APPLY_UF ); patTermsF.push_back( bd[0] ); }else{ - Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, d_user_no_gen[f], true ); + Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true ); } - Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; + Trace("auto-gen-trigger") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; Trace("auto-gen-trigger") << " "; for( int i=0; i<(int)patTermsF.size(); i++ ){ Trace("auto-gen-trigger") << patTermsF[i] << " "; @@ -321,8 +330,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor d_made_multi_trigger[f] = true; } //will possibly want to get an old trigger - tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD, - options::smartTriggers() ); + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD, options::smartTriggers() ); } if( tr ){ if( tr->isMultiTrigger() ){ @@ -356,8 +364,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor if( !options::relevantTriggers() || d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){ d_single_trigger_gen[ patTerms[index] ] = true; - Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, - options::smartTriggers() ); + Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() ); if( tr2 ){ //Notice() << "Add additional trigger " << patTerms[index] << std::endl; tr2->resetInstantiationRound(); @@ -404,7 +411,75 @@ void InstStrategyAutoGenTriggers::addUserNoPattern( Node f, Node pat ) { } } + +void InstStrategyLocalTheoryExt::processResetInstantiationRound( Theory::Effort effort ){ + //reset triggers + for( std::map< Node, Trigger* >::iterator it = d_lte_trigger.begin(); it != d_lte_trigger.end(); ++it ){ + it->second->resetInstantiationRound(); + it->second->reset( Node::null() ); + } +} + +int InstStrategyLocalTheoryExt::process( Node f, Theory::Effort effort, int e ) { + if( e<3 ){ + return STATUS_UNFINISHED; + }else if( e==3 ){ + if( isLocalTheoryExt( f ) ){ + std::map< Node, Trigger* >::iterator it = d_lte_trigger.find( f ); + if( it!=d_lte_trigger.end() ){ + Trigger * tr = it->second; + //process the trigger + Trace("process-trigger") << " LTE process "; + tr->debugPrint("process-trigger"); + Trace("process-trigger") << "..." << std::endl; + InstMatch baseMatch( f ); + int numInst = tr->addInstantiations( baseMatch ); + Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; + d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_lte += numInst; + } + } + } + return STATUS_UNKNOWN; +} + +bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { + std::map< Node, bool >::iterator itq = d_quant.find( f ); + if( itq==d_quant.end() ){ + //generate triggers + Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); + std::vector< Node > vars; + std::vector< Node > patTerms; + bool ret = Trigger::isLocalTheoryExt( bd, vars, patTerms ); + if( ret ){ + d_quant[f] = ret; + //add all variables to trigger that don't already occur + for( unsigned i=0; igetTermDatabase()->getInstantiationConstant( f, i ); + if( std::find( vars.begin(), vars.end(), x )==vars.end() ){ + patTerms.push_back( x ); + } + } + Trace("local-t-ext") << "Local theory extensions trigger for " << f << " : " << std::endl; + for( unsigned i=0; isecond; + } +} + void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){ + } int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ @@ -503,6 +578,6 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ } } } - return STATUS_UNKNOWN; } + return STATUS_UNKNOWN; } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index dd4486803..d2c611d34 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -58,7 +58,7 @@ public: std::string identify() const { return std::string("UserPatterns"); } };/* class InstStrategyUserPatterns */ -class InstStrategyAutoGenTriggers : public InstStrategy{ +class InstStrategyAutoGenTriggers : public InstStrategy { public: enum { RELEVANCE_NONE, @@ -98,7 +98,7 @@ public: /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all) rstrt is the relevance setting for trigger (use only relevant triggers vs. use all) rgfr is the frequency at which triggers are generated */ - InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rgfr = -1 ); + InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rgfr = -1 ); ~InstStrategyAutoGenTriggers(){} public: /** get auto-generated trigger */ @@ -109,6 +109,26 @@ public: void addUserNoPattern( Node f, Node pat ); };/* class InstStrategyAutoGenTriggers */ + +class InstStrategyLocalTheoryExt : public InstStrategy { +private: + /** have we registered quantifier, value is whether it is an LTE term */ + std::map< Node, bool > d_quant; + /** triggers for each quantifier */ + std::map< Node, inst::Trigger* > d_lte_trigger; +private: + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e ); +public: + InstStrategyLocalTheoryExt( QuantifiersEngine* qe ) : InstStrategy( qe ){} + /** identify */ + std::string identify() const { return std::string("LocalTheoryExt"); } + /** is local theory quantifier? */ + bool isLocalTheoryExt( Node f ); +}; + + class InstStrategyFreeVariable : public InstStrategy{ private: /** guessed instantiations */ @@ -124,6 +144,7 @@ public: std::string identify() const { return std::string("FreeVariable"); } };/* class InstStrategyFreeVariable */ + } }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 1cb86e32f..ade6d4313 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -31,26 +31,26 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) : -QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){ +QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){ } InstantiationEngine::~InstantiationEngine() { delete d_i_ag; delete d_isup; + delete d_i_lte; + delete d_i_fs; + delete d_i_splx; } void InstantiationEngine::finishInit(){ - if( !options::finiteModelFind() || options::fmfInstEngine() ){ - + if( options::eMatching() ){ //these are the instantiation strategies for E-matching //user-provided patterns if( options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ d_isup = new InstStrategyUserPatterns( d_quantEngine ); - addInstStrategy( d_isup ); - }else{ - d_isup = NULL; + d_instStrategies.push_back( d_isup ); } //auto-generated patterns @@ -61,18 +61,25 @@ void InstantiationEngine::finishInit(){ tstrt = Trigger::TS_MAX_TRIGGER; } d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, tstrt, 3 ); - addInstStrategy( d_i_ag ); - - //full saturation : instantiate from relevant domain, then arbitrary terms - if( !options::finiteModelFind() && options::fullSaturateQuant() ){ - addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) ); - } + d_instStrategies.push_back( d_i_ag ); + } + + //local theory extensions + if( options::localTheoryExt() ){ + d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine ); + d_instStrategies.push_back( d_i_lte ); + } + + //full saturation : instantiate from relevant domain, then arbitrary terms + if( options::fullSaturateQuant() ){ + d_i_fs = new InstStrategyFreeVariable( d_quantEngine ); + d_instStrategies.push_back( d_i_fs ); } //counterexample-based quantifier instantiation if( options::cbqi() ){ - addInstStrategy( new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ) ); - // addInstStrategy( new InstStrategyDatatypesValue( d_quantEngine ) ); + d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ); + d_instStrategies.push_back( d_i_splx ); } } @@ -117,18 +124,16 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //reset the instantiators for( size_t i=0; iprocessResetInstantiationRound( effort ); - } + is->processResetInstantiationRound( effort ); } //iterate over an internal effort level e int e = 0; int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2; - d_inst_round_status = InstStrategy::STATUS_UNFINISHED; + bool finished = false; //while unfinished, try effort level=0,1,2.... - while( d_inst_round_status==InstStrategy::STATUS_UNFINISHED && e<=eLimit ){ + while( !finished && e<=eLimit ){ Debug("inst-engine") << "IE: Prepare instantiation (" << e << ")." << std::endl; - d_inst_round_status = InstStrategy::STATUS_SAT; + finished = true; //instantiate each quantifier for( int q=0; qgetModel()->getNumAssertedQuantifiers(); q++ ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( q ); @@ -141,11 +146,13 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //check each instantiation strategy for( size_t i=0; ishouldProcess( f ) ){ + if( is->shouldProcess( f ) ){ Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl; int quantStatus = is->process( f, effort, e_use ); Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl; - InstStrategy::updateStatus( d_inst_round_status, quantStatus ); + if( quantStatus==InstStrategy::STATUS_UNFINISHED ){ + finished = false; + } } } } @@ -153,7 +160,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } //do not consider another level if already added lemma at this level if( d_quantEngine->d_lemmas_waiting.size()>lastWaiting ){ - d_inst_round_status = InstStrategy::STATUS_UNKNOWN; + finished = true; } e++; } @@ -266,28 +273,27 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ } if( quantActive ){ bool addedLemmas = doInstantiationRound( e ); - //Debug("quantifiers-dec") << "Do instantiation, level = " << d_quantEngine->getValuation().getDecisionLevel() << std::endl; - //for( int i=1; i<=(int)d_valuation.getDecisionLevel(); i++ ){ - // Debug("quantifiers-dec") << " " << d_valuation.getDecision( i ) << std::endl; - //} - if( e==Theory::EFFORT_LAST_CALL ){ - if( !addedLemmas ){ - if( d_inst_round_status==InstStrategy::STATUS_SAT ){ - Debug("inst-engine") << "No instantiation given, returning SAT..." << std::endl; - debugSat( SAT_INST_STRATEGY ); - }else if( d_setIncomplete ){ + if( !addedLemmas && e==Theory::EFFORT_LAST_CALL ){ + //check if we need to set the incomplete flag + if( d_setIncomplete ){ + //check if we are complete for all active quantifiers + bool inc = false; + for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); + if( isIncomplete( f ) ){ + inc = true; + break; + } + } + if( inc ){ Debug("inst-engine") << "No instantiation given, returning unknown..." << std::endl; d_quantEngine->getOutputChannel().setIncomplete(); }else{ - Assert( options::finiteModelFind() ); - Debug("inst-engine") << "No instantiation given, defer to another engine..." << std::endl; + Debug("inst-engine") << "Instantiation strategies were complete..." << std::endl; } - } - } - }else{ - if( e==Theory::EFFORT_LAST_CALL ){ - if( options::cbqi() ){ - debugSat( SAT_CBQI ); + }else{ + Assert( options::finiteModelFind() ); + Debug("inst-engine") << "No instantiation given, defer to another engine..." << std::endl; } } } @@ -365,6 +371,15 @@ bool InstantiationEngine::doCbqi( Node f ){ } } +bool InstantiationEngine::isIncomplete( Node f ) { + if( d_i_lte ){ + //TODO : ensure completeness for local theory extensions + //return !d_i_lte->isLocalTheoryExt( f ); + return true; + }else{ + return true; + } +} @@ -449,6 +464,7 @@ InstantiationEngine::Statistics::Statistics(): d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0), d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0), d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0), + d_instantiations_lte("InstantiationEngine::Instantiations_Local_T_Ext", 0), d_instantiation_rounds("InstantiationEngine::Rounds", 0 ) { StatisticsRegistry::registerStat(&d_instantiations_user_patterns); @@ -458,6 +474,7 @@ InstantiationEngine::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith); StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus); StatisticsRegistry::registerStat(&d_instantiations_cbqi_datatypes); + StatisticsRegistry::registerStat(&d_instantiations_lte); StatisticsRegistry::registerStat(&d_instantiation_rounds); } @@ -469,5 +486,6 @@ InstantiationEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith); StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus); StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes); + StatisticsRegistry::unregisterStat(&d_instantiations_lte); StatisticsRegistry::unregisterStat(&d_instantiation_rounds); } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index bf0bb03e1..2fa37ac35 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -26,6 +26,9 @@ namespace quantifiers { class InstStrategyUserPatterns; class InstStrategyAutoGenTriggers; +class InstStrategyLocalTheoryExt; +class InstStrategyFreeVariable; +class InstStrategySimplex; /** instantiation strategy class */ class InstStrategy { @@ -33,7 +36,6 @@ public: enum Status { STATUS_UNFINISHED, STATUS_UNKNOWN, - STATUS_SAT, };/* enum Status */ protected: /** reference to the instantiation engine */ @@ -57,16 +59,6 @@ public: virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; /** process method, returns a status */ virtual int process( Node f, Theory::Effort effort, int e ) = 0; - /** update status */ - static void updateStatus( int& currStatus, int addStatus ){ - if( addStatus==STATUS_UNFINISHED ){ - currStatus = STATUS_UNFINISHED; - }else if( addStatus==STATUS_UNKNOWN ){ - if( currStatus==STATUS_SAT ){ - currStatus = STATUS_UNKNOWN; - } - } - } /** identify */ virtual std::string identify() const { return std::string("Unknown"); } };/* class InstStrategy */ @@ -77,24 +69,19 @@ private: /** instantiation strategies */ std::vector< InstStrategy* > d_instStrategies; /** instantiation strategies active */ - std::map< InstStrategy*, bool > d_instStrategyActive; + //std::map< InstStrategy*, bool > d_instStrategyActive; /** user-pattern instantiation strategy */ InstStrategyUserPatterns* d_isup; /** auto gen triggers; only kept for destructor cleanup */ InstStrategyAutoGenTriggers* d_i_ag; - /** is instantiation strategy active */ - bool isActiveStrategy( InstStrategy* is ) { - return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is]; - } - /** add inst strategy */ - void addInstStrategy( InstStrategy* is ){ - d_instStrategies.push_back( is ); - d_instStrategyActive[is] = true; - } + /** local theory extensions */ + InstStrategyLocalTheoryExt * d_i_lte; + /** full saturate */ + InstStrategyFreeVariable * d_i_fs; + /** simplex (cbqi) */ + InstStrategySimplex * d_i_splx; private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - /** status of instantiation round (one of InstStrategy::STATUS_*) */ - int d_inst_round_status; /** whether the instantiation engine should set incomplete if it cannot answer SAT */ bool d_setIncomplete; /** inst round counter */ @@ -111,6 +98,8 @@ private: bool hasApplyUf( Node f ); /** whether to do CBQI for quantifier f */ bool doCbqi( Node f ); + /** is the engine incomplete for this quantifier */ + bool isIncomplete( Node f ); private: /** do instantiation round */ bool doInstantiationRound( Theory::Effort effort ); @@ -149,6 +138,7 @@ public: IntStat d_instantiations_cbqi_arith; IntStat d_instantiations_cbqi_arith_minus; IntStat d_instantiations_cbqi_datatypes; + IntStat d_instantiations_lte; IntStat d_instantiation_rounds; Statistics(); ~Statistics(); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index f4f1bcd86..dad173ff5 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -5,6 +5,9 @@ module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers +option eMatching --e-matching bool :read-write :default true + whether to do heuristic E-matching + # Whether to mini-scope quantifiers. # For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to # ( forall x. P( x ) ) ^ ( forall x. Q( x ) ) @@ -87,7 +90,7 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" when to apply instantiation -option instMaxLevel --inst-max-level=N int :default -1 +option instMaxLevel --inst-max-level=N int :read-write :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) option instLevelInputOnly --inst-level-input-only bool :default true only input terms are assigned instantiation level zero @@ -190,4 +193,8 @@ option ceGuidedInst --cegqi bool :default false option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h" if and how to apply fairness for cegqi + +option localTheoryExt --local-t-ext bool :default false + do instantiation based on local theory extensions + endmodule diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 9e7d14b9a..5dc8bb384 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -847,21 +847,29 @@ Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) { Node TermDb::getFreeVariableForInstConstant( Node n ){ - TypeNode tn = n.getType(); + return getFreeVariableForType( n.getType() ); +} + +Node TermDb::getFreeVariableForType( TypeNode tn ) { if( d_free_vars.find( tn )==d_free_vars.end() ){ - for( unsigned i=0; imkConst( z ); }else{ - d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar", tn, "is a free variable created by termdb" ); - Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl; + Node n = NodeManager::currentNM()->mkSkolem( "freevar", tn, "is a free variable created by termdb" ); + d_free_vars[tn] = n; + Trace("mkVar") << "FreeVar:: Make variable " << n << " : " << tn << std::endl; + //must set instantiation level attribute to 0 if we are using instantiation max level + if( options::instMaxLevel()!=-1 ){ + QuantifiersEngine::setInstantiationLevelAttr( n, 0 ); + } } } } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 4dca6b36c..2b151bb04 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -279,6 +279,8 @@ public: public: /** get free variable for instantiation constant */ Node getFreeVariableForInstConstant( Node n ); + /** get free variable for type */ + Node getFreeVariableForType( TypeNode tn ); //for triggers private: diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 511103019..65b976b4a 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -47,7 +47,7 @@ d_quantEngine( qe ), d_f( f ){ d_mg->setActiveAdd(true); } }else{ - d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption ); + d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe ); //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); //d_mg->setActiveAdd(); } @@ -385,29 +385,7 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< } } -bool Trigger::isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms ) { - if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){ - bool hasVar = false; - for( unsigned i=0; i& patTerms ) { - std::vector< Node > var_found; - return isLocalTheoryExt2( n, var_found, patTerms ); +bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) { + if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){ + if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){ + bool hasVar = false; + for( unsigned i=0; i& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){ diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 482701a82..28da9f959 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -95,8 +95,6 @@ private: static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false ); /** collect all APPLY_UF pattern terms for f in n */ static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ); - /** is local theory extensions term */ - static bool isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms ); public: //different strategies for choosing trigger terms enum { @@ -113,7 +111,7 @@ public: static bool isSimpleTrigger( Node n ); static bool isBooleanTermTrigger( Node n ); static bool isPureTheoryTrigger( Node n ); - static bool isLocalTheoryExt( Node n, std::vector< Node >& patTerms ); + static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ); /** return data structure for producing matches for this trigger. */ static InstMatchGenerator* getInstMatchGenerator( Node n ); static Node getInversionVariable( Node n ); diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 05eb710df..80fea45fc 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -60,7 +60,8 @@ TESTS = \ bug438.cvc \ bug438b.cvc \ wrong-sel-simp.cvc \ - tenum-bug.smt2 + tenum-bug.smt2 \ + cdt-non-canon-stream.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/cdt-non-canon-stream.smt2 b/test/regress/regress0/datatypes/cdt-non-canon-stream.smt2 new file mode 100644 index 000000000..4a111b41b --- /dev/null +++ b/test/regress/regress0/datatypes/cdt-non-canon-stream.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-codatatypes () ((list (cons (head Int) (tail list))))) + +(declare-fun x () list) +(declare-fun y () list) + +(assert (= x (cons 0 (cons 0 x)))) +(assert (= y (cons 0 y))) +(assert (not (= x y))) +(check-sat) -- 2.30.2