std::ostream& operator<<(std::ostream& o, const Constraint c){
- return o << *c;
+ if(c == NullConstraint){
+ return o << "NullConstraint";
+ }else{
+ return o << *c;
+ }
}
std::ostream& operator<<(std::ostream& o, const ConstraintType t){
Assert(d_nodetoConstraintMap.empty());
}
+ConstraintDatabase::Statistics::Statistics():
+ d_unatePropagateCalls("theory::arith::cd::unatePropagateCalls", 0),
+ d_unatePropagateImplications("theory::arith::cd::unatePropagateImplications", 0)
+{
+ StatisticsRegistry::registerStat(&d_unatePropagateCalls);
+ StatisticsRegistry::registerStat(&d_unatePropagateImplications);
+
+}
+ConstraintDatabase::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_unatePropagateCalls);
+ StatisticsRegistry::unregisterStat(&d_unatePropagateImplications);
+}
+
void ConstraintDatabase::addVariable(ArithVar v){
Assert(v == d_varDatabases.size());
d_varDatabases.push_back(new PerVariableDatabase(v));
out.push_back(orderOr);
}
-void ConstraintDatabase::outputAllUnateLemmas(std::vector<Node>& out, ArithVar v) const{
+void ConstraintDatabase::outputUnateInequalityLemmas(std::vector<Node>& out, ArithVar v) const{
SortedConstraintMap& scm = getVariableSCM(v);
-
- SortedConstraintMapConstIterator outer;
+ SortedConstraintMapConstIterator scm_iter = scm.begin();
SortedConstraintMapConstIterator scm_end = scm.end();
-
- vector<Constraint> equalities;
- for(outer = scm.begin(); outer != scm_end; ++outer){
- const ValueCollection& vc = outer->second;
- if(vc.hasEquality()){
- Constraint eq = vc.getEquality();
- if(eq->hasLiteral()){
- equalities.push_back(eq);
- }
- }
- }
-
Constraint prev = NullConstraint;
//get transitive unates
//Only lower bounds or upperbounds should be done.
- for(outer = scm.begin(); outer != scm_end; ++outer){
- const ValueCollection& vc = outer->second;
-
+ for(; scm_iter != scm_end; ++scm_iter){
+ const ValueCollection& vc = scm_iter->second;
if(vc.hasUpperBound()){
Constraint ub = vc.getUpperBound();
if(ub->hasLiteral()){
}
}
}
+}
+
+void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<Node>& out, ArithVar v) const{
+
+ vector<Constraint> equalities;
+
+ SortedConstraintMap& scm = getVariableSCM(v);
+ SortedConstraintMapConstIterator scm_iter = scm.begin();
+ SortedConstraintMapConstIterator scm_end = scm.end();
+
+ for(; scm_iter != scm_end; ++scm_iter){
+ const ValueCollection& vc = scm_iter->second;
+ if(vc.hasEquality()){
+ Constraint eq = vc.getEquality();
+ if(eq->hasLiteral()){
+ equalities.push_back(eq);
+ }
+ }
+ }
+
vector<Constraint>::const_iterator i, j, eq_end = equalities.end();
for(i = equalities.begin(); i != eq_end; ++i){
Constraint at_i = *i;
implies(out, eq, ub);
}
}
+}
+
+void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<Node>& lemmas) const{
+ for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){
+ outputUnateEqualityLemmas(lemmas, v);
}
+}
-void ConstraintDatabase::outputAllUnateLemmas(std::vector<Node>& lemmas) const{
+void ConstraintDatabase::outputUnateInequalityLemmas(std::vector<Node>& lemmas) const{
for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){
- outputAllUnateLemmas(lemmas, v);
+ outputUnateInequalityLemmas(lemmas, v);
}
}
+void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){
+ Debug("arith::unate") << "unatePropLowerBound " << curr << " " << prev << endl;
+ Assert(curr != prev);
+ Assert(curr != NullConstraint);
+ bool hasPrev = ! (prev == NullConstraint);
+ Assert(!hasPrev || curr->getValue() > prev->getValue());
+
+ ++d_statistics.d_unatePropagateCalls;
+
+ const SortedConstraintMap& scm = curr->constraintSet();
+ const SortedConstraintMapConstIterator scm_begin = scm.begin();
+ SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
+
+ //Ignore the first ValueCollection
+ // NOPE: (>= p c) then (= p c) NOPE
+ // NOPE: (>= p c) then (not (= p c)) NOPE
+
+ while(scm_i != scm_begin){
+ --scm_i; // move the iterator back
+
+ const ValueCollection& vc = scm_i->second;
+
+ //If it has the previous element, do nothing and stop!
+ if(hasPrev &&
+ vc.hasConstraintOfType(prev->getType())
+ && vc.getConstraintOfType(prev->getType()) == prev){
+ break;
+ }
+
+ //Don't worry about implying the negation of upperbound.
+ //These should all be handled by propagating the LowerBounds!
+ if(vc.hasLowerBound()){
+ Constraint lb = vc.getLowerBound();
+ if(!lb->isTrue()){
+ ++d_statistics.d_unatePropagateImplications;
+ Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << lb << endl;
+ lb->impliedBy(curr);
+ }
+ }
+ if(vc.hasDisequality()){
+ Constraint dis = vc.getDisequality();
+ if(!dis->isTrue()){
+ ++d_statistics.d_unatePropagateImplications;
+ Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << dis << endl;
+ dis->impliedBy(curr);
+ }
+ }
+ }
+}
+
+void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){
+ Debug("arith::unate") << "unatePropUpperBound " << curr << " " << prev << endl;
+ Assert(curr != prev);
+ Assert(curr != NullConstraint);
+ bool hasPrev = ! (prev == NullConstraint);
+ Assert(!hasPrev || curr->getValue() < prev->getValue());
+
+ ++d_statistics.d_unatePropagateCalls;
+
+ const SortedConstraintMap& scm = curr->constraintSet();
+ const SortedConstraintMapConstIterator scm_end = scm.end();
+ SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
+ ++scm_i;
+ for(; scm_i != scm_end; ++scm_i){
+ const ValueCollection& vc = scm_i->second;
+
+ //If it has the previous element, do nothing and stop!
+ if(hasPrev &&
+ vc.hasConstraintOfType(prev->getType()) &&
+ vc.getConstraintOfType(prev->getType()) == prev){
+ break;
+ }
+ //Don't worry about implying the negation of upperbound.
+ //These should all be handled by propagating the UpperBounds!
+ if(vc.hasUpperBound()){
+ Constraint ub = vc.getUpperBound();
+ if(!ub->isTrue()){
+ ++d_statistics.d_unatePropagateImplications;
+ Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << ub << endl;
+ ub->impliedBy(curr);
+ }
+ }
+ if(vc.hasDisequality()){
+ Constraint dis = vc.getDisequality();
+ if(!dis->isTrue()){
+ Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl;
+ ++d_statistics.d_unatePropagateImplications;
+ dis->impliedBy(curr);
+ }
+ }
+ }
+}
+
+void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, Constraint prevUB){
+ Debug("arith::unate") << "unatePropEquality " << curr << " " << prevLB << " " << prevUB << endl;
+ Assert(curr != prevLB);
+ Assert(curr != prevUB);
+ Assert(curr != NullConstraint);
+ bool hasPrevLB = ! (prevLB == NullConstraint);
+ bool hasPrevUB = ! (prevUB == NullConstraint);
+ Assert(!hasPrevLB || curr->getValue() >= prevLB->getValue());
+ Assert(!hasPrevUB || curr->getValue() <= prevUB->getValue());
+
+ ++d_statistics.d_unatePropagateCalls;
+
+ const SortedConstraintMap& scm = curr->constraintSet();
+ SortedConstraintMapConstIterator scm_curr = curr->d_variablePosition;
+ SortedConstraintMapConstIterator scm_last = hasPrevUB ? prevUB->d_variablePosition : scm.end();
+ SortedConstraintMapConstIterator scm_i;
+ if(hasPrevLB){
+ scm_i = prevLB->d_variablePosition;
+ if(scm_i != scm_curr){ // If this does not move this past scm_curr, move it one forward
+ ++scm_i;
+ }
+ }else{
+ scm_i = scm.begin();
+ }
+
+ for(; scm_i != scm_curr; ++scm_i){
+ // between the previous LB and the curr
+ const ValueCollection& vc = scm_i->second;
+
+ //Don't worry about implying the negation of upperbound.
+ //These should all be handled by propagating the LowerBounds!
+ if(vc.hasLowerBound()){
+ Constraint lb = vc.getLowerBound();
+ if(!lb->isTrue()){
+ ++d_statistics.d_unatePropagateImplications;
+ Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << lb << endl;
+ lb->impliedBy(curr);
+ }
+ }
+ if(vc.hasDisequality()){
+ Constraint dis = vc.getDisequality();
+ if(!dis->isTrue()){
+ ++d_statistics.d_unatePropagateImplications;
+ Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl;
+ dis->impliedBy(curr);
+ }
+ }
+ }
+ Assert(scm_i == scm_curr);
+ if(!hasPrevUB || scm_i != scm_last){
+ ++scm_i;
+ } // hasPrevUB implies scm_i != scm_last
+
+ for(; scm_i != scm_last; ++scm_i){
+ // between the curr and the previous UB imply the upperbounds and disequalities.
+ const ValueCollection& vc = scm_i->second;
+
+ //Don't worry about implying the negation of upperbound.
+ //These should all be handled by propagating the UpperBounds!
+ if(vc.hasUpperBound()){
+ Constraint ub = vc.getUpperBound();
+ if(!ub->isTrue()){
+ ++d_statistics.d_unatePropagateImplications;
+ Debug("arith::unate") << "unateProp " << curr << " implies " << ub << endl;
+ ub->impliedBy(curr);
+ }
+ }
+ if(vc.hasDisequality()){
+ Constraint dis = vc.getDisequality();
+ if(!dis->isTrue()){
+ ++d_statistics.d_unatePropagateImplications;
+ Debug("arith::unate") << "unateProp " << curr << " implies " << dis << endl;
+ dis->impliedBy(curr);
+ }
+ }
+ }
+}
}/* arith namespace */
}/* theory namespace */
*/
Constraint getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r);
+ /**
+ * Outputs a minimal set of unate implications onto the vector for the variable.
+ * This outputs lemmas of the general forms
+ * (= p c) implies (<= p d) for c < d, or
+ * (= p c) implies (not (= p d)) for c != d.
+ */
+ void outputUnateEqualityLemmas(std::vector<Node>& lemmas) const;
+ void outputUnateEqualityLemmas(std::vector<Node>& lemmas, ArithVar v) const;
/**
- * Outputs a minimal set of unate implications on the output channel
- * for all variables.
+ * Outputs a minimal set of unate implications onto the vector for the variable.
+ *
+ * If ineqs is true, this outputs lemmas of the general form
+ * (<= p c) implies (<= p d) for c < d.
*/
- void outputAllUnateLemmas(std::vector<Node>& lemmas) const;
+ void outputUnateInequalityLemmas(std::vector<Node>& lemmas) const;
+ void outputUnateInequalityLemmas(std::vector<Node>& lemmas, ArithVar v) const;
+
+
+ void unatePropLowerBound(Constraint curr, Constraint prev);
+ void unatePropUpperBound(Constraint curr, Constraint prev);
+ void unatePropEquality(Constraint curr, Constraint prevLB, Constraint prevUB);
+
+private:
+ class Statistics {
+ public:
+ IntStat d_unatePropagateCalls;
+ IntStat d_unatePropagateImplications;
- void outputAllUnateLemmas(std::vector<Node>& lemmas, ArithVar v) const;
+ Statistics();
+ ~Statistics();
+ } d_statistics;
}; /* ConstraintDatabase */
d_pivotsInRound(),
d_DELTA_ZERO(0,0)
{
- switch(Options::ArithPivotRule rule = Options::current()->pivotRule) {
+ switch(Options::ArithPivotRule rule = Options::current()->arithPivotRule) {
case Options::MINIMUM:
d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
break;
d_simplifyTimer("theory::arith::simplifyTimer"),
d_staticLearningTimer("theory::arith::staticLearningTimer"),
d_presolveTime("theory::arith::presolveTime"),
+ d_newPropTime("::newPropTimer"),
d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0),
d_initialTableauSize("theory::arith::initialTableauSize", 0),
d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
StatisticsRegistry::registerStat(&d_staticLearningTimer);
StatisticsRegistry::registerStat(&d_presolveTime);
+ StatisticsRegistry::registerStat(&d_newPropTime);
StatisticsRegistry::registerStat(&d_externalBranchAndBounds);
StatisticsRegistry::unregisterStat(&d_staticLearningTimer);
StatisticsRegistry::unregisterStat(&d_presolveTime);
+ StatisticsRegistry::unregisterStat(&d_newPropTime);
StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds);
StatisticsRegistry::unregisterStat(&d_boundPropagations);
}
+void TheoryArith::revertOutOfConflict(){
+ d_partialModel.revertAssignmentChanges();
+ clearUpdates();
+ d_currentPropagationList.clear();
+}
+
+void TheoryArith::clearUpdates(){
+ d_updatedBounds.purge();
+}
+
void TheoryArith::zeroDifferenceDetected(ArithVar x){
Assert(d_congruenceManager.isWatchedVariable(x));
Assert(d_partialModel.upperBoundIsZero(x));
}
}
+ d_currentPropagationList.push_back(constraint);
+ d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i));
+
d_partialModel.setLowerBoundConstraint(constraint);
if(d_congruenceManager.isWatchedVariable(x_i)){
}
+ d_currentPropagationList.push_back(constraint);
+ d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i));
+ //It is fine if this is NullConstraint
+
d_partialModel.setUpperBoundConstraint(constraint);
if(d_congruenceManager.isWatchedVariable(x_i)){
// Don't bother to check whether x_i != c_i is in d_diseq
// The a and (not a) should never be on the fact queue
+ d_currentPropagationList.push_back(constraint);
+ d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i));
+ d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i));
d_partialModel.setUpperBoundConstraint(constraint);
d_partialModel.setLowerBoundConstraint(constraint);
void TheoryArith::check(Effort effortLevel){
+ Assert(d_currentPropagationList.empty());
Debug("arith") << "TheoryArith::check begun" << std::endl;
d_hasDoneWorkSinceCut = d_hasDoneWorkSinceCut || !done();
Node possibleConflict = assertionCases(assertion);
if(!possibleConflict.isNull()){
- d_partialModel.revertAssignmentChanges();
+ revertOutOfConflict();
+
Debug("arith::conflict") << "conflict " << possibleConflict << endl;
- clearUpdates();
d_out->conflict(possibleConflict);
return;
}
if(d_congruenceManager.inConflict()){
Node c = d_congruenceManager.conflict();
- d_partialModel.revertAssignmentChanges();
+ revertOutOfConflict();
Debug("arith::conflict") << "difference manager conflict " << c << endl;
- clearUpdates();
d_out->conflict(c);
return;
}
Assert(d_conflicts.empty());
bool foundConflict = d_simplex.findModel();
if(foundConflict){
- d_partialModel.revertAssignmentChanges();
- clearUpdates();
+ revertOutOfConflict();
Assert(!d_conflicts.empty());
for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){
Node conflict = d_conflicts[i];
Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict << endl;
- d_out->conflict(conflict);
+ d_out->conflict(conflict);
}
emmittedConflictOrSplit = true;
}else{
d_partialModel.commitAssignmentChanges();
}
+ if(!emmittedConflictOrSplit &&
+ (Options::current()->arithPropagationMode == Options::UNATE_PROP ||
+ Options::current()->arithPropagationMode == Options::BOTH_PROP)){
+ TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
+
+ while(!d_currentPropagationList.empty()){
+ Constraint curr = d_currentPropagationList.front();
+ d_currentPropagationList.pop_front();
+
+ ConstraintType t = curr->getType();
+ Assert(t != Disequality, "Disequalities are not allowed in d_currentPropagation");
+
+
+ switch(t){
+ case LowerBound:
+ {
+ Constraint prev = d_currentPropagationList.front();
+ d_currentPropagationList.pop_front();
+ d_constraintDatabase.unatePropLowerBound(curr, prev);
+ break;
+ }
+ case UpperBound:
+ {
+ Constraint prev = d_currentPropagationList.front();
+ d_currentPropagationList.pop_front();
+ d_constraintDatabase.unatePropUpperBound(curr, prev);
+ break;
+ }
+ case Equality:
+ {
+ Constraint prevLB = d_currentPropagationList.front();
+ d_currentPropagationList.pop_front();
+ Constraint prevUB = d_currentPropagationList.front();
+ d_currentPropagationList.pop_front();
+ d_constraintDatabase.unatePropEquality(curr, prevLB, prevUB);
+ break;
+ }
+ default:
+ Unhandled(curr->getType());
+ }
+ }
+ }else{
+ TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
+ d_currentPropagationList.clear();
+ }
+ Assert( d_currentPropagationList.empty());
+
if(!emmittedConflictOrSplit && fullEffort(effortLevel)){
emmittedConflictOrSplit = splitDisequalities();
}
- Node possibleConflict = Node::null();
if(!emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()){
-
- if(!emmittedConflictOrSplit && Options::current()->dioSolver){
+ Node possibleConflict = Node::null();
+ if(!emmittedConflictOrSplit && Options::current()->arithDioSolver){
possibleConflict = callDioSolver();
if(possibleConflict != Node::null()){
+ revertOutOfConflict();
Debug("arith::conflict") << "dio conflict " << possibleConflict << endl;
d_out->conflict(possibleConflict);
emmittedConflictOrSplit = true;
}
}
- if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && Options::current()->dioSolver){
+ if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && Options::current()->arithDioSolver){
Node possibleLemma = dioCutting();
if(!possibleLemma.isNull()){
Debug("arith") << "dio cut " << possibleLemma << endl;
void TheoryArith::propagate(Effort e) {
- if(Options::current()->arithPropagation && hasAnyUpdates()){
+ if((Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP ||
+ Options::current()->arithPropagationMode == Options::BOTH_PROP)
+ && hasAnyUpdates()){
propagateCandidates();
}else{
clearUpdates();
callCount = callCount + 1;
}
- if(Options::current()->arithPropagation ){
- vector<Node> lemmas;
- d_constraintDatabase.outputAllUnateLemmas(lemmas);
- vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
- for(; i != i_end; ++i){
- Node lem = *i;
- Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
- d_out->lemma(lem);
- }
+ vector<Node> lemmas;
+ switch(Options::current()->arithUnateLemmaMode){
+ case Options::NO_PRESOLVE_LEMMAS:
+ break;
+ case Options::INEQUALITY_PRESOLVE_LEMMAS:
+ d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
+ break;
+ case Options::EQUALITY_PRESOLVE_LEMMAS:
+ d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
+ break;
+ case Options::ALL_PRESOLVE_LEMMAS:
+ d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
+ d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
+ break;
+ default:
+ Unhandled(Options::current()->arithUnateLemmaMode);
}
+ vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
+ for(; i != i_end; ++i){
+ Node lem = *i;
+ Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
+ d_out->lemma(lem);
+ }
+
+ // if(Options::current()->arithUnateLemmaMode == Options::ALL_UNATE){
+ // vector<Node> lemmas;
+ // d_constraintDatabase.outputAllUnateLemmas(lemmas);
+ // vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
+ // for(; i != i_end; ++i){
+ // Node lem = *i;
+ // Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
+ // d_out->lemma(lem);
+ // }
+ // }
+
d_learner.clear();
}
Comparison mkIntegerEqualityFromAssignment(ArithVar v);
/**
- * List of all of the inequalities asserted in the current context.
+ * List of all of the disequalities asserted in the current context that are not known
+ * to be satisfied.
*/
- //context::CDHashSet<Node, NodeHashFunction> d_diseq;
context::CDQueue<Constraint> d_diseqQueue;
+ /**
+ * Constraints that have yet to be processed by proagation work list.
+ * All of the elements have type of LowerBound, UpperBound, or
+ * Equality.
+ *
+ * This is empty at the beginning of every check call.
+ *
+ * If head()->getType() == LowerBound or UpperBound,
+ * then d_cPL[1] is the previous constraint in d_partialModel for the
+ * corresponding bound.
+ * If head()->getType() == Equality,
+ * then d_cPL[1] is the previous lowerBound in d_partialModel,
+ * and d_cPL[2] is the previous upperBound in d_partialModel.
+ */
+ std::deque<Constraint> d_currentPropagationList;
/**
* Manages information about the assignment and upper and lower bounds on
DenseSet d_candidateBasics;
bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
- void clearUpdates(){ d_updatedBounds.purge(); }
+ void clearUpdates();
+
+ void revertOutOfConflict();
void propagateCandidates();
void propagateCandidate(ArithVar basic);
TimerStat d_presolveTime;
+ TimerStat d_newPropTime;
+
IntStat d_externalBranchAndBounds;
IntStat d_initialTableauSize;
replayFilename(""),
replayStream(NULL),
replayLog(NULL),
- arithPropagation(true),
satRandomFreq(0.0),
satRandomSeed(91648253),// Minisat's default value
satVarDecay(0.95),
satClauseDecay(0.999),
satRestartFirst(25),
satRestartInc(3.0),
- pivotRule(MINIMUM),
+ arithUnateLemmaMode(ALL_PRESOLVE_LEMMAS),
+ arithPropagationMode(BOTH_PROP),
+ arithPivotRule(MINIMUM),
arithPivotThreshold(16),
arithPropagateMaxLength(16),
- ufSymmetryBreaker(false),
- ufSymmetryBreakerSetByUser(false),
- dioSolver(true),
+ arithDioSolver(true),
arithRewriteEq(false),
arithRewriteEqSetByUser(false),
+ ufSymmetryBreaker(false),
+ ufSymmetryBreakerSetByUser(false),
lemmaOutputChannel(NULL),
lemmaInputChannel(NULL),
threads(2),// default should be 1 probably, but say 2 for now
Most commonly-used CVC4 options:\n\
--version | -V identify this CVC4 binary\n\
--help | -h full command line reference\n\
- --lang | -L force input language (default is `auto'; see --lang help)\n\
- --output-lang force output language (default is `auto'; see --lang help)\n\
+ --lang | -L force input language\n\
+ (default is `auto'; see --lang help)\n\
+ --output-lang force output language\n\
+ (default is `auto'; see --lang help)\n\
--verbose | -v increase verbosity (may be repeated)\n\
--quiet | -q decrease verbosity (may be repeated)\n\
--stats give statistics on exit\n\
--mmap memory map file input\n\
--segv-nospin don't spin on segfault waiting for gdb\n\
--lazy-type-checking type check expressions only when necessary (default)\n\
- --eager-type-checking type check expressions immediately on creation (debug builds only)\n\
+ --eager-type-checking type check expressions immediately on creation\n\
+ (debug builds only)\n\
--no-type-checking never type check expressions\n\
--no-checking disable ALL semantic checks, including type checks\n\
--no-theory-registration disable theory reg (not safe for some theories)\n\
--no-ite-simp turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
--replay=file replay decisions from file\n\
--replay-log=file log decisions and propagations to file\n\
- --pivot-rule=RULE change the pivot rule (see --pivot-rule help)\n\
- --pivot-threshold=N sets the number of heuristic pivots per variable per simplex instance\n\
- --prop-row-length=N sets the maximum row length to be used in propagation\n\
- --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\
+ SAT:\n\
+ --random-freq=P frequency of random decisions in the sat solver\n\
+ (P=0.0 by default)\n\
--random-seed=S sets the random seed for the sat solver\n\
- --restart-int-base=I sets the base restart interval for the sat solver (I=25 by default)\n\
- --restart-int-inc=F sets the restart interval increase factor for the sat solver (F=3.0 by default)\n\
- --disable-arithmetic-propagation turns on arithmetic propagation\n\
- --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\
+ --restart-int-base=I sets the base restart interval for the sat solver\n\
+ (I=25 by default)\n\
+ --restart-int-inc=F restart interval increase factor for the sat solver\n\
+ (F=3.0 by default)\n\
+ ARITHMETIC:\n\
+ --arith-presolve-lemmas=MODE determines which lemmas to add before solving\n\
+ (default is 'all', see --arith-presolve-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\
+ --pivot-threshold=N sets the number of pivots using --pivot-rule\n\
+ per basic variable per simplex instance before\n\
+ using variable order\n\
+ --prop-row-length=N sets the maximum row length to be used in propagation\n\
+ --disable-dio-solver turns off Linear Diophantine Equation solver \n\
+ (Griggio, JSAT 2012)\n\
+ --enable-arith-rewrite-equalities turns on the preprocessing rewrite\n\
+ turning equalities into a conjunction of inequalities.\n \
+ --disable-arith-rewrite-equalities turns off the preprocessing rewrite\n\
+ turning equalities into a conjunction of inequalities.\n \
+ UF:\n\
+ --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al.,\n\
+ CADE 2011) [on by default only for QF_UF]\n\
--disable-symmetry-breaker turns off UF symmetry breaker\n\
- --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\
- --disable-arith-rewrite-equalities turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n\
--threads=N sets the number of solver threads\n\
--threadN=string configures thread N (0..#threads-1)\n\
--filter-lemma-length=N don't share lemmas strictly longer than N\n\
to a file.\n\
";
+static const string arithPresolveLemmasHelp = "\
+Presolve lemmas are generated before SAT search begins using the relationship\n\
+of constant terms and polynomials.\n\
+Modes currently supported by the --arith-presolve-lemmas option:\n\
++ none \n\
++ ineqs \n\
+ Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\
++ eqs \n\
+ Outputs lemmas of the general forms\n\
+ (= p c) implies (<= p d) for c < d, or\n\
+ (= p c) implies (not (= p d)) for c != d.\n\
++ all \n\
+ A combination of inequalities and equalities.\n\
+";
+
+static const string propagationModeHelp = "\
+This decides on kind of propagation arithmetic attempts to do during the search.\n\
++ none\n\
++ unate\n\
+ use constraints to do unate propagation\n\
++ bi (Bounds Inference)\n\
+ infers bounds on basic variables using the upper and lower bounds of the\n\
+ non-basic variables in the tableau.\n\
++both\n\
+";
+
+static const string pivotRulesHelp = "\
+This decides on the rule used by simplex during hueristic rounds\n\
+for deciding the next basic variable to select.\n\
+Pivot rules available:\n\
++min\n\
+ The minimum abs() value of the variable's violation of its bound. (default)\n\
++min-break-ties\n\
+ The minimum violation with ties broken by variable order (total)\n\
++max\n\
+ The maximum violation the bound\n\
+";
+
string Options::getDescription() const {
return optionsDescription;
}
* any collision.
*/
enum OptionValue {
- SMTCOMP = 256, /* avoid clashing with char options */
+ OPTION_VALUE_BEGIN = 256, /* avoid clashing with char options */
+ SMTCOMP,
STATS,
SEGV_NOSPIN,
OUTPUT_LANGUAGE,
EAGER_TYPE_CHECKING,
REPLAY,
REPLAY_LOG,
- PIVOT_RULE,
PRINT_WINNER,
RANDOM_FREQUENCY,
RANDOM_SEED,
SAT_RESTART_FIRST,
SAT_RESTART_INC,
- ARITHMETIC_PROPAGATION,
+ ARITHMETIC_UNATE_LEMMA_MODE,
+ ARITHMETIC_PROPAGATION_MODE,
+ ARITHMETIC_PIVOT_RULE,
ARITHMETIC_PIVOT_THRESHOLD,
ARITHMETIC_PROP_MAX_LENGTH,
ARITHMETIC_DIO_SOLVER,
BITVECTOR_EAGER_BITBLAST,
BITVECTOR_SHARE_LEMMAS,
BITVECTOR_EAGER_FULLCHECK,
- SAT_REFINE_CONFLICTS
+ SAT_REFINE_CONFLICTS,
+ OPTION_VALUE_END
};/* enum OptionValue */
/**
{ "incremental", no_argument , NULL, 'i' },
{ "replay" , required_argument, NULL, REPLAY },
{ "replay-log" , required_argument, NULL, REPLAY_LOG },
- { "pivot-rule" , required_argument, NULL, PIVOT_RULE },
- { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD },
- { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH },
{ "random-freq" , required_argument, NULL, RANDOM_FREQUENCY },
{ "random-seed" , required_argument, NULL, RANDOM_SEED },
{ "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST },
{ "restart-int-inc", required_argument, NULL, SAT_RESTART_INC },
{ "print-winner", no_argument , NULL, PRINT_WINNER },
- { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
+ { "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 },
+ { "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 },
{ "enable-arith-rewrite-equalities", no_argument, NULL, ENABLE_ARITHMETIC_REWRITE_EQUALITIES },
{ "disable-arith-rewrite-equalities", no_argument, NULL, DISABLE_ARITHMETIC_REWRITE_EQUALITIES },
#endif /* CVC4_REPLAY */
break;
- case ARITHMETIC_PROPAGATION:
- arithPropagation = false;
- break;
-
- case ARITHMETIC_DIO_SOLVER:
- dioSolver = false;
- break;
-
- case ENABLE_ARITHMETIC_REWRITE_EQUALITIES:
- arithRewriteEq = true;
- arithRewriteEqSetByUser = true;
- break;
-
- case DISABLE_ARITHMETIC_REWRITE_EQUALITIES:
- arithRewriteEq = false;
- arithRewriteEqSetByUser = true;
- break;
-
case ENABLE_SYMMETRY_BREAKER:
ufSymmetryBreaker = true;
ufSymmetryBreakerSetByUser = true;
}
break;
- case PIVOT_RULE:
+ case ARITHMETIC_UNATE_LEMMA_MODE:
+ if(!strcmp(optarg, "all")) {
+ arithUnateLemmaMode = ALL_PRESOLVE_LEMMAS;
+ break;
+ } else if(!strcmp(optarg, "none")) {
+ arithUnateLemmaMode = NO_PRESOLVE_LEMMAS;
+ break;
+ } else if(!strcmp(optarg, "ineqs")) {
+ arithUnateLemmaMode = INEQUALITY_PRESOLVE_LEMMAS;
+ break;
+ } else if(!strcmp(optarg, "eqs")) {
+ arithUnateLemmaMode = EQUALITY_PRESOLVE_LEMMAS;
+ break;
+ } else if(!strcmp(optarg, "help")) {
+ puts(arithPresolveLemmasHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(string("unknown option for --arith-presolve-lemmas: `") +
+ optarg + "'. Try --arith-presolve-lemmas=help.");
+ }
+ break;
+
+ case ARITHMETIC_PROPAGATION_MODE:
+ if(!strcmp(optarg, "none")) {
+ arithPropagationMode = NO_PROP;
+ break;
+ } else if(!strcmp(optarg, "unate")) {
+ arithPropagationMode = UNATE_PROP;
+ break;
+ } else if(!strcmp(optarg, "bi")) {
+ arithPropagationMode = BOUND_INFERENCE_PROP;
+ break;
+ } else if(!strcmp(optarg, "both")) {
+ arithPropagationMode = BOTH_PROP;
+ break;
+ } else if(!strcmp(optarg, "help")) {
+ puts(propagationModeHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(string("unknown option for --arith-prop: `") +
+ optarg + "'. Try --arith-prop help.");
+ }
+ break;
+
+ case ARITHMETIC_PIVOT_RULE:
if(!strcmp(optarg, "min")) {
- pivotRule = MINIMUM;
+ arithPivotRule = MINIMUM;
break;
} else if(!strcmp(optarg, "min-break-ties")) {
- pivotRule = BREAK_TIES;
+ arithPivotRule = BREAK_TIES;
break;
} else if(!strcmp(optarg, "max")) {
- pivotRule = MAXIMUM;
+ arithPivotRule = MAXIMUM;
break;
} else if(!strcmp(optarg, "help")) {
- printf("Pivot rules available:\n");
- printf("min\n");
- printf("min-break-ties\n");
- printf("max\n");
+ puts(pivotRulesHelp.c_str());
exit(1);
} else {
throw OptionException(string("unknown option for --pivot-rule: `") +
arithPropagateMaxLength = atoi(optarg);
break;
+ case ARITHMETIC_DIO_SOLVER:
+ arithDioSolver = false;
+ break;
+
+ case ENABLE_ARITHMETIC_REWRITE_EQUALITIES:
+ arithRewriteEq = true;
+ arithRewriteEqSetByUser = true;
+ break;
+
+ case DISABLE_ARITHMETIC_REWRITE_EQUALITIES:
+ arithRewriteEq = false;
+ arithRewriteEqSetByUser = true;
+ break;
+
case SHOW_DEBUG_TAGS:
if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
printf("available tags:");
case ':':
// This can be a long or short option, and the way to get at the name of it is different.
- if(optopt == 0) { // was a long option
+ if(optopt == 0 || // was a long option
+ (optopt >= OPTION_VALUE_BEGIN && optopt <= OPTION_VALUE_END)) { // OptionValue option
throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
} else { // was a short option
throw OptionException(string("option `-") + char(optopt) + "' missing its required argument");
/** Log to write replay instructions to; NULL if not logging. */
std::ostream* replayLog;
- /** Turn on and of arithmetic propagation. */
- bool arithPropagation;
-
/**
* Frequency for the sat solver to make random decisions.
* Should be between 0 and 1.
/** Restart interval increase factor for Minisat */
double satRestartInc;
+ /** Determines the type of Arithmetic Presolve Lemmas are generated.*/
+ typedef enum { NO_PRESOLVE_LEMMAS, INEQUALITY_PRESOLVE_LEMMAS, EQUALITY_PRESOLVE_LEMMAS, ALL_PRESOLVE_LEMMAS} ArithUnateLemmaMode;
+ ArithUnateLemmaMode arithUnateLemmaMode;
+
+ /** Determines the mode of arithmetic propagation. */
+ 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 pivotRule;
+ ArithPivotRule arithPivotRule;
/**
* The number of pivots before Bland's pivot rule is used on a basic
*/
uint16_t arithPropagateMaxLength;
- /**
- * Whether to do the symmetry-breaking preprocessing in UF as
- * described by Deharbe et al. in CADE 2011 (on by default).
- */
- bool ufSymmetryBreaker;
-
- /**
- * Whether the user explicitly requested that the symmetry
- * breaker be enabled or disabled.
- */
- bool ufSymmetryBreakerSetByUser;
-
/**
* Whether to do the linear diophantine equation solver
* in Arith as described by Griggio JSAT 2012 (on by default).
*/
- bool dioSolver;
+ bool arithDioSolver;
/**
* Whether to split (= x y) into (and (<= x y) (>= x y)) in
*/
bool arithRewriteEqSetByUser;
+ /**
+ * Whether to do the symmetry-breaking preprocessing in UF as
+ * described by Deharbe et al. in CADE 2011 (on by default).
+ */
+ bool ufSymmetryBreaker;
+
+ /**
+ * Whether the user explicitly requested that the symmetry
+ * breaker be enabled or disabled.
+ */
+ bool ufSymmetryBreakerSetByUser;
+
+
/** The output channel to receive notfication events for new lemmas */
LemmaOutputChannel* lemmaOutputChannel;
LemmaInputChannel* lemmaInputChannel;
Node gt0Orlt1 = NodeBuilder<2>(OR) << gt0 << lt1;
Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
- cout << d_outputChannel.getIthNode(0) << endl;
- cout << d_outputChannel.getIthNode(1) << endl;
+ cout << d_outputChannel.getIthNode(0) << endl << endl;
+ cout << d_outputChannel.getIthNode(1) << endl << endl;
+ cout << d_outputChannel.getIthNode(2) << endl << endl;
- TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
+ TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
+
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), PROPAGATE);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq1);
}
cout << d_outputChannel.getIthNode(0) << endl;
cout << d_outputChannel.getIthNode(1) << endl;
+ cout << d_outputChannel.getIthNode(2) << endl;
+ cout << d_outputChannel.getIthNode(3) << endl;
- TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
+ TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 4u);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
+
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), PROPAGATE);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1 );
+
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), PROPAGATE);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(3), leq1);
}
void testTPLeq1() {
projects / cvc5.git / commitdiff