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 );
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 );
}
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() ){
if (done() && !fullEffort(e)) {
return;
}
+ d_addedLemma = false;
TimerStat::CodeTimer checkTimer(d_checkTime);
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 );
}
Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl;
d_out->lemma( lem );
+ d_addedLemma = true;
}else{
assertFact( fact, exp );
}
}
//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;
//BoolMap d_consEqc;
/** Are we in conflict */
context::CDO<bool> d_conflict;
+ /** Added lemma ? */
+ bool d_addedLemma;
/** The conflict node */
Node d_conflictNode;
/** cache for which terms we have called collectTerms(...) on */
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();
}
// 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(){}
}
/** 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;
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) */
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
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] << " ";
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() ){
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();
}
}
+
+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; i<f[0].getNumChildren(); i++ ){
+ Node x = d_quantEngine->getTermDatabase()->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; i<patTerms.size(); i++ ){
+ Trace("local-t-ext") << " " << patTerms[i] << std::endl;
+ }
+ Trace("local-t-ext") << std::endl;
+ int matchOption = 0;
+ Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, true, Trigger::TR_GET_OLD, options::smartTriggers() );
+ d_lte_trigger[f] = tr;
+ }else{
+ Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl;
+ Trace("local-t-ext-warn") << "WARNING: not local theory extensions : " << f << std::endl;
+ }
+ d_quant[f] = ret;
+ return ret;
+ }else{
+ return itq->second;
+ }
+}
+
void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
+
}
int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
}
}
}
- return STATUS_UNKNOWN;
}
+ return STATUS_UNKNOWN;
}
std::string identify() const { return std::string("UserPatterns"); }
};/* class InstStrategyUserPatterns */
-class InstStrategyAutoGenTriggers : public InstStrategy{
+class InstStrategyAutoGenTriggers : public InstStrategy {
public:
enum {
RELEVANCE_NONE,
/** 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 */
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 */
std::string identify() const { return std::string("FreeVariable"); }
};/* class InstStrategyFreeVariable */
+
}
}/* CVC4::theory namespace */
}/* CVC4 namespace */
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
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 );
}
}
//reset the instantiators
for( size_t i=0; i<d_instStrategies.size(); ++i ){
InstStrategy* is = d_instStrategies[i];
- if( isActiveStrategy( is ) ){
- is->processResetInstantiationRound( 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; q<d_quantEngine->getModel()->getNumAssertedQuantifiers(); q++ ){
Node f = d_quantEngine->getModel()->getAssertedQuantifier( q );
//check each instantiation strategy
for( size_t i=0; i<d_instStrategies.size(); ++i ){
InstStrategy* is = d_instStrategies[i];
- if( isActiveStrategy( is ) && is->shouldProcess( 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;
+ }
}
}
}
}
//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++;
}
}
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; i<d_quantEngine->getModel()->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;
}
}
}
}
}
+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;
+ }
+}
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);
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);
}
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);
}
class InstStrategyUserPatterns;
class InstStrategyAutoGenTriggers;
+class InstStrategyLocalTheoryExt;
+class InstStrategyFreeVariable;
+class InstStrategySimplex;
/** instantiation strategy class */
class InstStrategy {
enum Status {
STATUS_UNFINISHED,
STATUS_UNKNOWN,
- STATUS_SAT,
};/* enum Status */
protected:
/** reference to the instantiation engine */
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 */
/** 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 */
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 );
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();
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 ) )
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
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
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; i<d_type_map[ tn ].size(); i++ ){
- if( !quantifiers::TermDb::hasInstConstAttr(d_type_map[ tn ][ i ]) ){
- d_free_vars[tn] = d_type_map[ tn ][ i ];
- }
- }
- if( d_free_vars.find( tn )==d_free_vars.end() ){
+ for( unsigned i=0; i<d_type_map[ tn ].size(); i++ ){
+ if( !quantifiers::TermDb::hasInstConstAttr(d_type_map[ tn ][ i ]) ){
+ d_free_vars[tn] = d_type_map[ tn ][ i ];
+ }
+ }
+ if( d_free_vars.find( tn )==d_free_vars.end() ){
//if integer or real, make zero
if( tn.isInteger() || tn.isReal() ){
Rational z(0);
d_free_vars[tn] = NodeManager::currentNM()->mkConst( 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 );
+ }
}
}
}
public:
/** get free variable for instantiation constant */
Node getFreeVariableForInstConstant( Node n );
+ /** get free variable for type */
+ Node getFreeVariableForType( TypeNode tn );
//for triggers
private:
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();
}
}
}
-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<n.getNumChildren(); i++ ){
- if( n[i].getKind()==APPLY_UF ){
- return false;
- }else if( n[i].getKind()==INST_CONSTANT ){
- hasVar = true;
- //if( std::find( var_found.begin(), var_found.end(), n[i]
- }
- }
- if( hasVar ){
- patTerms.push_back( n );
- }
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !isLocalTheoryExt2( n, var_found, patTerms ) ){
- return false;
- }
- }
- }
- return true;
-}
+
bool Trigger::isBooleanTermTrigger( Node n ) {
if( n.getKind()==ITE ){
}
}
-bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& 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<n.getNumChildren(); i++ ){
+ if( n[i].getKind()==INST_CONSTANT ){
+ hasVar = true;
+ if( std::find( vars.begin(), vars.end(), n[i] )==vars.end() ){
+ vars.push_back( n[i] );
+ }else{
+ //do not allow duplicate variables
+ return false;
+ }
+ }else{
+ //do not allow nested function applications
+ return false;
+ }
+ }
+ if( hasVar ){
+ patTerms.push_back( n );
+ }
+ }
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !isLocalTheoryExt( n[i], vars, patTerms ) ){
+ return false;
+ }
+ }
+ }
+ return true;
}
void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){
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 {
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 );
bug438.cvc \
bug438b.cvc \
wrong-sel-simp.cvc \
- tenum-bug.smt2
+ tenum-bug.smt2 \
+ cdt-non-canon-stream.smt2
FAILING_TESTS = \
datatype-dump.cvc
--- /dev/null
+(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)
projects / cvc5.git / commitdiff