From fd3844131f334e929bfb04eb2dcb6229cf1190cd Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 12 Mar 2016 10:38:36 -0600 Subject: [PATCH] Add options related to interleaving quantifiers and theory combination, changes default behavior. --- src/options/quantifiers_options | 8 +++- src/smt/smt_engine.cpp | 17 +++++++-- src/theory/quantifiers_engine.cpp | 38 +++++++------------ test/regress/regress0/quantifiers/Makefile.am | 27 +++++++------ 4 files changed, 46 insertions(+), 44 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{ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 6e7b25286..e8000eff1 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -38,10 +38,9 @@ TESTS = \ gauss_init_0030.fof.smt2 \ qcft-javafe.filespace.TreeWalker.006.smt2 \ qcft-smtlib3dbc51.smt2 \ - symmetric_unsat_7.smt2 \ javafe.ast.StmtVec.009.smt2 \ ARI176e1.smt2 \ - bi-artm-s.smt2 \ + bi-artm-s.smt2 \ simp-typ-test.smt2 \ macros-int-real.smt2 \ stream-x2014-09-18-unsat.smt2 \ @@ -65,18 +64,18 @@ TESTS = \ ext-ex-deq-trigger.smt2 \ matching-lia-1arg.smt2 \ RND_4_16.smt2 \ - cdt-0208-to.smt2 \ - psyco-196.smt2 \ - agg-rew-test.smt2 \ - agg-rew-test-cf.smt2 \ - rew-to-0211-dd.smt2 \ - rew-to-scala.smt2 \ - macro-subtype-param.smt2 \ - macros-real-arg.smt2 \ - subtype-param-unk.smt2 \ - subtype-param.smt2 \ - anti-sk-simp.smt2 \ - pure_dt_cbqi.smt2 + cdt-0208-to.smt2 \ + psyco-196.smt2 \ + agg-rew-test.smt2 \ + agg-rew-test-cf.smt2 \ + rew-to-0211-dd.smt2 \ + rew-to-scala.smt2 \ + macro-subtype-param.smt2 \ + macros-real-arg.smt2 \ + subtype-param-unk.smt2 \ + subtype-param.smt2 \ + anti-sk-simp.smt2 \ + pure_dt_cbqi.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine -- 2.30.2