From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Sun, 17 Jun 2012 23:02:01 +0000 (+0000)
Subject: QF_AUFLIA: enable use decision for (only for) stopping search
X-Git-Tag: cvc5-1.0.0~7981
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f653df8f015e38bbe2dd39fb3852afa6fe0d89da;p=cvc5.git

QF_AUFLIA: enable use decision for (only for) stopping search
---

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)