Brings the tuning branch into trunk. This includes the changes from restricted-simplex.

1 files changed, 30 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4887ef540..b91272d64 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -490,6 +490,36 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
     Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl;
     NodeManager::currentNM()->getOptions()->arithRewriteEq = arithRewriteEq;
   }
+  if(!  Options::current()->arithHeuristicPivotsSetByUser){
+    int16_t heuristicPivots = 5;
+    if(d_logic.isPure(theory::THEORY_ARITH) && !d_logic.isQuantified()){
+      if(d_logic.isDifferenceLogic()){
+        heuristicPivots = -1;
+      }else if(!d_logic.areIntegersUsed()){
+        heuristicPivots = 0;
+      }
+    }
+    Trace("smt") << "setting arithHeuristicPivots  " << heuristicPivots << std::endl;
+    NodeManager::currentNM()->getOptions()->arithHeuristicPivots = heuristicPivots;
+  }
+  if(! Options::current()->arithPivotThresholdSetByUser){
+    uint16_t pivotThreshold = 2;
+    if(d_logic.isPure(theory::THEORY_ARITH) && !d_logic.isQuantified()){
+      if(d_logic.isDifferenceLogic()){
+        pivotThreshold = 16;
+      }
+    }
+    Trace("smt") << "setting arith arithPivotThreshold  " << pivotThreshold << std::endl;
+    NodeManager::currentNM()->getOptions()->arithPivotThreshold = pivotThreshold;
+  }
+  if(! Options::current()->arithStandardCheckVarOrderPivotsSetByUser){
+    int16_t varOrderPivots = -1;
+    if(d_logic.isPure(theory::THEORY_ARITH) && !d_logic.isQuantified()){
+      varOrderPivots = 200;
+    }
+    Trace("smt") << "setting arithStandardCheckVarOrderPivots  " << varOrderPivots << std::endl;
+    NodeManager::currentNM()->getOptions()->arithStandardCheckVarOrderPivots = varOrderPivots;
+  }
   // Turn off early theory preprocessing if arithRewriteEq is on
   if (NodeManager::currentNM()->getOptions()->arithRewriteEq) {
     d_earlyTheoryPP = false;