diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-05 11:13:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-05 11:13:39 -0500 |
| commit | 1bd02cac69871158d71c74b23aa94c99cd69bead (patch) | |
| tree | 7675faf1a4c21d40744f3a1dc067964eb1b6ada5 /src/smt | |
| parent | 044fb6315119e0ad2f1ce57354f72d20ff4c6dc7 (diff) | |
Update default options for sygus (#2586)
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 78 |
1 files changed, 40 insertions, 38 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 11c03de6c..334879993 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1634,35 +1634,40 @@ void SmtEngine::setDefaults() { // Set decision mode based on logic (if not set by user) if(!options::decisionMode.wasSetByUser()) { decision::DecisionMode decMode = - // ALL - d_logic.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION : - ( // QF_BV - (not d_logic.isQuantified() && - d_logic.isPure(THEORY_BV) - ) || - // QF_AUFBV or QF_ABV or QF_UFBV - (not d_logic.isQuantified() && - (d_logic.isTheoryEnabled(THEORY_ARRAYS) || - d_logic.isTheoryEnabled(THEORY_UF)) && - d_logic.isTheoryEnabled(THEORY_BV) - ) || - // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?) - (not d_logic.isQuantified() && - d_logic.isTheoryEnabled(THEORY_ARRAYS) && - d_logic.isTheoryEnabled(THEORY_UF) && - d_logic.isTheoryEnabled(THEORY_ARITH) - ) || - // QF_LRA - (not d_logic.isQuantified() && - d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed() - ) || - // Quantifiers - d_logic.isQuantified() || - // Strings - d_logic.isTheoryEnabled(THEORY_STRINGS) - ? decision::DECISION_STRATEGY_JUSTIFICATION - : decision::DECISION_STRATEGY_INTERNAL - ); + // sygus uses internal + is_sygus ? decision::DECISION_STRATEGY_INTERNAL : + // ALL + d_logic.hasEverything() + ? decision::DECISION_STRATEGY_JUSTIFICATION + : ( // QF_BV + (not d_logic.isQuantified() && d_logic.isPure(THEORY_BV)) + || + // QF_AUFBV or QF_ABV or QF_UFBV + (not d_logic.isQuantified() + && (d_logic.isTheoryEnabled(THEORY_ARRAYS) + || d_logic.isTheoryEnabled(THEORY_UF)) + && d_logic.isTheoryEnabled(THEORY_BV)) + || + // QF_AUFLIA (and may be ends up enabling + // QF_AUFLRA?) + (not d_logic.isQuantified() + && d_logic.isTheoryEnabled(THEORY_ARRAYS) + && d_logic.isTheoryEnabled(THEORY_UF) + && d_logic.isTheoryEnabled(THEORY_ARITH)) + || + // QF_LRA + (not d_logic.isQuantified() + && d_logic.isPure(THEORY_ARITH) + && d_logic.isLinear() + && !d_logic.isDifferenceLogic() + && !d_logic.areIntegersUsed()) + || + // Quantifiers + d_logic.isQuantified() || + // Strings + d_logic.isTheoryEnabled(THEORY_STRINGS) + ? decision::DECISION_STRATEGY_JUSTIFICATION + : decision::DECISION_STRATEGY_INTERNAL); bool stoponly = // ALL @@ -1895,13 +1900,11 @@ void SmtEngine::setDefaults() { //counterexample-guided instantiation for non-sygus // enable if any possible quantifiers with arithmetic, datatypes or bitvectors 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) - || d_logic.isTheoryEnabled(THEORY_FP))) - || d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV) - || options::cbqiAll())) + && (d_logic.isTheoryEnabled(THEORY_ARITH) + || d_logic.isTheoryEnabled(THEORY_DATATYPES) + || d_logic.isTheoryEnabled(THEORY_BV) + || d_logic.isTheoryEnabled(THEORY_FP)) + || options::cbqiAll()) { if( !options::cbqi.wasSetByUser() ){ options::cbqi.set( true ); @@ -1942,8 +1945,7 @@ void SmtEngine::setDefaults() { options::cbqiNestedQE.set(false); } // prenexing - if (options::cbqiNestedQE() - || options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) + if (options::cbqiNestedQE()) { // only complete with prenex = disj_normal or normal if (options::prenexQuant() <= quantifiers::PRENEX_QUANT_DISJ_NORMAL) |