diff options
author | Tim King <taking@cs.nyu.edu> | 2012-06-14 04:39:43 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-06-14 04:39:43 +0000 |
commit | a8f1f0e2cef69acd278f859fe32a2df7852256e0 (patch) | |
tree | 70f590c29e7224ca8c34a53fb44c456baa5baa9c /src/smt | |
parent | d192b7f7aed685e89053bd0f0a4c3e42f1136b80 (diff) |
Brings the tuning branch into trunk. This includes the changes from restricted-simplex.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 30 |
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; |