diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-17 23:02:01 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-17 23:02:01 +0000 |
| commit | f653df8f015e38bbe2dd39fb3852afa6fe0d89da (patch) | |
| tree | 41c8fe8c8c5c83dd6bbd3de6498382a02ade40f9 /src/smt | |
| parent | 8ac3a5f6bcab217186afb8a8143d342209fc273c (diff) | |
QF_AUFLIA: enable use decision for (only for) stopping search
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6567a775b..3ad12cc78 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -552,6 +552,7 @@ void SmtEngine::setLogicInternal() throw(AssertionException) { d_earlyTheoryPP = false; } // Turn on justification heuristic of the decision engine for QF_BV and QF_AUFBV + // and also use it in stop-only mode for QF_AUFLIA if(!Options::current()->decisionModeSetByUser) { Options::DecisionMode decMode = //QF_BV @@ -563,13 +564,33 @@ void SmtEngine::setLogicInternal() throw(AssertionException) { d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV) + ) || + //QF_AUFLIA (and may be ends up enabling QF_AUFLRA?) + (!d_logic.isQuantified() && + d_logic.isTheoryEnabled(THEORY_ARRAY) && + d_logic.isTheoryEnabled(THEORY_UF) && + d_logic.isTheoryEnabled(THEORY_ARITH) ) ? Options::DECISION_STRATEGY_JUSTIFICATION : Options::DECISION_STRATEGY_INTERNAL; + + bool stoponly = + // QF_AUFLIA + (!d_logic.isQuantified() && + d_logic.isTheoryEnabled(THEORY_ARRAY) && + d_logic.isTheoryEnabled(THEORY_UF) && + d_logic.isTheoryEnabled(THEORY_ARITH) + ) + ? true : false; + + // Turn on justification-stoponly for QF_AUFLIA + if(!Options::current()->decisionModeSetByUser) + + Trace("smt") << "setting decision mode to " << decMode << std::endl; NodeManager::currentNM()->getOptions()->decisionMode = decMode; + NodeManager::currentNM()->getOptions()->decisionOptions.stopOnly = stoponly; } - } void SmtEngine::setInfo(const std::string& key, const SExpr& value) |