Disables justification stop only for LRA if the problem contains no ites. This is...

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 687515ff0d4d92e136dd243a92af33c141a1f2be..f634a28d9a7f16ef75aada41c1fb2f055f96b08c 100644 (file)
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -82,6 +82,13 @@ void DecisionEngine::enableStrategy(DecisionStrategy* ds)
   d_enabledStrategies.push_back(ds);
 }
 
+void DecisionEngine::clearStrategies(){
+  for(unsigned i = 0; i < d_enabledStrategies.size(); ++i){
+    delete d_enabledStrategies[i];
+  }
+  d_enabledStrategies.clear();
+  d_needIteSkolemMap.clear();
+}
 
 bool DecisionEngine::isRelevant(SatVariable var)
 {

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index bc071f7f6ef2e63efc7b350eb0ccc76c6009d8c7..f28b13774a8b642580a94edb714ef0b25e1c294f 100644 (file)
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -96,6 +96,10 @@ public:
   /* enables decision stragies based on options */
   void init();
 
+  /* clears all of the strategies */
+  void clearStrategies();
+
+
   /**
    * This is called by SmtEngine, at shutdown time, just before
    * destruction.  It is important because there are destruction
@@ -106,8 +110,7 @@ public:
     d_engineState = 2;
 
     Trace("decision") << "Shutting down decision engine" << std::endl;
-    for(unsigned i = 0; i < d_enabledStrategies.size(); ++i)
-      delete d_enabledStrategies[i];
+    clearStrategies();
   }
 
   // Interface for External World to use our services

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0d473a1a1f4a9209b7ded9bce2037fa7b3a8cf36..75cffefc25683d5d419035430730d89787d3c872 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -292,14 +292,13 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   Node d_modZero;
 
+public:
   /**
    * Map from skolem variables to index in d_assertionsToCheck containing
    * corresponding introduced Boolean ite
    */
   IteSkolemMap d_iteSkolemMap;
 
-public:
-
   /** Instance of the ITE remover */
   RemoveITE d_iteRemover;
 
@@ -2534,6 +2533,21 @@ Result SmtEngine::check() {
   Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
   d_private->processAssertions();
 
+  // Turn off stop only for QF_LRA
+  // TODO: Bring up in a meeting where to put this
+  if(options::decisionStopOnly() && !options::decisionMode.wasSetByUser() ){
+    if( // QF_LRA
+       (not d_logic.isQuantified() &&
+        d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
+        )){
+      if(d_private->d_iteSkolemMap.empty()){
+        options::decisionStopOnly.set(false);
+        d_decisionEngine->clearStrategies();
+        Trace("smt") << "SmtEngine::check(): turning off stop only" << endl;
+      }
+    }
+  }
+
   unsigned long millis = 0;
   if(d_timeBudgetCumulative != 0) {
     millis = getTimeRemaining();