summaryrefslogtreecommitdiff
path: root/src/theory/arith/simplex.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/simplex.cpp')
-rw-r--r--src/theory/arith/simplex.cpp132
1 files changed, 108 insertions, 24 deletions
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 2e9fb7352..f7e3c112c 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -21,7 +21,10 @@ SimplexDecisionProcedure::Statistics::Statistics():
d_statUnEjections("theory::arith::UnEjections", 0),
d_statEarlyConflicts("theory::arith::EarlyConflicts", 0),
d_statEarlyConflictImprovements("theory::arith::EarlyConflictImprovements", 0),
- d_selectInitialConflictTime("theory::arith::selectInitialConflictTime")
+ d_selectInitialConflictTime("theory::arith::selectInitialConflictTime"),
+ d_pivotsAfterConflict("theory::arith::pivotsAfterConflict", 0),
+ d_checksWithWastefulPivots("theory::arith::checksWithWastefulPivots", 0),
+ d_pivotTime("theory::arith::pivotTime")
{
StatisticsRegistry::registerStat(&d_statPivots);
StatisticsRegistry::registerStat(&d_statUpdates);
@@ -33,6 +36,10 @@ SimplexDecisionProcedure::Statistics::Statistics():
StatisticsRegistry::registerStat(&d_statEarlyConflicts);
StatisticsRegistry::registerStat(&d_statEarlyConflictImprovements);
StatisticsRegistry::registerStat(&d_selectInitialConflictTime);
+
+ StatisticsRegistry::registerStat(&d_pivotsAfterConflict);
+ StatisticsRegistry::registerStat(&d_checksWithWastefulPivots);
+ StatisticsRegistry::registerStat(&d_pivotTime);
}
SimplexDecisionProcedure::Statistics::~Statistics(){
@@ -46,10 +53,15 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_statEarlyConflicts);
StatisticsRegistry::unregisterStat(&d_statEarlyConflictImprovements);
StatisticsRegistry::unregisterStat(&d_selectInitialConflictTime);
+
+ StatisticsRegistry::unregisterStat(&d_pivotsAfterConflict);
+ StatisticsRegistry::unregisterStat(&d_checksWithWastefulPivots);
+ StatisticsRegistry::unregisterStat(&d_pivotTime);
}
void SimplexDecisionProcedure::ejectInactiveVariables(){
+ return; //die die die
for(ArithVarSet::iterator i = d_tableau.begin(), end = d_tableau.end(); i != end;){
ArithVar variable = *i;
@@ -247,6 +259,32 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
Assert(x_i != x_j);
+ TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime);
+
+ if(Debug.isOn("arith::pivotAndUpdate")){
+ Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl;
+ ReducedRowVector* row_k = d_tableau.lookup(x_i);
+ for(ReducedRowVector::NonZeroIterator varIter = row_k->beginNonZero();
+ varIter != row_k->endNonZero();
+ ++varIter){
+
+ ArithVar var = varIter->first;
+ const Rational& coeff = varIter->second;
+ DeltaRational beta = d_partialModel.getAssignment(var);
+ Debug("arith::pivotAndUpdate") << var << beta << coeff;
+ if(d_partialModel.hasLowerBound(var)){
+ Debug("arith::pivotAndUpdate") << "(lb " << d_partialModel.getLowerBound(var) << ")";
+ }
+ if(d_partialModel.hasUpperBound(var)){
+ Debug("arith::pivotAndUpdate") << "(up " << d_partialModel.getUpperBound(var)
+ << ")";
+ }
+ Debug("arith::pivotAndUpdate") << endl;
+ }
+ Debug("arith::pivotAndUpdate") << "end row"<< endl;
+ }
+
+
ReducedRowVector* row_i = d_tableau.lookup(x_i);
const Rational& a_ij = row_i->lookup(x_j);
@@ -279,11 +317,35 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
}
}
+ // Pivots
++(d_statistics.d_statPivots);
+ if( d_foundAConflict ){
+ ++d_pivotsSinceConflict;
+ if(d_pivotsSinceConflict == 1){
+ ++(d_statistics.d_checksWithWastefulPivots);
+ }
+ ++(d_statistics.d_pivotsAfterConflict);
+ }
+
d_tableau.pivot(x_i, x_j);
checkBasicVariable(x_j);
+ // Debug found conflict
+ if( !d_foundAConflict ){
+ DeltaRational beta_j = d_partialModel.getAssignment(x_j);
+
+ if(d_partialModel.belowLowerBound(x_j, beta_j, true)){
+ if(selectSlackBelow(x_j) == ARITHVAR_SENTINEL ){
+ d_foundAConflict = true;
+ }
+ }else if(d_partialModel.aboveUpperBound(x_j, beta_j, true)){
+ if(selectSlackAbove(x_j) == ARITHVAR_SENTINEL ){
+ d_foundAConflict = true;
+ }
+ }
+ }
+
if(Debug.isOn("tableau")){
d_tableau.printTableau();
}
@@ -364,7 +426,8 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
}else{
slack = nonbasic; break;
}
- }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){if(d_pivotStage){
+ }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
+ if(d_pivotStage){
if(d_tableau.getRowCount(nonbasic) < numRows){
slack = nonbasic;
numRows = d_tableau.getRowCount(nonbasic);
@@ -409,26 +472,15 @@ Node SimplexDecisionProcedure::selectInitialConflict() {
ArithVar x_i = (*i).first;
d_griggioRuleQueue.push(*i);
- DeltaRational beta_i = d_partialModel.getAssignment(x_i);
+ Node possibleConflict = checkBasicForConflict(x_i);
+ if(!possibleConflict.isNull()){
+ Node better = betterConflict(bestConflict, possibleConflict);
- if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
- DeltaRational l_i = d_partialModel.getLowerBound(x_i);
- ArithVar x_j = selectSlackBelow(x_i);
- if(x_j == ARITHVAR_SENTINEL ){
- Node better = betterConflict(bestConflict, generateConflictBelow(x_i));
- if(better != bestConflict) ++conflictChanges;
- bestConflict = better;
- ++(d_statistics.d_statEarlyConflicts);
- }
- }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
- DeltaRational u_i = d_partialModel.getUpperBound(x_i);
- ArithVar x_j = selectSlackAbove(x_i);
- if(x_j == ARITHVAR_SENTINEL ){
- Node better = betterConflict(bestConflict, generateConflictAbove(x_i));
- if(better != bestConflict) ++conflictChanges;
- bestConflict = better;
- ++(d_statistics.d_statEarlyConflicts);
+ if(better != bestConflict){
+ ++conflictChanges;
}
+ bestConflict = better;
+ ++(d_statistics.d_statEarlyConflicts);
}
}
if(conflictChanges > 1) ++(d_statistics.d_statEarlyConflictImprovements);
@@ -438,7 +490,13 @@ Node SimplexDecisionProcedure::selectInitialConflict() {
Node SimplexDecisionProcedure::updateInconsistentVars(){
if(d_griggioRuleQueue.empty()) return Node::null();
- Node possibleConflict = selectInitialConflict();
+ d_foundAConflict = false;
+ d_pivotsSinceConflict = 0;
+
+ Node possibleConflict = Node::null();
+ if(d_griggioRuleQueue.size() > 1){
+ possibleConflict = selectInitialConflict();
+ }
if(possibleConflict.isNull()){
possibleConflict = privateUpdateInconsistentVars();
}
@@ -457,6 +515,25 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
return possibleConflict;
}
+Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
+
+ Assert(d_basicManager.isMember(basic));
+ const DeltaRational& beta = d_partialModel.getAssignment(basic);
+
+ if(d_partialModel.belowLowerBound(basic, beta, true)){
+ ArithVar x_j = selectSlackBelow(basic);
+ if(x_j == ARITHVAR_SENTINEL ){
+ return generateConflictBelow(basic);
+ }
+ }else if(d_partialModel.aboveUpperBound(basic, beta, true)){
+ ArithVar x_j = selectSlackAbove(basic);
+ if(x_j == ARITHVAR_SENTINEL ){
+ return generateConflictAbove(basic);
+ }
+ }
+ return Node::null();
+}
+
//corresponds to Check() in dM06
Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
Assert(d_pivotStage || d_griggioRuleQueue.empty());
@@ -470,7 +547,7 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
ArithVar x_i = selectSmallestInconsistentVar();
- Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
+ Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
if(x_i == ARITHVAR_SENTINEL){
Debug("arith_update") << "No inconsistent variables" << endl;
return Node::null(); //sat
@@ -481,10 +558,11 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
ejectInactiveVariables();
DeltaRational beta_i = d_partialModel.getAssignment(x_i);
+ ArithVar x_j = ARITHVAR_SENTINEL;
if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
DeltaRational l_i = d_partialModel.getLowerBound(x_i);
- ArithVar x_j = selectSlackBelow(x_i);
+ x_j = selectSlackBelow(x_i);
if(x_j == ARITHVAR_SENTINEL ){
++(d_statistics.d_statUpdateConflicts);
return generateConflictBelow(x_i); //unsat
@@ -493,13 +571,19 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
}else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
DeltaRational u_i = d_partialModel.getUpperBound(x_i);
- ArithVar x_j = selectSlackAbove(x_i);
+ x_j = selectSlackAbove(x_i);
if(x_j == ARITHVAR_SENTINEL ){
++(d_statistics.d_statUpdateConflicts);
return generateConflictAbove(x_i); //unsat
}
pivotAndUpdate(x_i, x_j, u_i);
}
+ Assert(x_j != ARITHVAR_SENTINEL);
+ //Check to see if we already have a conflict with x_j to prevent wasteful work
+ Node earlyConflict = checkBasicForConflict(x_j);
+ if(!earlyConflict.isNull()){
+ return earlyConflict;
+ }
}
if(d_pivotStage && iteratationNum >= d_numVariables){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback