From 8fdc49e1bc53fb99050c3c46b9a8ba8541cf851b Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 31 May 2017 11:11:02 -0500 Subject: Minor change to defaults, update smt comp script, minor changes to options in regressions. --- src/smt/smt_engine.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b5fbecf7d..ace33a164 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1852,8 +1852,10 @@ void SmtEngine::setDefaults() { } //counterexample-guided instantiation for non-sygus // enable if any possible quantifiers with arithmetic, datatypes or bitvectors - if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) || - options::cbqiAll() ){ + if( d_logic.isQuantified() && + ( ( options::decisionMode()!=decision::DECISION_STRATEGY_INTERNAL && + ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) || + options::cbqiAll() ) ){ if( !options::cbqi.wasSetByUser() ){ options::cbqi.set( true ); } @@ -1889,11 +1891,14 @@ void SmtEngine::setDefaults() { if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } - if( options::cbqiNestedQE() ){ - //only sound with prenex = disj_normal or normal + if( options::cbqi() && + ( options::cbqiNestedQE() || options::decisionMode()==decision::DECISION_STRATEGY_INTERNAL ) ){ + //only complete with prenex = disj_normal or normal if( options::prenexQuant()<=quantifiers::PRENEX_QUANT_DISJ_NORMAL ){ options::prenexQuant.set( quantifiers::PRENEX_QUANT_DISJ_NORMAL ); } + } + if( options::cbqiNestedQE() ){ options::prenexQuantUser.set( true ); if( !options::preSkolemQuant.wasSetByUser() ){ options::preSkolemQuant.set( true ); -- cgit v1.2.3