diff options
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; |