From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 18 Jun 2012 01:46:39 +0000 (+0000)
Subject: QF_LRA, Quantifiers: enable use decision for (only for) stopping search
X-Git-Tag: cvc5-1.0.0~7979
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=863541c547df629e680d9497ae15717e0de1f73c;p=cvc5.git

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

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;