diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/options/quantifiers_options | 8 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 38 |
3 files changed, 33 insertions, 30 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 1363626c6..d001684a0 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -99,8 +99,12 @@ option incrementTriggers --increment-triggers bool :default true option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "options/quantifiers_modes.h" :handler stringToInstWhenMode :predicate checkInstWhenMode when to apply instantiation -option instWhenDelayIncrement --inst-when-delay-increment bool :default false - delay incrementing counters for inst-when mode to ensure theory combination and standard quantifier effort strategies take turns +option instWhenStrictInterleave --inst-when-strict-interleave bool :default true :read-write + ensure theory combination and standard quantifier effort strategies take turns +option instWhenPhase --inst-when-phase=N int :read-write :default 2 :read-write + instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen +option instWhenTcFirst --inst-when-tc-first bool :default true :read-write + allow theory combination to happen once initially, before quantifier strategies are run 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) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 93623408e..0a2f50a78 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1683,16 +1683,25 @@ void SmtEngine::setDefaults() { options::sortInference.set( false ); options::ufssFairnessMonotone.set( false ); } + if( d_logic.hasCardinalityConstraints() ){ + //must have finite model finding on + options::finiteModelFind.set( true ); + } + + //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved + if( d_logic.isTheoryEnabled(THEORY_STRINGS) || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ){ + if( !options::instWhenStrictInterleave.wasSetByUser() ){ + options::instWhenStrictInterleave.set( false ); + } + } + //local theory extensions if( options::localTheoryExt() ){ if( !options::instMaxLevel.wasSetByUser() ){ options::instMaxLevel.set( 0 ); } } - if( d_logic.hasCardinalityConstraints() ){ - //must have finite model finding on - options::finiteModelFind.set( true ); - } + if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) { options::fmfBoundInt.set( true ); } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 5d19d603c..568483380 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -138,12 +138,11 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_builder = NULL; d_total_inst_count_debug = 0; - //allow theory combination to go first, once initially, when instWhenDelayIncrement = true - d_ierCounter = options::instWhenDelayIncrement() ? 1 : 0; - d_ierCounter_lc = options::instWhenDelayIncrement() ? 1 : 0; - d_ierCounterLastLc = -1; - //if any strategy called only on last call, use phase 3 - d_inst_when_phase = options::cbqi() ? 3 : 2; + //allow theory combination to go first, once initially + d_ierCounter = options::instWhenTcFirst() ? 0 : 1; + d_ierCounter_lc = 0; + d_ierCounterLastLc = d_ierCounter_lc; + d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() ); } QuantifiersEngine::~QuantifiersEngine(){ @@ -340,13 +339,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl; return; } - if( !options::instWhenDelayIncrement() ){ - if( e==Theory::EFFORT_FULL ){ - d_ierCounter++; - }else if( e==Theory::EFFORT_LAST_CALL ){ - d_ierCounter_lc++; - } - } bool needsCheck = !d_lemmas_waiting.empty(); unsigned needsModelE = QEFFORT_NONE; std::vector< QuantifiersModule* > qm; @@ -470,16 +462,14 @@ void QuantifiersEngine::check( Theory::Effort e ){ break; }else{ if( quant_e==QEFFORT_CONFLICT ){ - if( options::instWhenDelayIncrement() ){ - if( e==Theory::EFFORT_FULL ){ - //increment if a last call happened, or if we already were in phase - if( d_ierCounterLastLc!=d_ierCounter_lc || d_ierCounter%d_inst_when_phase==0 ){ - d_ierCounter++; - d_ierCounterLastLc = d_ierCounter_lc; - } - }else if( e==Theory::EFFORT_LAST_CALL ){ - d_ierCounter_lc++; + if( e==Theory::EFFORT_FULL ){ + //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase + if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){ + d_ierCounter++; + d_ierCounterLastLc = d_ierCounter_lc; } + }else if( e==Theory::EFFORT_LAST_CALL ){ + d_ierCounter_lc++; } }else if( quant_e==QEFFORT_MODEL ){ if( e==Theory::EFFORT_LAST_CALL ){ @@ -1052,9 +1042,9 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){ performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck(); }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){ - performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase==0 ) || e==Theory::EFFORT_LAST_CALL ); + performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL ); }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL ){ - performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase==0 ) || e==Theory::EFFORT_LAST_CALL ); + performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL ); }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){ performCheck = ( e >= Theory::EFFORT_LAST_CALL ); }else{ |