summaryrefslogtreecommitdiff
path: root/src/theory/arith/soi_simplex.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/soi_simplex.cpp')
-rw-r--r--src/theory/arith/soi_simplex.cpp129
1 files changed, 87 insertions, 42 deletions
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 34f911b81..0d07c5ffc 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -634,12 +634,16 @@ unsigned SumOfInfeasibilitiesSPD::trySet(const ArithVarVec& set){
}
std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
+ Debug("arith::greedyConflictSubsets") << "greedyConflictSubsets start" << endl;
+
std::vector< ArithVarVec > subsets;
Assert(d_soiVar == ARITHVAR_SENTINEL);
if(d_errorSize <= 2){
ArithVarVec inError;
d_errorSet.pushFocusInto(inError);
+
+ Assert(debugIsASet(inError));
subsets.push_back(inError);
return subsets;
}
@@ -653,9 +657,11 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
ArithVar e = *iter;
addRowSgns(sgns, e, d_errorSet.getSgn(e));
- //cout << "basic error var: " << e << endl;
- //d_tableau.debugPrintIsBasic(e);
- //d_tableau.printBasicRow(e, cout);
+ Debug("arith::greedyConflictSubsets") << "basic error var: " << e << endl;
+ if(Debug.isOn("arith::greedyConflictSubsets")){
+ d_tableau.debugPrintIsBasic(e);
+ d_tableau.printBasicRow(e, Debug("arith::greedyConflictSubsets"));
+ }
}
// Phase 1: Try to find at least 1 pair for every element
@@ -683,9 +689,10 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
tmp[0] = e;
tmp[1] = b;
if(trySet(tmp) == 2){
- //cout << "found a pair" << endl;
+ Debug("arith::greedyConflictSubsets") << "found a pair " << b << " " << e << endl;
hasParticipated.softAdd(b);
hasParticipated.softAdd(e);
+ Assert(debugIsASet(tmp));
subsets.push_back(tmp);
++(d_statistics.d_soiConflicts);
++(d_statistics.d_hasToBeMinimal);
@@ -704,13 +711,15 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
possibleStarts.pop_back();
if(hasParticipated.isMember(v)){ continue; }
+ hasParticipated.add(v);
+
Assert(d_soiVar == ARITHVAR_SENTINEL);
//d_soiVar's row = \sumofinfeasibilites underConstruction
ArithVarVec underConstruction;
underConstruction.push_back(v);
d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, v);
- //cout << "trying " << v << endl;
+ Debug("arith::greedyConflictSubsets") << "trying " << v << endl;
const Tableau::Entry* spoiler = NULL;
while( (spoiler = d_linEq.selectSlackEntry(d_soiVar, false)) != NULL){
@@ -718,16 +727,16 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
int oppositeSgn = -(spoiler->getCoefficient().sgn());
Assert(oppositeSgn != 0);
- //cout << "looking for " << nb << " " << oppositeSgn << endl;
+ Debug("arith::greedyConflictSubsets") << "looking for " << nb << " " << oppositeSgn << endl;
ArithVar basicWithOp = find_basic_in_sgns(sgns, nb, oppositeSgn, hasParticipated, false);
if(basicWithOp == ARITHVAR_SENTINEL){
- //cout << "search did not work for " << nb << endl;
+ Debug("arith::greedyConflictSubsets") << "search did not work for " << nb << endl;
// greedy construction has failed
break;
}else{
- //cout << "found " << basicWithOp << endl;
+ Debug("arith::greedyConflictSubsets") << "found " << basicWithOp << endl;
addToInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, basicWithOp);
hasParticipated.softAdd(basicWithOp);
@@ -735,8 +744,9 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
}
}
if(spoiler == NULL){
- //cout << "success" << endl;
+ Debug("arith::greedyConflictSubsets") << "success" << endl;
//then underConstruction contains a conflicting subset
+ Assert(debugIsASet(underConstruction));
subsets.push_back(underConstruction);
++d_statistics.d_soiConflicts;
if(underConstruction.size() == 3){
@@ -745,7 +755,7 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
++d_statistics.d_maybeNotMinimal;
}
}else{
- //cout << "failure" << endl;
+ Debug("arith::greedyConflictSubsets") << "failure" << endl;
}
tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
d_soiVar = ARITHVAR_SENTINEL;
@@ -762,52 +772,89 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
Assert(d_soiVar == ARITHVAR_SENTINEL);
+ Debug("arith::greedyConflictSubsets") << "greedyConflictSubsets done" << endl;
return subsets;
}
-void SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){
+bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){
Assert(d_soiVar == ARITHVAR_SENTINEL);
d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, subset);
+ Assert(!subset.empty());
+ Assert(!d_conflictBuilder->underConstruction());
+
+ Debug("arith::generateSOIConflict") << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) start" << endl;
- //NodeBuilder<> conflict(kind::AND);
+ bool success = false;
+
for(ArithVarVec::const_iterator iter = subset.begin(), end = subset.end(); iter != end; ++iter){
ArithVar e = *iter;
ConstraintP violated = d_errorSet.getViolated(e);
- //cout << "basic error var: " << violated << endl;
- d_conflictChannel.addConstraint(violated);
- //violated->explainForConflict(conflict);
+ Assert(violated != NullConstraint);
- //d_tableau.debugPrintIsBasic(e);
- //d_tableau.printBasicRow(e, cout);
- }
- for(Tableau::RowIterator i = d_tableau.basicRowIterator(d_soiVar); !i.atEnd(); ++i){
- const Tableau::Entry& entry = *i;
- ArithVar v = entry.getColVar();
- if(v == d_soiVar){ continue; }
- const Rational& coeff = entry.getCoefficient();
- ConstraintP c = (coeff.sgn() > 0) ?
- d_variables.getUpperBoundConstraint(v) :
- d_variables.getLowerBoundConstraint(v);
+ int sgn = d_errorSet.getSgn(e);
+ const Rational& violatedCoeff = sgn > 0 ? d_negOne : d_posOne;
+ Debug("arith::generateSOIConflict") << "basic error var: "
+ << "(" << violatedCoeff << ")"
+ << " " << violated
+ << endl;
- //cout << "nb : " << c << endl;
- d_conflictChannel.addConstraint(c);
+
+ d_conflictBuilder->addConstraint(violated, violatedCoeff);
+ Assert(violated->hasProof());
+ if(!success && !violated->negationHasProof()){
+ success = true;
+ d_conflictBuilder->makeLastConsequent();
+ }
+ }
+
+ if(!success){
+ // failure
+ d_conflictBuilder->reset();
+ } else {
+ // pick a violated constraint arbitrarily. any of them may be selected for the conflict
+ Assert(d_conflictBuilder->underConstruction());
+ Assert(d_conflictBuilder->consequentIsSet());
+
+ for(Tableau::RowIterator i = d_tableau.basicRowIterator(d_soiVar); !i.atEnd(); ++i){
+ const Tableau::Entry& entry = *i;
+ ArithVar v = entry.getColVar();
+ if(v == d_soiVar){ continue; }
+ const Rational& coeff = entry.getCoefficient();
+
+ ConstraintP c = (coeff.sgn() > 0) ?
+ d_variables.getUpperBoundConstraint(v) :
+ d_variables.getLowerBoundConstraint(v);
+
+ Debug("arith::generateSOIConflict") << "non-basic var: "
+ << "(" << coeff << ")"
+ << " " << c
+ << endl;
+ d_conflictBuilder->addConstraint(c, coeff);
+ }
+ ConstraintCP conflicted = d_conflictBuilder->commitConflict();
+ d_conflictChannel.raiseConflict(conflicted);
}
- //Node conf = conflict;
tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
d_soiVar = ARITHVAR_SENTINEL;
- d_conflictChannel.commitConflict();
- //return conf;
+ Debug("arith::generateSOIConflict") << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) done" << endl;
+ Assert(d_soiVar == ARITHVAR_SENTINEL);
+ Assert(!d_conflictBuilder->underConstruction());
+ return success;
}
WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
static int instance = 0;
instance++;
- //cout << "SOI conflict " << instance << ": |E| = " << d_errorSize << endl;
- //d_errorSet.debugPrint(cout);
- //cout << endl;
+
+ Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() start "
+ << instance << ": |E| = " << d_errorSize << endl;
+ if(Debug.isOn("arith::SOIConflict")){
+ d_errorSet.debugPrint(cout);
+ }
+ Debug("arith::SOIConflict") << endl;
tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
d_soiVar = ARITHVAR_SENTINEL;
@@ -815,24 +862,22 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
if(options::soiQuickExplain()){
quickExplain();
generateSOIConflict(d_qeConflict);
- //Node conflict = generateSOIConflict(d_qeConflict);
- //cout << conflict << endl;
- //d_conflictChannel(conflict);
}else{
-
vector<ArithVarVec> subsets = greedyConflictSubsets();
Assert( d_soiVar == ARITHVAR_SENTINEL);
-
+ bool anySuccess = false;
Assert(!subsets.empty());
for(vector<ArithVarVec>::const_iterator i = subsets.begin(), end = subsets.end(); i != end; ++i){
const ArithVarVec& subset = *i;
- generateSOIConflict(subset);
+ Assert(debugIsASet(subset));
+ anySuccess = generateSOIConflict(subset) || anySuccess;
//Node conflict = generateSOIConflict(subset);
//cout << conflict << endl;
//reportConflict(conf); do not do this. We need a custom explanations!
//d_conflictChannel(conflict);
}
+ Assert(anySuccess);
}
Assert( d_soiVar == ARITHVAR_SENTINEL);
d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization);
@@ -840,7 +885,8 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
//reportConflict(conf); do not do this. We need a custom explanations!
d_conflictVariables.add(d_soiVar);
- //cout << "SOI conflict " << instance << "end" << endl;
+ Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() done "
+ << instance << "end" << endl;
return ConflictFound;
}
@@ -877,7 +923,6 @@ WitnessImprovement SumOfInfeasibilitiesSPD::soiRound() {
}
bool SumOfInfeasibilitiesSPD::debugSOI(WitnessImprovement w, ostream& out, int instance) const{
-//#warning "Redo SOI"
return true;
// out << "DLV("<<instance<<") ";
// switch(w){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback