diff options
author | Tim King <taking@cs.nyu.edu> | 2013-05-06 15:00:34 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-05-06 15:00:34 -0400 |
commit | 5b0b97587e3640567ecd864171b309f39d829358 (patch) | |
tree | 769cdb285693bc48bb82300dc5972033db9ed7f2 /src/smt/smt_engine.cpp | |
parent | d96271f4abcb92c67461080ed33a8aa742c2a0f4 (diff) |
Disables justification stop only for LRA if the problem contains no ites. This is a bandaid for constraints-tempo-width family of benchmarks.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0d473a1a1..75cffefc2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -292,14 +292,13 @@ class SmtEnginePrivate : public NodeManagerListener { */ Node d_modZero; +public: /** * Map from skolem variables to index in d_assertionsToCheck containing * corresponding introduced Boolean ite */ IteSkolemMap d_iteSkolemMap; -public: - /** Instance of the ITE remover */ RemoveITE d_iteRemover; @@ -2534,6 +2533,21 @@ Result SmtEngine::check() { Trace("smt") << "SmtEngine::check(): processing assertions" << endl; d_private->processAssertions(); + // Turn off stop only for QF_LRA + // TODO: Bring up in a meeting where to put this + if(options::decisionStopOnly() && !options::decisionMode.wasSetByUser() ){ + if( // QF_LRA + (not d_logic.isQuantified() && + d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed() + )){ + if(d_private->d_iteSkolemMap.empty()){ + options::decisionStopOnly.set(false); + d_decisionEngine->clearStrategies(); + Trace("smt") << "SmtEngine::check(): turning off stop only" << endl; + } + } + } + unsigned long millis = 0; if(d_timeBudgetCumulative != 0) { millis = getTimeRemaining(); |