diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-04 13:58:14 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-04 11:58:14 -0700 |
| commit | db491e2e8100101f30e3f211a3c5da55686f7d27 (patch) | |
| tree | 15907815b8231b7761f131d2ec96c8e82246f0d6 /src/smt | |
| parent | 8b7a4af93226b2ecb82814a7609855deea0230cd (diff) | |
Enable cegqi (with model values) for floating point by default (#2023)
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9d10e72be..2836f73b4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2071,11 +2071,15 @@ 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.isPure(THEORY_ARITH) || d_logic.isPure(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) + || d_logic.isTheoryEnabled(THEORY_FP))) + || d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV) + || options::cbqiAll())) + { if( !options::cbqi.wasSetByUser() ){ options::cbqi.set( true ); } |