diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-31 11:11:02 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-31 11:11:22 -0500 |
commit | 8fdc49e1bc53fb99050c3c46b9a8ba8541cf851b (patch) | |
tree | 532ae530f41e22437b6b847ee57b99547a662707 /src | |
parent | 61623d7bfb05143e52013db3610b63d632e61d92 (diff) |
Minor change to defaults, update smt comp script, minor changes to options in regressions.
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 13 |
1 files changed, 9 insertions, 4 deletions
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 ); |