From 863541c547df629e680d9497ae15717e0de1f73c Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Mon, 18 Jun 2012 01:46:39 +0000 Subject: QF_LRA, Quantifiers: enable use decision for (only for) stopping search --- src/smt/smt_engine.cpp | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) (limited to 'src/smt/smt_engine.cpp') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3ad12cc78..b9c15ac71 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -552,41 +552,49 @@ 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 + // and also use it in stop-only mode for QF_AUFLIA, QF_LRA and Quantifiers if(!Options::current()->decisionModeSetByUser) { Options::DecisionMode decMode = //QF_BV - ( !d_logic.isQuantified() && + (not d_logic.isQuantified() && d_logic.isPure(THEORY_BV) ) || //QF_AUFBV - (!d_logic.isQuantified() && + (not d_logic.isQuantified() && 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() && + (not d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_ARITH) - ) + ) || + // QF_LRA + (not d_logic.isQuantified() && + d_logic.isPure(THEORY_ARITH) + ) || + // Quantifiers + d_logic.isQuantified() ? Options::DECISION_STRATEGY_JUSTIFICATION : Options::DECISION_STRATEGY_INTERNAL; bool stoponly = // QF_AUFLIA - (!d_logic.isQuantified() && + (not d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_ARITH) - ) + ) || + // QF_LRA + (not d_logic.isQuantified() && + d_logic.isPure(THEORY_ARITH) + ) || + // Quantifiers + d_logic.isQuantified() ? 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; -- cgit v1.2.3