diff options
| -rw-r--r-- | src/theory/arith/options | 3 | ||||
| -rw-r--r-- | src/theory/arith/simplex.cpp | 10 | ||||
| -rw-r--r-- | src/theory/arith/simplex.h | 4 | ||||
| -rw-r--r-- | src/theory/arith/soi_simplex.cpp | 241 | ||||
| -rw-r--r-- | src/theory/arith/soi_simplex.h | 13 |
5 files changed, 234 insertions, 37 deletions
diff --git a/src/theory/arith/options b/src/theory/arith/options index 977d6cb32..388dcc7ff 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -91,4 +91,7 @@ option fancyFinal --fancy-final bool :default false :read-write option exportDioDecompositions --dio-decomps bool :default false :read-write Let skolem variables for integer divisibility constraints leak from the dio solver. +option soiQuickExplain --soi-qe bool :default false :read-write + Use quick explain to minimize the sum of infeasibility conflicts. + endmodule diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 02e49258c..06ec0312d 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -168,6 +168,12 @@ void SimplexDecisionProcedure::addToInfeasFunc(TimerStat& timer, ArithVar inf, A adjustInfeasFunc(timer, inf, justE); } +void SimplexDecisionProcedure::removeFromInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e){ + AVIntPairVec justE; + int opSgn = -d_errorSet.getSgn(e); + justE.push_back(make_pair(e, opSgn)); + adjustInfeasFunc(timer, inf, justE); +} ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set){ TimerStat::CodeTimer codeTimer(timer); @@ -226,7 +232,7 @@ void SimplexDecisionProcedure::addRowSgns(sgn_table& sgns, ArithVar basic, int n } } -ArithVar SimplexDecisionProcedure::find_basic_outside(const sgn_table& sgns, ArithVar col, int sgn, const DenseSet& m){ +ArithVar SimplexDecisionProcedure::find_basic_in_sgns(const sgn_table& sgns, ArithVar col, int sgn, const DenseSet& m, bool inside){ pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn)); sgn_table::const_iterator i = sgns.find(p); @@ -234,7 +240,7 @@ ArithVar SimplexDecisionProcedure::find_basic_outside(const sgn_table& sgns, Ari const ArithVarVec& vec = (*i).second; for(ArithVarVec::const_iterator viter = vec.begin(), vend = vec.end(); viter != vend; ++viter){ ArithVar curr = *viter; - if(!m.isMember(curr)){ + if(inside == m.isMember(curr)){ return curr; } } diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index bc47a128a..d646ca889 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -121,6 +121,7 @@ protected: void tearDownInfeasiblityFunction(TimerStat& timer, ArithVar inf); void adjustInfeasFunc(TimerStat& timer, ArithVar inf, const AVIntPairVec& focusChanges); void addToInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e); + void removeFromInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e); void shrinkInfeasFunc(TimerStat& timer, ArithVar inf, const ArithVarVec& dropped); public: @@ -197,7 +198,8 @@ protected: void addSgn(sgn_table& sgns, ArithVar col, int sgn, ArithVar basic); void addRowSgns(sgn_table& sgns, ArithVar basic, int norm); - ArithVar find_basic_outside(const sgn_table& sgns, ArithVar col, int sgn, const DenseSet& m); + ArithVar find_basic_in_sgns(const sgn_table& sgns, ArithVar col, int sgn, const DenseSet& m, bool inside); + sgn_table::const_iterator find_sgns(const sgn_table& sgns, ArithVar col, int sgn); };/* class SimplexDecisionProcedure */ diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index f19b13fa5..a5c7c712d 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -22,6 +22,8 @@ #include "util/statistics_registry.h" +#include <algorithm> + using namespace std; namespace CVC4 { @@ -433,6 +435,192 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes adjustFocusAndError(selected, focusChanges); } +void SumOfInfeasibilitiesSPD::qeAddRange(uint32_t begin, uint32_t end){ + Assert(!d_qeInSoi.empty()); + for(uint32_t i = begin; i != end; ++i){ + ArithVar v = d_qeConflict[i]; + addToInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, v); + d_qeInSoi.add(v); + } +} + +void SumOfInfeasibilitiesSPD::qeRemoveRange(uint32_t begin, uint32_t end){ + for(uint32_t i = begin; i != end; ++i){ + ArithVar v = d_qeConflict[i]; + removeFromInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, v); + d_qeInSoi.remove(v); + } + Assert(!d_qeInSoi.empty()); +} + +void SumOfInfeasibilitiesSPD::qeSwapRange(uint32_t N, uint32_t r, uint32_t s){ + for(uint32_t i = 0; i < N; ++i){ + std::swap(d_qeConflict[r+i], d_qeConflict[s+i]); + } +} + +/** + * Region notation: + * A region is either + * - A single element X@i with the name X at the position i + * - A sequence of indices X@[i,j) with the name X and the elements between i [inclusive] and j exclusive + * - A concatenation of regions R1 and R2, R1;R2 + * + * Given the fixed assumptions C @ [0,cEnd) and a set of candidate minimizations U@[cEnd, uEnd) + * s.t. C \cup U is known to be in conflict ([0,uEnd) has a conflict), find a minimal + * subset of U, Delta, s.t. C \cup Delta is in conflict. + * + * Pre: + * [0, uEnd) is a set and is in conflict. + * uEnd <= assumptions.size() + * [0, cEnd) is in d_inSoi. + * + * Invariants: [0,cEnd) is never modified + * + * Post: + * [0, cEnd); [cEnd, deltaEnd) is in conflict + * [0, deltaEnd) is a set + * [0, deltaEnd) is in d_inSoi + */ +uint32_t SumOfInfeasibilitiesSPD::quickExplainRec(uint32_t cEnd, uint32_t uEnd){ + Assert(cEnd <= uEnd); + Assert(d_qeInUAndNotInSoi.empty()); + Assert(d_qeGreedyOrder.empty()); + + const Tableau::Entry* spoiler = NULL; + + if(d_soiVar != ARITHVAR_SENTINEL && d_linEq.selectSlackEntry(d_soiVar, false) == NULL){ + // already in conflict + return cEnd; + } + + Assert(cEnd < uEnd); + + // Phase 1 : Construct the conflict greedily + + for(uint32_t i = cEnd; i < uEnd; ++i){ + d_qeInUAndNotInSoi.add(d_qeConflict[i]); + } + if(d_soiVar == ARITHVAR_SENTINEL){ // special case for d_soiVar being empty + ArithVar first = d_qeConflict[cEnd]; + d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, first); + d_qeInSoi.add(first); + d_qeInUAndNotInSoi.remove(first); + d_qeGreedyOrder.push_back(first); + } + while((spoiler = d_linEq.selectSlackEntry(d_soiVar, false)) != NULL){ + Assert(!d_qeInUAndNotInSoi.empty()); + + ArithVar nb = spoiler->getColVar(); + int oppositeSgn = -(spoiler->getCoefficient().sgn()); + Assert(oppositeSgn != 0); + + ArithVar basicWithOp = find_basic_in_sgns(d_qeSgns, nb, oppositeSgn, d_qeInUAndNotInSoi, true); + Assert(basicWithOp != ARITHVAR_SENTINEL); + + addToInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, basicWithOp); + d_qeInSoi.add(basicWithOp); + d_qeInUAndNotInSoi.remove(basicWithOp); + d_qeGreedyOrder.push_back(basicWithOp); + } + Assert(spoiler == NULL); + + // Compact the set u + uint32_t newEnd = cEnd + d_qeGreedyOrder.size(); + std::copy(d_qeGreedyOrder.begin(), d_qeGreedyOrder.end(), d_qeConflict.begin()+cEnd); + + d_qeInUAndNotInSoi.purge(); + d_qeGreedyOrder.clear(); + + // Phase 2 : Recursively determine the minimal set of rows + + uint32_t xPos = cEnd; + std::swap(d_qeGreedyOrder[xPos], d_qeGreedyOrder[newEnd - 1]); + uint32_t uBegin = xPos + 1; + uint32_t split = (newEnd - uBegin)/2 + uBegin; + + //assumptions : C @ [0, cEnd); X @ xPos; U1 @ [u1Begin, split); U2 @ [split, newEnd) + // [0, newEnd) == d_inSoi + + uint32_t compactU2; + if(split == newEnd){ // U2 is empty + compactU2 = newEnd; + }else{ + // Remove U2 from Soi + qeRemoveRange(split, newEnd); + // [0, split) == d_inSoi + + // pre assumptions: C + X + U1 @ [0,split); U2 [split, newEnd) + compactU2 = quickExplainRec(split, newEnd); + // post: + // assumptions: C + X + U1 @ [0, split); delta2 @ [split - compactU2) + // d_inSoi = [0, compactU2) + } + uint32_t deltaSize = compactU2 - split; + qeSwapRange(deltaSize, uBegin, split); + uint32_t d2End = uBegin+deltaSize; + // assumptions : C @ [0, cEnd); X @ xPos; delta2 @ [uBegin, d2End); U1 @ [d2End, compactU2) + // d_inSoi == [0, compactU2) + + uint32_t d1End; + if(d2End == compactU2){ // U1 is empty + d1End = d2End; + }else{ + qeRemoveRange(d2End, compactU2); + + //pre assumptions : C + X + delta2 @ [0, d2End); U1 @ [d2End, compactU2); + d1End = quickExplainRec(d2End, compactU2); + //post: + // assumptions : C + X + delta2 @ [0, d2End); delta1 @ [d2End, d1End); + // d_inSoi = [0, d1End) + } + //After both: + // d_inSoi == [0, d1End), C @ [0, cEnd); X + delta2 + delta 1 @ [xPos, d1End); + + Assert(d_qeInUAndNotInSoi.empty()); + Assert(d_qeGreedyOrder.empty()); + return d1End; +} + +void SumOfInfeasibilitiesSPD::quickExplain(){ + Assert(d_qeInSoi.empty()); + Assert(d_soiVar.empty()); + Assert(d_qeGreedyOrder.empty()); + Assert(d_soiVar == ARITHVAR_SENTINEL); + Assert(d_qeSgns.empty()); + + d_qeConflict.clear(); + d_errorSet.pushFocusInto(d_qeConflict); + + cout << d_qeConflict.size() << " "; + uint32_t size = d_qeConflict.size(); + + if(size > 2){ + for(ErrorSet::focus_iterator iter = d_errorSet.focusBegin(), end = d_errorSet.focusEnd(); iter != end; ++iter){ + ArithVar e = *iter; + addRowSgns(d_qeSgns, e, d_errorSet.getSgn(e)); + } + uint32_t end = quickExplainRec(0u, size); + Assert(end <= d_qeConflict.size()); + Assert(d_soiVar != ARITHVAR_SENTINEL); + Assert(!d_qeInSoi.empty()); + + d_qeConflict.resize(end); + tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar); + d_soiVar = ARITHVAR_SENTINEL; + d_qeInSoi.purge(); + d_qeSgns.clear(); + } + + cout << d_qeConflict.size() << endl; + + Assert(d_qeInSoi.empty()); + Assert(d_soiVar.empty()); + Assert(d_qeGreedyOrder.empty()); + Assert(d_soiVar == ARITHVAR_SENTINEL); + Assert(d_qeSgns.empty()); +} + unsigned SumOfInfeasibilitiesSPD::trySet(const ArithVarVec& set){ Assert(d_soiVar == ARITHVAR_SENTINEL); bool success = false; @@ -446,30 +634,6 @@ unsigned SumOfInfeasibilitiesSPD::trySet(const ArithVarVec& set){ return success ? set.size() : std::numeric_limits<int>::max(); } -unsigned SumOfInfeasibilitiesSPD::tryAllSubsets(const ArithVarVec& set, unsigned depth, ArithVarVec& tmp) { - if(depth < set.size()){ - unsigned resWithout = tryAllSubsets(set, depth+1, tmp); - if(resWithout == tmp.size() && resWithout < set.size()){ - for(unsigned i = 0; i < tmp.size(); ++i){ - cout << tmp[i] << " "; - } - cout << endl; - } - tmp.push_back(set[depth]); - unsigned resWith = tryAllSubsets(set, depth+1, tmp); - if(resWith == tmp.size() && resWith < set.size()){ - for(unsigned i = 0; i < tmp.size(); ++i){ - cout << tmp[i] << " "; - } - cout << endl; - } - tmp.pop_back(); - return std::min(resWith, resWithout); - }else{ - return trySet(tmp); - } -} - std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){ std::vector< ArithVarVec > subsets; Assert(d_soiVar == ARITHVAR_SENTINEL); @@ -559,7 +723,7 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){ //cout << "looking for " << nb << " " << oppositeSgn << endl; - ArithVar basicWithOp = find_basic_outside(sgns, nb, oppositeSgn, hasParticipated); + ArithVar basicWithOp = find_basic_in_sgns(sgns, nb, oppositeSgn, hasParticipated, false); if(basicWithOp == ARITHVAR_SENTINEL){ //cout << "search did not work for " << nb << endl; @@ -648,17 +812,26 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){ tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar); d_soiVar = ARITHVAR_SENTINEL; - vector<ArithVarVec> subsets = greedyConflictSubsets(); - Assert( d_soiVar == ARITHVAR_SENTINEL); - Assert(!subsets.empty()); - for(vector<ArithVarVec>::const_iterator i = subsets.begin(), end = subsets.end(); i != end; ++i){ - const ArithVarVec& subset = *i; - Node conflict = generateSOIConflict(subset); - //cout << conflict << endl; - - //reportConflict(conf); do not do this. We need a custom explanations! + if(options::soiQuickExplain()){ + quickExplain(); + Node conflict = generateSOIConflict(d_qeConflict); + cout << conflict << endl; d_conflictChannel(conflict); + }else{ + + vector<ArithVarVec> subsets = greedyConflictSubsets(); + Assert( d_soiVar == ARITHVAR_SENTINEL); + + Assert(!subsets.empty()); + for(vector<ArithVarVec>::const_iterator i = subsets.begin(), end = subsets.end(); i != end; ++i){ + const ArithVarVec& subset = *i; + Node conflict = generateSOIConflict(subset); + //cout << conflict << endl; + + //reportConflict(conf); do not do this. We need a custom explanations! + d_conflictChannel(conflict); + } } Assert( d_soiVar == ARITHVAR_SENTINEL); d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization); diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index 1a6becccb..86b9276ed 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -193,6 +193,19 @@ private: IntStat& conflictStat = d_statistics.d_initialConflicts; return standardProcessSignals(timer, conflictStat); } + + void quickExplain(); + DenseSet d_qeInSoi; + DenseSet d_qeInUAndNotInSoi; + ArithVarVec d_qeConflict; + ArithVarVec d_qeGreedyOrder; + sgn_table d_qeSgns; + + uint32_t quickExplainRec(uint32_t cEnd, uint32_t uEnd); + void qeAddRange(uint32_t begin, uint32_t end); + void qeRemoveRange(uint32_t begin, uint32_t end); + void qeSwapRange(uint32_t N, uint32_t r, uint32_t s); + unsigned trySet(const ArithVarVec& set); unsigned tryAllSubsets(const ArithVarVec& set, unsigned depth, ArithVarVec& tmp); |