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;
void ArithPriorityQueue::transitionToCollectionMode() {
Assert(inDifferenceMode() || inVariableOrderMode());
- Assert(d_diffQueue.empty());
Assert(d_candidates.empty());
+
+ if(inDifferenceMode()){
+ Assert(d_varSet.empty());
+ Assert(d_varOrderQueue.empty());
+ Assert(inDifferenceMode());
+
+ DifferenceArray::const_iterator i = d_diffQueue.begin(), end = d_diffQueue.end();
+ for(; i != end; ++i){
+ ArithVar var = (*i).variable();
+ if(basicAndInconsistent(var) && !d_varSet.isMember(var)){
+ d_candidates.push_back(var);
+ d_varSet.add(var);
+ }
+ }
+ d_diffQueue.clear();
+ }else{
+ Assert(d_diffQueue.empty());
+ Assert(inVariableOrderMode());
+
+ d_varSet.purge();
+
+ ArithVarArray::const_iterator i = d_varOrderQueue.begin(), end = d_varOrderQueue.end();
+ for(; i != end; ++i){
+ ArithVar var = *i;
+ if(basicAndInconsistent(var)){
+ d_candidates.push_back(var);
+ d_varSet.add(var); // cannot have duplicates.
+ }
+ }
+ d_varOrderQueue.clear();
+ }
+
+ Assert(d_diffQueue.empty());
Assert(d_varOrderQueue.empty());
- Assert(d_varSet.empty());
Debug("arith::priorityqueue") << "transitionToCollectionMode()" << endl;
*/
ArithVarArray d_varOrderQueue;
+ /**
+ * A superset of the basic variables that may be inconsistent.
+ * This is empty during DiffOrderMode, and otherwise it is the same set as candidates
+ * or varOrderQueue.
+ */
DenseSet d_varSet;
/**
return getHead().isConstant();
}
+ uint32_t size() const{
+ if(singleton()){
+ return 1;
+ }else{
+ Assert(getNode().getKind() == kind::PLUS);
+ return getNode().getNumChildren();
+ }
+ }
+
Monomial getHead() const {
return *(begin());
}
using namespace CVC4::theory;
using namespace CVC4::theory::arith;
-
-static const uint32_t NUM_CHECKS = 10;
static const bool CHECK_AFTER_PIVOT = true;
-static const uint32_t VARORDER_CHECK_PERIOD = 200;
SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, NodeCallBack& conflictChannel) :
d_conflictVariable(ARITHVAR_SENTINEL),
d_pivotsInRound(),
d_DELTA_ZERO(0,0)
{
- switch(Options::ArithPivotRule rule = Options::current()->arithPivotRule) {
+ switch(Options::ArithHeuristicPivotRule rule = Options::current()->arithHeuristicPivotRule) {
case Options::MINIMUM:
d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
break;
}
}
-bool SimplexDecisionProcedure::findModel(){
+Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){
Assert(d_conflictVariable == ARITHVAR_SENTINEL);
if(d_queue.empty()){
- return false;
+ return Result::SAT;
}
- bool foundConflict = false;
-
static CVC4_THREADLOCAL(unsigned int) instance = 0;
instance = instance + 1;
Debug("arith::findModel") << "begin findModel()" << instance << endl;
d_queue.transitionToDifferenceMode();
- if(d_queue.size() > 1){
- foundConflict = findConflictOnTheQueue(BeforeDiffSearch);
+ Result::Sat result = Result::SAT_UNKNOWN;
+
+ if(d_queue.empty()){
+ result = Result::SAT;
+ }else if(d_queue.size() > 1){
+ if(findConflictOnTheQueue(BeforeDiffSearch)){
+ result = Result::UNSAT;
+ }
}
- if(!foundConflict){
- uint32_t numHeuristicPivots = d_numVariables + 1;
- uint32_t pivotsRemaining = numHeuristicPivots;
- uint32_t pivotsPerCheck = (numHeuristicPivots/NUM_CHECKS) + (NUM_CHECKS-1);
+ static const bool verbose = false;
+ exactResult |= Options::current()->arithStandardCheckVarOrderPivots < 0;
+ const uint32_t inexactResultsVarOrderPivots = exactResult ? 0 : Options::current()->arithStandardCheckVarOrderPivots;
+
+ uint32_t checkPeriod = Options::current()->arithSimplexCheckPeriod;
+ if(result == Result::SAT_UNKNOWN){
+ uint32_t numDifferencePivots = Options::current()->arithHeuristicPivots < 0 ?
+ d_numVariables + 1 : Options::current()->arithHeuristicPivots;
+ // The signed to unsigned conversion is safe.
+ uint32_t pivotsRemaining = numDifferencePivots;
while(!d_queue.empty() &&
- !foundConflict &&
+ result != Result::UNSAT &&
pivotsRemaining > 0){
- uint32_t pivotsToDo = min(pivotsPerCheck, pivotsRemaining);
- foundConflict = searchForFeasibleSolution(pivotsToDo);
+ uint32_t pivotsToDo = min(checkPeriod, pivotsRemaining);
pivotsRemaining -= pivotsToDo;
- //Once every CHECK_PERIOD examine the entire queue for conflicts
- if(!foundConflict){
- foundConflict = findConflictOnTheQueue(DuringDiffSearch);
+ if(searchForFeasibleSolution(pivotsToDo)){
+ result = Result::UNSAT;
+ }//Once every CHECK_PERIOD examine the entire queue for conflicts
+ if(result != Result::UNSAT){
+ if(findConflictOnTheQueue(DuringDiffSearch)) { result = Result::UNSAT; }
}else{
- findConflictOnTheQueue(AfterDiffSearch);
+ findConflictOnTheQueue(AfterDiffSearch); // already unsat
+ }
+ }
+
+ if(verbose && numDifferencePivots > 0){
+ if(result == Result::UNSAT){
+ cout << "diff order found unsat" << endl;
+ }else if(d_queue.empty()){
+ cout << "diff order found model" << endl;
+ }else{
+ cout << "diff order missed" << endl;
}
}
}
- if(!d_queue.empty() && !foundConflict){
- d_queue.transitionToVariableOrderMode();
+ if(!d_queue.empty() && result != Result::UNSAT){
+ if(exactResult){
+ d_queue.transitionToVariableOrderMode();
- while(!d_queue.empty() && !foundConflict){
- foundConflict = searchForFeasibleSolution(VARORDER_CHECK_PERIOD);
+ while(!d_queue.empty() && result != Result::UNSAT){
+ if(searchForFeasibleSolution(checkPeriod)){
+ result = Result::UNSAT;
+ }
- //Once every CHECK_PERIOD examine the entire queue for conflicts
- if(!foundConflict){
- foundConflict = findConflictOnTheQueue(DuringVarOrderSearch);
- } else{
- findConflictOnTheQueue(AfterVarOrderSearch);
+ //Once every CHECK_PERIOD examine the entire queue for conflicts
+ if(result != Result::UNSAT){
+ if(findConflictOnTheQueue(DuringVarOrderSearch)){
+ result = Result::UNSAT;
+ }
+ } else{
+ findConflictOnTheQueue(AfterVarOrderSearch);
+ }
+ }
+ if(verbose){
+ if(result == Result::UNSAT){
+ cout << "bland found unsat" << endl;
+ }else if(d_queue.empty()){
+ cout << "bland found model" << endl;
+ }else{
+ cout << "bland order missed" << endl;
+ }
+ }
+ }else{
+ d_queue.transitionToVariableOrderMode();
+
+ if(searchForFeasibleSolution(inexactResultsVarOrderPivots)){
+ result = Result::UNSAT;
+ findConflictOnTheQueue(AfterVarOrderSearch); // already unsat
+ }else{
+ if(findConflictOnTheQueue(AfterVarOrderSearch)) { result = Result::UNSAT; }
+ }
+
+ if(verbose){
+ if(result == Result::UNSAT){
+ cout << "restricted var order found unsat" << endl;
+ }else if(d_queue.empty()){
+ cout << "restricted var order found model" << endl;
+ }else{
+ cout << "restricted var order missed" << endl;
+ }
}
}
}
- Assert(foundConflict || d_queue.empty());
+ if(result == Result::SAT_UNKNOWN && d_queue.empty()){
+ result = Result::SAT;
+ }
+
+
- // Curiously the invariant that we always do a full check
- // means that the assignment we can always empty these queues.
- d_queue.clear();
d_pivotsInRound.purge();
d_conflictVariable = ARITHVAR_SENTINEL;
- Assert(!d_queue.inCollectionMode());
d_queue.transitionToCollectionMode();
+ Assert(d_queue.inCollectionMode());
+ Debug("arith::findModel") << "end findModel() " << instance << " " << result << endl;
+ return result;
- Assert(d_queue.inCollectionMode());
+ // Assert(foundConflict || d_queue.empty());
+
+ // // Curiously the invariant that we always do a full check
+ // // means that the assignment we can always empty these queues.
+ // d_queue.clear();
+ // d_pivotsInRound.purge();
+ // d_conflictVariable = ARITHVAR_SENTINEL;
+
+ // Assert(!d_queue.inCollectionMode());
+ // d_queue.transitionToCollectionMode();
+
+
+ // Assert(d_queue.inCollectionMode());
- Debug("arith::findModel") << "end findModel() " << instance << endl;
+ // Debug("arith::findModel") << "end findModel() " << instance << endl;
- return foundConflict;
+ // return foundConflict;
}
Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
#include "util/dense_map.h"
#include "util/options.h"
#include "util/stats.h"
+#include "util/result.h"
#include <queue>
*
* Corresponds to the "check()" procedure in [Cav06].
*/
- bool findModel();
+ Result::Sat findModel(bool exactResult);
private:
public:
void increaseMax() {d_numVariables++;}
+
+ void clearQueue() {
+ d_queue.clear();
+ }
+
private:
/** Reports a conflict to on the output channel. */
TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe),
+ d_qflraStatus(Result::SAT_UNKNOWN),
+ d_unknownsInARow(0),
d_hasDoneWorkSinceCut(false),
d_learner(d_pbSubstitutions),
d_setupLiteralCallback(this),
d_restartTimer("theory::arith::restartTimer"),
d_boundComputationTime("theory::arith::bound::time"),
d_boundComputations("theory::arith::bound::boundComputations",0),
- d_boundPropagations("theory::arith::bound::boundPropagations",0)
+ d_boundPropagations("theory::arith::bound::boundPropagations",0),
+ d_unknownChecks("theory::arith::status::unknowns", 0),
+ d_maxUnknownsInARow("theory::arith::status::maxUnknownsInARow", 0),
+ d_avgUnknownsInARow("theory::arith::status::avgUnknownsInARow"),
+ d_revertsOnConflicts("theory::arith::status::revertsOnConflicts",0),
+ d_commitsOnConflicts("theory::arith::status::commitsOnConflicts",0),
+ d_nontrivialSatChecks("theory::arith::status::nontrivialSatChecks",0)
{
StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
StatisticsRegistry::registerStat(&d_boundComputationTime);
StatisticsRegistry::registerStat(&d_boundComputations);
StatisticsRegistry::registerStat(&d_boundPropagations);
+
+ StatisticsRegistry::registerStat(&d_unknownChecks);
+ StatisticsRegistry::registerStat(&d_maxUnknownsInARow);
+ StatisticsRegistry::registerStat(&d_avgUnknownsInARow);
+ StatisticsRegistry::registerStat(&d_revertsOnConflicts);
+ StatisticsRegistry::registerStat(&d_commitsOnConflicts);
+ StatisticsRegistry::registerStat(&d_nontrivialSatChecks);
}
TheoryArith::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_boundComputationTime);
StatisticsRegistry::unregisterStat(&d_boundComputations);
StatisticsRegistry::unregisterStat(&d_boundPropagations);
+
+ StatisticsRegistry::unregisterStat(&d_unknownChecks);
+ StatisticsRegistry::unregisterStat(&d_maxUnknownsInARow);
+ StatisticsRegistry::unregisterStat(&d_avgUnknownsInARow);
+ StatisticsRegistry::unregisterStat(&d_revertsOnConflicts);
+ StatisticsRegistry::unregisterStat(&d_commitsOnConflicts);
+ StatisticsRegistry::unregisterStat(&d_nontrivialSatChecks);
}
void TheoryArith::revertOutOfConflict(){
// Add the substitution if not recursive
Assert(elim == Rewriter::rewrite(elim));
- if(elim.hasSubterm(minVar)){
+
+ static const int MAX_SUB_SIZE = 20;
+ if(false && right.size() > MAX_SUB_SIZE){
+ Debug("simplify") << "TheoryArith::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl;
+ Debug("simplify") << right.size() << endl;
+ }else if(elim.hasSubterm(minVar)){
Debug("simplify") << "TheoryArith::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl;
}else if (!minVar.getType().isInteger() || right.isIntegral()) {
Assert(!elim.hasSubterm(minVar));
void TheoryArith::check(Effort effortLevel){
Assert(d_currentPropagationList.empty());
- Debug("arith") << "TheoryArith::check begun" << std::endl;
+ Debug("effortlevel") << "TheoryArith::check " << effortLevel << std::endl;
+ Debug("arith") << "TheoryArith::check begun " << effortLevel << std::endl;
+
+ bool newFacts = !done();
+ Result::Sat previous = d_qflraStatus;
+ if(newFacts){
+ d_qflraStatus = Result::SAT_UNKNOWN;
+ d_hasDoneWorkSinceCut = true;
+ }
- d_hasDoneWorkSinceCut = d_hasDoneWorkSinceCut || !done();
while(!done()){
Constraint curr = constraintFromFactQueue();
if(curr != NullConstraint){
if(inConflict()){
revertOutOfConflict();
outputConflicts();
+ d_qflraStatus = Result::UNSAT;
return;
}
}
Assert(!res || inConflict());
if(inConflict()){
+ d_qflraStatus = Result::UNSAT;
revertOutOfConflict();
outputConflicts();
return;
}
bool emmittedConflictOrSplit = false;
+
+
Assert(d_conflicts.empty());
- bool foundConflict = d_simplex.findModel();
- if(foundConflict){
- revertOutOfConflict();
+
+ d_qflraStatus = d_simplex.findModel(fullEffort(effortLevel));
+ switch(d_qflraStatus){
+ case Result::SAT:
+ if(newFacts){
+ ++d_statistics.d_nontrivialSatChecks;
+ }
+ d_partialModel.commitAssignmentChanges();
+ d_unknownsInARow = 0;
+ break;
+ case Result::SAT_UNKNOWN:
+ ++d_unknownsInARow;
+ ++(d_statistics.d_unknownChecks);
+ Assert(!fullEffort(effortLevel));
+ d_partialModel.commitAssignmentChanges();
+ d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow);
+ break;
+ case Result::UNSAT:
+ d_unknownsInARow = 0;
+ if(previous == Result::SAT){
+ ++d_statistics.d_revertsOnConflicts;
+
+ revertOutOfConflict();
+ d_simplex.clearQueue();
+ }else{
+ ++d_statistics.d_commitsOnConflicts;
+
+ d_partialModel.commitAssignmentChanges();
+ revertOutOfConflict();
+ }
outputConflicts();
emmittedConflictOrSplit = true;
- }else{
- d_partialModel.commitAssignmentChanges();
+ break;
+ default:
+ Unimplemented();
}
+ d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow);
+ // This should be fine if sat or unknown
if(!emmittedConflictOrSplit &&
(Options::current()->arithPropagationMode == Options::UNATE_PROP ||
Options::current()->arithPropagationMode == Options::BOTH_PROP)){
TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
+ Assert(d_qflraStatus != Result::UNSAT);
while(!d_currentPropagationList.empty() && !inConflict()){
Constraint curr = d_currentPropagationList.front();
}
}
+
+
Node TheoryArith::explain(TNode n) {
Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
void TheoryArith::propagate(Effort e) {
- if((Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP ||
+ // This uses model values for safety. Disable for now.
+ if(d_qflraStatus == Result::SAT &&
+ (Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP ||
Options::current()->arithPropagationMode == Options::BOTH_PROP)
&& hasAnyUpdates()){
propagateCandidates();
}
bool TheoryArith::getDeltaAtomValue(TNode n) {
+ Assert(d_qflraStatus != Result::SAT_UNKNOWN);
switch (n.getKind()) {
case kind::EQUAL: // 2 args
DeltaRational TheoryArith::getDeltaValue(TNode n) {
-
+ Assert(d_qflraStatus != Result::SAT_UNKNOWN);
Debug("arith::value") << n << std::endl;
switch(n.getKind()) {
}
EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
- if (getDeltaValue(a) == getDeltaValue(b)) {
+ if(d_qflraStatus == Result::SAT_UNKNOWN){
+ return EQUALITY_UNKNOWN;
+ }else if (getDeltaValue(a) == getDeltaValue(b)) {
return EQUALITY_TRUE_IN_MODEL;
} else {
return EQUALITY_FALSE_IN_MODEL;
#include "theory/arith/constraint.h"
#include "util/stats.h"
+#include "util/result.h"
#include <vector>
#include <map>
class TheoryArith : public Theory {
friend class InstantiatorTheoryArith;
private:
+ enum Result::Sat d_qflraStatus;
+ // check()
+ // !done() -> d_qflraStatus = Unknown
+ // fullEffort(e) -> simplex returns either sat or unsat
+ // !fullEffort(e) -> simplex returns either sat, unsat or unknown
+ // if unknown, save the assignment
+ // if unknown, the simplex priority queue cannot be emptied
+ int d_unknownsInARow;
+
bool rowImplication(ArithVar v, bool upperBound, const DeltaRational& r);
/**
}
} d_setupLiteralCallback;
+
+
/**
* (For the moment) the type hierarchy goes as:
* Integer <: Real
TimerStat d_boundComputationTime;
IntStat d_boundComputations, d_boundPropagations;
+ IntStat d_unknownChecks;
+ IntStat d_maxUnknownsInARow;
+ AverageStat d_avgUnknownsInARow;
+
+ IntStat d_revertsOnConflicts;
+ IntStat d_commitsOnConflicts;
+ IntStat d_nontrivialSatChecks;
+
Statistics();
~Statistics();
};
satRestartInc(3.0),
arithUnateLemmaMode(ALL_PRESOLVE_LEMMAS),
arithPropagationMode(BOTH_PROP),
- arithPivotRule(MINIMUM),
- arithPivotThreshold(16),
+ arithHeuristicPivots(0),
+ arithHeuristicPivotsSetByUser(false),
+ arithStandardCheckVarOrderPivots(-1),
+ arithStandardCheckVarOrderPivotsSetByUser(false),
+ arithHeuristicPivotRule(MINIMUM),
+ arithSimplexCheckPeriod(200),
+ arithPivotThreshold(2),
+ arithPivotThresholdSetByUser(false),
arithPropagateMaxLength(16),
arithDioSolver(true),
arithRewriteEq(false),
--restart-int-inc=F restart interval increase factor for the sat solver\n\
(F=3.0 by default)\n\
ARITHMETIC:\n\
- ---unate-lemmas=MODE determines which lemmas to add before solving\n\
+ --unate-lemmas=MODE determines which lemmas to add before solving\n\
(default is 'all', see --unate-lemmas=help)\n\
--arith-prop=MODE turns on arithmetic propagation\n\
(default is 'old', see --arith-prop=help)\n\
- --pivot-rule=RULE change the pivot rule for the basic variable\n\
- (default is 'min', see --pivot-rule help)\n\
+ --heuristic-pivot-rule=RULE change the pivot rule for the basic variable\n\
+ (default is 'min', see --heuristic-pivot-rule help)\n\
+ --heuristic-pivots=N the number of times to apply the heuristic pivot rule.\n\
+ If N < 0, this defaults to the number of variables\n\
+ If this is unset, this is tuned by the logic selection.\n\
+ --simplex-check-period=N The number of pivots to do in simplex before rechecking for\n\
+ a conflict on all variables.\n\
--pivot-threshold=N sets the number of pivots using --pivot-rule\n\
per basic variable per simplex instance before\n\
using variable order\n\
SAT_RESTART_INC,
ARITHMETIC_UNATE_LEMMA_MODE,
ARITHMETIC_PROPAGATION_MODE,
+ ARITHMETIC_HEURISTIC_PIVOTS,
+ ARITHMETIC_VAR_ORDER_PIVOTS,
ARITHMETIC_PIVOT_RULE,
+ ARITHMETIC_CHECK_PERIOD,
ARITHMETIC_PIVOT_THRESHOLD,
ARITHMETIC_PROP_MAX_LENGTH,
ARITHMETIC_DIO_SOLVER,
{ "print-winner", no_argument , NULL, PRINT_WINNER },
{ "unate-lemmas", required_argument, NULL, ARITHMETIC_UNATE_LEMMA_MODE },
{ "arith-prop", required_argument, NULL, ARITHMETIC_PROPAGATION_MODE },
- { "pivot-rule" , required_argument, NULL, ARITHMETIC_PIVOT_RULE },
+ { "heuristic-pivots", required_argument, NULL, ARITHMETIC_HEURISTIC_PIVOTS },
+ { "heuristic-pivot-rule" , required_argument, NULL, ARITHMETIC_PIVOT_RULE },
+ { "standard-effort-variable-order-pivots", required_argument, NULL, ARITHMETIC_VAR_ORDER_PIVOTS },
+ { "simplex-check-period" , required_argument, NULL, ARITHMETIC_CHECK_PERIOD },
{ "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD },
{ "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH },
{ "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER },
}
break;
+ case ARITHMETIC_HEURISTIC_PIVOTS:
+ arithHeuristicPivots = atoi(optarg);
+ arithHeuristicPivotsSetByUser = true;
+ break;
+
+ case ARITHMETIC_VAR_ORDER_PIVOTS:
+ arithStandardCheckVarOrderPivots = atoi(optarg);
+ arithStandardCheckVarOrderPivotsSetByUser = true;
+ break;
+
case ARITHMETIC_PIVOT_RULE:
if(!strcmp(optarg, "min")) {
- arithPivotRule = MINIMUM;
+ arithHeuristicPivotRule = MINIMUM;
break;
} else if(!strcmp(optarg, "min-break-ties")) {
- arithPivotRule = BREAK_TIES;
+ arithHeuristicPivotRule = BREAK_TIES;
break;
} else if(!strcmp(optarg, "max")) {
- arithPivotRule = MAXIMUM;
+ arithHeuristicPivotRule = MAXIMUM;
break;
} else if(!strcmp(optarg, "help")) {
puts(pivotRulesHelp.c_str());
exit(1);
} else {
- throw OptionException(string("unknown option for --pivot-rule: `") +
- optarg + "'. Try --pivot-rule help.");
+ throw OptionException(string("unknown option for --heuristic-pivot-rule: `") +
+ optarg + "'. Try --heuristic-pivot-rule help.");
}
break;
+ case ARITHMETIC_CHECK_PERIOD:
+ arithSimplexCheckPeriod = atoi(optarg);
+ break;
+
case ARITHMETIC_PIVOT_THRESHOLD:
arithPivotThreshold = atoi(optarg);
+ arithPivotThresholdSetByUser = true;
break;
case ARITHMETIC_PROP_MAX_LENGTH:
languageHelp = true;
}
-std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) {
+std::ostream& operator<<(std::ostream& out, Options::ArithHeuristicPivotRule rule) {
switch(rule) {
case Options::MINIMUM:
out << "MINIMUM";
typedef enum { NO_PROP, UNATE_PROP, BOUND_INFERENCE_PROP, BOTH_PROP} ArithPropagationMode;
ArithPropagationMode arithPropagationMode;
- /** The pivot rule for arithmetic */
- typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule;
- ArithPivotRule arithPivotRule;
+ /**
+ * The maximum number of difference pivots to do per invokation of simplex.
+ * If this is negative, the number of pivots done is the number of variables.
+ * If this is not set by the user, different logics are free to chose different
+ * defaults.
+ */
+ int16_t arithHeuristicPivots;
+ bool arithHeuristicPivotsSetByUser;
+
+ /**
+ * The maximum number of variable order pivots to do per invokation of simplex.
+ * If this is negative, the number of pivots done is unlimited.
+ * If this is not set by the user, different logics are free to chose different
+ * defaults.
+ */
+ int16_t arithStandardCheckVarOrderPivots;
+ bool arithStandardCheckVarOrderPivotsSetByUser;
+
+ /** The heuristic pivot rule for arithmetic. */
+ typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithHeuristicPivotRule;
+ ArithHeuristicPivotRule arithHeuristicPivotRule;
+
+ /**
+ * The number of pivots before simplex rechecks every basic variable for a conflict.
+ */
+ uint16_t arithSimplexCheckPeriod;
/**
- * The number of pivots before Bland's pivot rule is used on a basic
- * variable in arithmetic.
+ * This is the pivots per basic variable that can be done using heuristic choices
+ * before variable order must be used.
+ * If this is not set by the user, different logics are free to chose different
+ * defaults.
*/
uint16_t arithPivotThreshold;
+ bool arithPivotThresholdSetByUser;
/**
* The maximum row length that arithmetic will use for propagation.
return out;
}
-std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, Options::ArithHeuristicPivotRule rule) CVC4_PUBLIC;
}/* CVC4 namespace */
projects / cvc5.git / commitdiff