diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 27d06e104..fbc5821ce 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1627,35 +1627,6 @@ void SmtEngine::setDefaults() { Theory::setUninterpretedSortOwner(THEORY_UF); } - // Turn on ite simplification for QF_LIA and QF_AUFBV - // WARNING: These checks match much more than just QF_AUFBV and - // QF_LIA logics. --K [2014/10/15] - if(! options::doITESimp.wasSetByUser()) { - bool qf_aufbv = !d_logic.isQuantified() && - d_logic.isTheoryEnabled(THEORY_ARRAYS) && - d_logic.isTheoryEnabled(THEORY_UF) && - d_logic.isTheoryEnabled(THEORY_BV); - bool qf_lia = !d_logic.isQuantified() && - d_logic.isPure(THEORY_ARITH) && - d_logic.isLinear() && - !d_logic.isDifferenceLogic() && - !d_logic.areRealsUsed(); - - bool iteSimp = (qf_aufbv || qf_lia); - Trace("smt") << "setting ite simplification to " << iteSimp << endl; - options::doITESimp.set(iteSimp); - } - if(! options::compressItes.wasSetByUser() ){ - bool qf_lia = !d_logic.isQuantified() && - d_logic.isPure(THEORY_ARITH) && - d_logic.isLinear() && - !d_logic.isDifferenceLogic() && - !d_logic.areRealsUsed(); - - bool compressIte = qf_lia; - Trace("smt") << "setting ite compression to " << compressIte << endl; - options::compressItes.set(compressIte); - } if(! options::simplifyWithCareEnabled.wasSetByUser() ){ bool qf_aufbv = !d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_ARRAYS) && |