From f653df8f015e38bbe2dd39fb3852afa6fe0d89da Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Sun, 17 Jun 2012 23:02:01 +0000 Subject: [PATCH] QF_AUFLIA: enable use decision for (only for) stopping search --- src/smt/smt_engine.cpp | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) 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) -- 2.30.2