diff options
Diffstat (limited to 'src/theory/arith/soi_simplex.cpp')
-rw-r--r-- | src/theory/arith/soi_simplex.cpp | 129 |
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){ |