QF_LRA, Quantifiers: enable use decision for (only for) stopping search

1 files changed, 19 insertions, 11 deletions

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;