1 /********************* */
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): mdeters
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
19 #include "theory/arith/soi_simplex.h"
20 #include "theory/arith/options.h"
21 #include "theory/arith/constraint.h"
23 #include "util/statistics_registry.h"
34 SumOfInfeasibilitiesSPD::SumOfInfeasibilitiesSPD(LinearEqualityModule
& linEq
, ErrorSet
& errors
, RaiseConflict conflictChannel
, TempVarMalloc tvmalloc
)
35 : SimplexDecisionProcedure(linEq
, errors
, conflictChannel
, tvmalloc
)
36 , d_soiVar(ARITHVAR_SENTINEL
)
38 , d_prevWitnessImprovement(AntiProductive
)
39 , d_witnessImprovementInARow(0)
40 , d_sgnDisagreements()
41 , d_statistics(d_pivots
)
44 SumOfInfeasibilitiesSPD::Statistics::Statistics(uint32_t& pivots
):
45 d_initialSignalsTime("theory::arith::SOI::initialProcessTime"),
46 d_initialConflicts("theory::arith::SOI::UpdateConflicts", 0),
47 d_soiFoundUnsat("theory::arith::SOI::FoundUnsat", 0),
48 d_soiFoundSat("theory::arith::SOI::FoundSat", 0),
49 d_soiMissed("theory::arith::SOI::Missed", 0),
50 d_soiConflicts("theory::arith::SOI::ConfMin::num", 0),
51 d_hasToBeMinimal("theory::arith::SOI::HasToBeMin", 0),
52 d_maybeNotMinimal("theory::arith::SOI::MaybeNotMin", 0),
53 d_soiTimer("theory::arith::SOI::Time"),
54 d_soiFocusConstructionTimer("theory::arith::SOI::Construction"),
55 d_soiConflictMinimization("theory::arith::SOI::Conflict::Minimization"),
56 d_selectUpdateForSOI("theory::arith::SOI::selectSOI"),
57 d_finalCheckPivotCounter("theory::arith::SOI::lastPivots", pivots
)
59 StatisticsRegistry::registerStat(&d_initialSignalsTime
);
60 StatisticsRegistry::registerStat(&d_initialConflicts
);
62 StatisticsRegistry::registerStat(&d_soiFoundUnsat
);
63 StatisticsRegistry::registerStat(&d_soiFoundSat
);
64 StatisticsRegistry::registerStat(&d_soiMissed
);
66 StatisticsRegistry::registerStat(&d_soiConflicts
);
67 StatisticsRegistry::registerStat(&d_hasToBeMinimal
);
68 StatisticsRegistry::registerStat(&d_maybeNotMinimal
);
70 StatisticsRegistry::registerStat(&d_soiTimer
);
71 StatisticsRegistry::registerStat(&d_soiFocusConstructionTimer
);
73 StatisticsRegistry::registerStat(&d_soiConflictMinimization
);
75 StatisticsRegistry::registerStat(&d_selectUpdateForSOI
);
77 StatisticsRegistry::registerStat(&d_finalCheckPivotCounter
);
80 SumOfInfeasibilitiesSPD::Statistics::~Statistics(){
81 StatisticsRegistry::unregisterStat(&d_initialSignalsTime
);
82 StatisticsRegistry::unregisterStat(&d_initialConflicts
);
84 StatisticsRegistry::unregisterStat(&d_soiFoundUnsat
);
85 StatisticsRegistry::unregisterStat(&d_soiFoundSat
);
86 StatisticsRegistry::unregisterStat(&d_soiMissed
);
88 StatisticsRegistry::unregisterStat(&d_soiConflicts
);
89 StatisticsRegistry::unregisterStat(&d_hasToBeMinimal
);
90 StatisticsRegistry::unregisterStat(&d_maybeNotMinimal
);
92 StatisticsRegistry::unregisterStat(&d_soiTimer
);
93 StatisticsRegistry::unregisterStat(&d_soiFocusConstructionTimer
);
95 StatisticsRegistry::unregisterStat(&d_soiConflictMinimization
);
97 StatisticsRegistry::unregisterStat(&d_selectUpdateForSOI
);
98 StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter
);
101 Result::Sat
SumOfInfeasibilitiesSPD::findModel(bool exactResult
){
102 Assert(d_conflictVariables
.empty());
103 Assert(d_sgnDisagreements
.empty());
106 static CVC4_THREADLOCAL(unsigned int) instance
= 0;
107 instance
= instance
+ 1;
108 static const bool verbose
= false;
110 if(d_errorSet
.errorEmpty() && !d_errorSet
.moreSignals()){
111 Debug("soi::findModel") << "soiFindModel("<< instance
<<") trivial" << endl
;
112 Assert(d_conflictVariables
.empty());
116 // We need to reduce this because of
117 d_errorSet
.reduceToSignals();
119 // We must start tracking NOW
120 d_errorSet
.setSelectionRule(SUM_METRIC
);
122 if(initialProcessSignals()){
123 d_conflictVariables
.purge();
124 if(verbose
){ Message() << "fcFindModel("<< instance
<<") early conflict" << endl
; }
125 Debug("soi::findModel") << "fcFindModel("<< instance
<<") early conflict" << endl
;
126 Assert(d_conflictVariables
.empty());
127 return Result::UNSAT
;
128 }else if(d_errorSet
.errorEmpty()){
129 Debug("soi::findModel") << "fcFindModel("<< instance
<<") fixed itself" << endl
;
130 Assert(!d_errorSet
.moreSignals());
131 Assert(d_conflictVariables
.empty());
135 Debug("soi::findModel") << "fcFindModel(" << instance
<<") start non-trivial" << endl
;
137 exactResult
|= options::arithStandardCheckVarOrderPivots() < 0;
139 d_prevWitnessImprovement
= HeuristicDegenerate
;
140 d_witnessImprovementInARow
= 0;
142 Result::Sat result
= Result::SAT_UNKNOWN
;
144 if(result
== Result::SAT_UNKNOWN
){
148 d_pivotBudget
= options::arithStandardCheckVarOrderPivots();
151 result
= sumOfInfeasibilities();
153 if(result
== Result::UNSAT
){
154 ++(d_statistics
.d_soiFoundUnsat
);
155 if(verbose
){ Message() << "fc found unsat";}
156 }else if(d_errorSet
.errorEmpty()){
157 ++(d_statistics
.d_soiFoundSat
);
158 if(verbose
){ Message() << "fc found model"; }
160 ++(d_statistics
.d_soiMissed
);
161 if(verbose
){ Message() << "fc missed"; }
165 Message() << "(" << instance
<< ") pivots " << d_pivots
<< endl
;
168 Assert(!d_errorSet
.moreSignals());
169 if(result
== Result::SAT_UNKNOWN
&& d_errorSet
.errorEmpty()){
170 result
= Result::SAT
;
173 // ensure that the conflict variable is still in the queue.
174 d_conflictVariables
.purge();
176 Debug("soi::findModel") << "end findModel() " << instance
<< " " << result
<< endl
;
178 Assert(d_conflictVariables
.empty());
183 void SumOfInfeasibilitiesSPD::logPivot(WitnessImprovement w
){
184 if(d_pivotBudget
> 0) {
187 Assert(w
!= AntiProductive
);
189 if(w
== d_prevWitnessImprovement
){
190 ++d_witnessImprovementInARow
;
191 if(d_witnessImprovementInARow
== 0){
192 --d_witnessImprovementInARow
;
195 if(w
!= BlandsDegenerate
){
196 d_witnessImprovementInARow
= 1;
198 d_prevWitnessImprovement
= w
;
200 if(strongImprovement(w
)){
201 d_leavingCountSinceImprovement
.purge();
204 Debug("logPivot") << "logPivot " << d_prevWitnessImprovement
<< " " << d_witnessImprovementInARow
<< endl
;
207 uint32_t SumOfInfeasibilitiesSPD::degeneratePivotsInARow() const {
208 switch(d_prevWitnessImprovement
){
213 case HeuristicDegenerate
:
214 case BlandsDegenerate
:
215 return d_witnessImprovementInARow
;
216 // Degenerate is unreachable for its own reasons
226 void SumOfInfeasibilitiesSPD::adjustFocusAndError(const UpdateInfo
& up
, const AVIntPairVec
& focusChanges
){
227 uint32_t newErrorSize
= d_errorSet
.errorSize();
228 adjustInfeasFunc(d_statistics
.d_soiFocusConstructionTimer
, d_soiVar
, focusChanges
);
229 d_errorSize
= newErrorSize
;
233 UpdateInfo
SumOfInfeasibilitiesSPD::selectUpdate(LinearEqualityModule::UpdatePreferenceFunction upf
, LinearEqualityModule::VarPreferenceFunction bpf
) {
236 static int instance
= 0 ;
239 Debug("soi::selectPrimalUpdate")
240 << "selectPrimalUpdate " << instance
<< endl
241 << d_soiVar
<< " " << d_tableau
.basicRowLength(d_soiVar
)
242 << " " << d_linEq
.debugBasicAtBoundCount(d_soiVar
) << endl
;
244 typedef std::vector
<Cand
> CandVector
;
245 CandVector candidates
;
247 for(Tableau::RowIterator ri
= d_tableau
.basicRowIterator(d_soiVar
); !ri
.atEnd(); ++ri
){
248 const Tableau::Entry
& e
= *ri
;
249 ArithVar curr
= e
.getColVar();
250 if(curr
== d_soiVar
){ continue; }
252 int sgn
= e
.getCoefficient().sgn();
254 (sgn
> 0 && d_variables
.cmpAssignmentUpperBound(curr
) < 0) ||
255 (sgn
< 0 && d_variables
.cmpAssignmentLowerBound(curr
) > 0);
257 Debug("soi::selectPrimalUpdate")
258 << "storing " << d_soiVar
261 << " " << e
.getCoefficient()
262 << " " << sgn
<< endl
;
265 candidates
.push_back(Cand(curr
, 0, sgn
, &e
.getCoefficient()));
269 CompPenaltyColLength
colCmp(&d_linEq
);
270 CandVector::iterator i
= candidates
.begin();
271 CandVector::iterator end
= candidates
.end();
272 std::make_heap(i
, end
, colCmp
);
274 // For the first 3 pivots take the best
275 // After that, once an improvement is found on look at a
276 // small number of pivots after finding an improvement
277 // the longer the search to more willing we are to look at more candidates
278 int maxCandidatesAfterImprove
=
279 (d_pivots
<= 2) ? std::numeric_limits
<int>::max() : d_pivots
/5;
281 int candidatesAfterFocusImprove
= 0;
282 while(i
!= end
&& candidatesAfterFocusImprove
<= maxCandidatesAfterImprove
){
283 std::pop_heap(i
, end
, colCmp
);
286 ArithVar curr
= cand
.d_nb
;
287 const Rational
& coeff
= *cand
.d_coeff
;
289 LinearEqualityModule::UpdatePreferenceFunction leavingPrefFunc
= selectLeavingFunction(curr
);
290 UpdateInfo currProposal
= d_linEq
.speculativeUpdate(curr
, coeff
, leavingPrefFunc
);
292 Debug("soi::selectPrimalUpdate")
293 << "selected " << selected
<< endl
294 << "currProp " << currProposal
<< endl
295 << "coeff " << coeff
<< endl
;
297 Assert(!currProposal
.uninitialized());
299 if(candidatesAfterFocusImprove
> 0){
300 candidatesAfterFocusImprove
++;
303 if(selected
.uninitialized() || (d_linEq
.*upf
)(selected
, currProposal
)){
304 selected
= currProposal
;
305 WitnessImprovement w
= selected
.getWitness(false);
306 Debug("soi::selectPrimalUpdate") << "selected " << w
<< endl
;
307 //setPenalty(curr, w);
311 case ConflictFound
: exitEarly
= true; break;
313 candidatesAfterFocusImprove
= 1;
317 exitEarly
= false; break;
319 if(exitEarly
){ break; }
322 Debug("soi::selectPrimalUpdate") << "dropped "<< endl
;
329 bool debugCheckWitness(const UpdateInfo
& inf
, WitnessImprovement w
, bool useBlands
){
330 if(inf
.getWitness(useBlands
) == w
){
332 case ConflictFound
: return inf
.foundConflict();
333 case ErrorDropped
: return inf
.errorsChange() < 0;
334 case FocusImproved
: return inf
.focusDirection() > 0;
335 case FocusShrank
: return false; // This is not a valid output
336 case Degenerate
: return false; // This is not a valid output
337 case BlandsDegenerate
: return useBlands
;
338 case HeuristicDegenerate
: return !useBlands
;
339 case AntiProductive
: return false;
346 void SumOfInfeasibilitiesSPD::debugPrintSignal(ArithVar updated
) const{
347 Debug("updateAndSignal") << "updated basic " << updated
;
348 Debug("updateAndSignal") << " length " << d_tableau
.basicRowLength(updated
);
349 Debug("updateAndSignal") << " consistent " << d_variables
.assignmentIsConsistent(updated
);
350 int dir
= !d_variables
.assignmentIsConsistent(updated
) ?
351 d_errorSet
.getSgn(updated
) : 0;
352 Debug("updateAndSignal") << " dir " << dir
;
353 Debug("updateAndSignal") << " debugBasicAtBoundCount " << d_linEq
.debugBasicAtBoundCount(updated
) << endl
;
357 void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo
& selected
, WitnessImprovement w
){
358 ArithVar nonbasic
= selected
.nonbasic();
360 static bool verbose
= false;
362 Debug("updateAndSignal") << "updateAndSignal " << selected
<< endl
;
366 d_errorSet
.debugPrint(ss
);
367 if(selected
.describesPivot()){
368 ArithVar leaving
= selected
.leaving();
369 ss
<< "leaving " << leaving
370 << " " << d_tableau
.basicRowLength(leaving
)
371 << " " << d_linEq
.debugBasicAtBoundCount(leaving
)
374 if(degenerate(w
) && selected
.describesPivot()){
375 ArithVar leaving
= selected
.leaving();
377 << "degenerate " << leaving
378 << ", atBounds " << d_linEq
.basicsAtBounds(selected
)
379 << ", len " << d_tableau
.basicRowLength(leaving
)
380 << ", bc " << d_linEq
.debugBasicAtBoundCount(leaving
)
385 if(selected
.describesPivot()){
386 Constraint limiting
= selected
.limiting();
387 ArithVar basic
= limiting
->getVariable();
388 Assert(d_linEq
.basicIsTracked(basic
));
389 d_linEq
.pivotAndUpdate(basic
, nonbasic
, limiting
->getValue());
391 Assert(!selected
.unbounded() || selected
.errorsChange() < 0);
393 DeltaRational newAssignment
=
394 d_variables
.getAssignment(nonbasic
) + selected
.nonbasicDelta();
396 d_linEq
.updateTracked(nonbasic
, newAssignment
);
400 increaseLeavingCount(nonbasic
);
402 vector
< pair
<ArithVar
, int> > focusChanges
;
403 while(d_errorSet
.moreSignals()){
404 ArithVar updated
= d_errorSet
.topSignal();
405 int prevFocusSgn
= d_errorSet
.popSignal();
407 if(d_tableau
.isBasic(updated
)){
408 Assert(!d_variables
.assignmentIsConsistent(updated
) == d_errorSet
.inError(updated
));
409 if(Debug
.isOn("updateAndSignal")){debugPrintSignal(updated
);}
410 if(!d_variables
.assignmentIsConsistent(updated
)){
411 if(checkBasicForConflict(updated
)){
412 reportConflict(updated
);
413 //Assert(debugUpdatedBasic(selected, updated));
417 Debug("updateAndSignal") << "updated nonbasic " << updated
<< endl
;
419 int currFocusSgn
= d_errorSet
.focusSgn(updated
);
420 if(currFocusSgn
!= prevFocusSgn
){
421 int change
= currFocusSgn
- prevFocusSgn
;
422 focusChanges
.push_back(make_pair(updated
, change
));
427 Message() << "conflict variable " << selected
<< endl
;
428 Message() << ss
.str();
430 if(Debug
.isOn("error")){ d_errorSet
.debugPrint(Debug("error")); }
432 //Assert(debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize()));
434 adjustFocusAndError(selected
, focusChanges
);
437 void SumOfInfeasibilitiesSPD::qeAddRange(uint32_t begin
, uint32_t end
){
438 Assert(!d_qeInSoi
.empty());
439 for(uint32_t i
= begin
; i
!= end
; ++i
){
440 ArithVar v
= d_qeConflict
[i
];
441 addToInfeasFunc(d_statistics
.d_soiConflictMinimization
, d_soiVar
, v
);
446 void SumOfInfeasibilitiesSPD::qeRemoveRange(uint32_t begin
, uint32_t end
){
447 for(uint32_t i
= begin
; i
!= end
; ++i
){
448 ArithVar v
= d_qeConflict
[i
];
449 removeFromInfeasFunc(d_statistics
.d_soiConflictMinimization
, d_soiVar
, v
);
452 Assert(!d_qeInSoi
.empty());
455 void SumOfInfeasibilitiesSPD::qeSwapRange(uint32_t N
, uint32_t r
, uint32_t s
){
456 for(uint32_t i
= 0; i
< N
; ++i
){
457 std::swap(d_qeConflict
[r
+i
], d_qeConflict
[s
+i
]);
464 * - A single element X@i with the name X at the position i
465 * - A sequence of indices X@[i,j) with the name X and the elements between i [inclusive] and j exclusive
466 * - A concatenation of regions R1 and R2, R1;R2
468 * Given the fixed assumptions C @ [0,cEnd) and a set of candidate minimizations U@[cEnd, uEnd)
469 * s.t. C \cup U is known to be in conflict ([0,uEnd) has a conflict), find a minimal
470 * subset of U, Delta, s.t. C \cup Delta is in conflict.
473 * [0, uEnd) is a set and is in conflict.
474 * uEnd <= assumptions.size()
475 * [0, cEnd) is in d_inSoi.
477 * Invariants: [0,cEnd) is never modified
480 * [0, cEnd); [cEnd, deltaEnd) is in conflict
481 * [0, deltaEnd) is a set
482 * [0, deltaEnd) is in d_inSoi
484 uint32_t SumOfInfeasibilitiesSPD::quickExplainRec(uint32_t cEnd
, uint32_t uEnd
){
485 Assert(cEnd
<= uEnd
);
486 Assert(d_qeInUAndNotInSoi
.empty());
487 Assert(d_qeGreedyOrder
.empty());
489 const Tableau::Entry
* spoiler
= NULL
;
491 if(d_soiVar
!= ARITHVAR_SENTINEL
&& d_linEq
.selectSlackEntry(d_soiVar
, false) == NULL
){
492 // already in conflict
498 // Phase 1 : Construct the conflict greedily
500 for(uint32_t i
= cEnd
; i
< uEnd
; ++i
){
501 d_qeInUAndNotInSoi
.add(d_qeConflict
[i
]);
503 if(d_soiVar
== ARITHVAR_SENTINEL
){ // special case for d_soiVar being empty
504 ArithVar first
= d_qeConflict
[cEnd
];
505 d_soiVar
= constructInfeasiblityFunction(d_statistics
.d_soiConflictMinimization
, first
);
506 d_qeInSoi
.add(first
);
507 d_qeInUAndNotInSoi
.remove(first
);
508 d_qeGreedyOrder
.push_back(first
);
510 while((spoiler
= d_linEq
.selectSlackEntry(d_soiVar
, false)) != NULL
){
511 Assert(!d_qeInUAndNotInSoi
.empty());
513 ArithVar nb
= spoiler
->getColVar();
514 int oppositeSgn
= -(spoiler
->getCoefficient().sgn());
515 Assert(oppositeSgn
!= 0);
517 ArithVar basicWithOp
= find_basic_in_sgns(d_qeSgns
, nb
, oppositeSgn
, d_qeInUAndNotInSoi
, true);
518 Assert(basicWithOp
!= ARITHVAR_SENTINEL
);
520 addToInfeasFunc(d_statistics
.d_soiConflictMinimization
, d_soiVar
, basicWithOp
);
521 d_qeInSoi
.add(basicWithOp
);
522 d_qeInUAndNotInSoi
.remove(basicWithOp
);
523 d_qeGreedyOrder
.push_back(basicWithOp
);
525 Assert(spoiler
== NULL
);
528 uint32_t newEnd
= cEnd
+ d_qeGreedyOrder
.size();
529 std::copy(d_qeGreedyOrder
.begin(), d_qeGreedyOrder
.end(), d_qeConflict
.begin()+cEnd
);
531 d_qeInUAndNotInSoi
.purge();
532 d_qeGreedyOrder
.clear();
534 // Phase 2 : Recursively determine the minimal set of rows
536 uint32_t xPos
= cEnd
;
537 std::swap(d_qeGreedyOrder
[xPos
], d_qeGreedyOrder
[newEnd
- 1]);
538 uint32_t uBegin
= xPos
+ 1;
539 uint32_t split
= (newEnd
- uBegin
)/2 + uBegin
;
541 //assumptions : C @ [0, cEnd); X @ xPos; U1 @ [u1Begin, split); U2 @ [split, newEnd)
542 // [0, newEnd) == d_inSoi
545 if(split
== newEnd
){ // U2 is empty
548 // Remove U2 from Soi
549 qeRemoveRange(split
, newEnd
);
550 // [0, split) == d_inSoi
552 // pre assumptions: C + X + U1 @ [0,split); U2 [split, newEnd)
553 compactU2
= quickExplainRec(split
, newEnd
);
555 // assumptions: C + X + U1 @ [0, split); delta2 @ [split - compactU2)
556 // d_inSoi = [0, compactU2)
558 uint32_t deltaSize
= compactU2
- split
;
559 qeSwapRange(deltaSize
, uBegin
, split
);
560 uint32_t d2End
= uBegin
+deltaSize
;
561 // assumptions : C @ [0, cEnd); X @ xPos; delta2 @ [uBegin, d2End); U1 @ [d2End, compactU2)
562 // d_inSoi == [0, compactU2)
565 if(d2End
== compactU2
){ // U1 is empty
568 qeRemoveRange(d2End
, compactU2
);
570 //pre assumptions : C + X + delta2 @ [0, d2End); U1 @ [d2End, compactU2);
571 d1End
= quickExplainRec(d2End
, compactU2
);
573 // assumptions : C + X + delta2 @ [0, d2End); delta1 @ [d2End, d1End);
574 // d_inSoi = [0, d1End)
577 // d_inSoi == [0, d1End), C @ [0, cEnd); X + delta2 + delta 1 @ [xPos, d1End);
579 Assert(d_qeInUAndNotInSoi
.empty());
580 Assert(d_qeGreedyOrder
.empty());
584 void SumOfInfeasibilitiesSPD::quickExplain(){
585 Assert(d_qeInSoi
.empty());
586 Assert(d_qeInUAndNotInSoi
.empty());
587 Assert(d_qeGreedyOrder
.empty());
588 Assert(d_soiVar
== ARITHVAR_SENTINEL
);
589 Assert(d_qeSgns
.empty());
591 d_qeConflict
.clear();
592 d_errorSet
.pushFocusInto(d_qeConflict
);
594 //cout << d_qeConflict.size() << " ";
595 uint32_t size
= d_qeConflict
.size();
598 for(ErrorSet::focus_iterator iter
= d_errorSet
.focusBegin(), end
= d_errorSet
.focusEnd(); iter
!= end
; ++iter
){
600 addRowSgns(d_qeSgns
, e
, d_errorSet
.getSgn(e
));
602 uint32_t end
= quickExplainRec(0u, size
);
603 Assert(end
<= d_qeConflict
.size());
604 Assert(d_soiVar
!= ARITHVAR_SENTINEL
);
605 Assert(!d_qeInSoi
.empty());
607 d_qeConflict
.resize(end
);
608 tearDownInfeasiblityFunction(d_statistics
.d_soiConflictMinimization
, d_soiVar
);
609 d_soiVar
= ARITHVAR_SENTINEL
;
614 //cout << d_qeConflict.size() << endl;
616 Assert(d_qeInSoi
.empty());
617 Assert(d_qeInUAndNotInSoi
.empty());
618 Assert(d_qeGreedyOrder
.empty());
619 Assert(d_soiVar
== ARITHVAR_SENTINEL
);
620 Assert(d_qeSgns
.empty());
623 unsigned SumOfInfeasibilitiesSPD::trySet(const ArithVarVec
& set
){
624 Assert(d_soiVar
== ARITHVAR_SENTINEL
);
625 bool success
= false;
627 d_soiVar
= constructInfeasiblityFunction(d_statistics
.d_soiConflictMinimization
, set
);
628 success
= d_linEq
.selectSlackEntry(d_soiVar
, false) == NULL
;
630 tearDownInfeasiblityFunction(d_statistics
.d_soiConflictMinimization
, d_soiVar
);
631 d_soiVar
= ARITHVAR_SENTINEL
;
633 return success
? set
.size() : std::numeric_limits
<int>::max();
636 std::vector
< ArithVarVec
> SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
637 std::vector
< ArithVarVec
> subsets
;
638 Assert(d_soiVar
== ARITHVAR_SENTINEL
);
640 if(d_errorSize
<= 2){
642 d_errorSet
.pushFocusInto(inError
);
643 subsets
.push_back(inError
);
646 Assert(d_errorSize
> 2);
648 //sgns_table< <nonbasic,sgn>, [basics] >;
649 // Phase 0: Construct the sgns table
651 DenseSet hasParticipated
; //Has participated in a conflict
652 for(ErrorSet::focus_iterator iter
= d_errorSet
.focusBegin(), end
= d_errorSet
.focusEnd(); iter
!= end
; ++iter
){
654 addRowSgns(sgns
, e
, d_errorSet
.getSgn(e
));
656 //cout << "basic error var: " << e << endl;
657 //d_tableau.debugPrintIsBasic(e);
658 //d_tableau.printBasicRow(e, cout);
661 // Phase 1: Try to find at least 1 pair for every element
665 for(ErrorSet::focus_iterator iter
= d_errorSet
.focusBegin(), end
= d_errorSet
.focusEnd(); iter
!= end
; ++iter
){
669 int errSgn
= d_errorSet
.getSgn(e
);
670 bool decreasing
= errSgn
< 0;
671 const Tableau::Entry
* spoiler
= d_linEq
.selectSlackEntry(e
, decreasing
);
672 Assert(spoiler
!= NULL
);
673 ArithVar nb
= spoiler
->getColVar();
674 int oppositeSgn
= -(errSgn
* (spoiler
->getCoefficient().sgn()));
676 sgn_table::const_iterator opposites
= find_sgns(sgns
, nb
, oppositeSgn
);
677 Assert(opposites
!= sgns
.end());
679 const ArithVarVec
& choices
= (*opposites
).second
;
680 for(ArithVarVec::const_iterator j
= choices
.begin(), jend
= choices
.end(); j
!= jend
; ++j
){
682 if(b
< e
){ continue; }
685 if(trySet(tmp
) == 2){
686 //cout << "found a pair" << endl;
687 hasParticipated
.softAdd(b
);
688 hasParticipated
.softAdd(e
);
689 subsets
.push_back(tmp
);
690 ++(d_statistics
.d_soiConflicts
);
691 ++(d_statistics
.d_hasToBeMinimal
);
697 // Phase 2: If there is a variable that has not participated attempt to start a conflict
698 ArithVarVec possibleStarts
; //List of elements that can be tried for starts.
699 d_errorSet
.pushFocusInto(possibleStarts
);
700 while(!possibleStarts
.empty()){
701 Assert(d_soiVar
== ARITHVAR_SENTINEL
);
703 ArithVar v
= possibleStarts
.back();
704 possibleStarts
.pop_back();
705 if(hasParticipated
.isMember(v
)){ continue; }
707 Assert(d_soiVar
== ARITHVAR_SENTINEL
);
708 //d_soiVar's row = \sumofinfeasibilites underConstruction
709 ArithVarVec underConstruction
;
710 underConstruction
.push_back(v
);
711 d_soiVar
= constructInfeasiblityFunction(d_statistics
.d_soiConflictMinimization
, v
);
713 //cout << "trying " << v << endl;
715 const Tableau::Entry
* spoiler
= NULL
;
716 while( (spoiler
= d_linEq
.selectSlackEntry(d_soiVar
, false)) != NULL
){
717 ArithVar nb
= spoiler
->getColVar();
718 int oppositeSgn
= -(spoiler
->getCoefficient().sgn());
719 Assert(oppositeSgn
!= 0);
721 //cout << "looking for " << nb << " " << oppositeSgn << endl;
723 ArithVar basicWithOp
= find_basic_in_sgns(sgns
, nb
, oppositeSgn
, hasParticipated
, false);
725 if(basicWithOp
== ARITHVAR_SENTINEL
){
726 //cout << "search did not work for " << nb << endl;
727 // greedy construction has failed
730 //cout << "found " << basicWithOp << endl;
732 addToInfeasFunc(d_statistics
.d_soiConflictMinimization
, d_soiVar
, basicWithOp
);
733 hasParticipated
.softAdd(basicWithOp
);
734 underConstruction
.push_back(basicWithOp
);
738 //cout << "success" << endl;
739 //then underConstruction contains a conflicting subset
740 subsets
.push_back(underConstruction
);
741 ++d_statistics
.d_soiConflicts
;
742 if(underConstruction
.size() == 3){
743 ++d_statistics
.d_hasToBeMinimal
;
745 ++d_statistics
.d_maybeNotMinimal
;
748 //cout << "failure" << endl;
750 tearDownInfeasiblityFunction(d_statistics
.d_soiConflictMinimization
, d_soiVar
);
751 d_soiVar
= ARITHVAR_SENTINEL
;
752 // if(false && spoiler == NULL){
754 // int smallest = tryAllSubsets(underConstruction, 0, tmp);
755 // cout << underConstruction.size() << " " << smallest << endl;
756 // Assert(smallest >= underConstruction.size());
757 // if(smallest < underConstruction.size()){
764 Assert(d_soiVar
== ARITHVAR_SENTINEL
);
768 Node
SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec
& subset
){
769 Assert(d_soiVar
== ARITHVAR_SENTINEL
);
770 d_soiVar
= constructInfeasiblityFunction(d_statistics
.d_soiConflictMinimization
, subset
);
772 NodeBuilder
<> conflict(kind::AND
);
773 for(ArithVarVec::const_iterator iter
= subset
.begin(), end
= subset
.end(); iter
!= end
; ++iter
){
775 Constraint violated
= d_errorSet
.getViolated(e
);
776 //cout << "basic error var: " << violated << endl;
777 violated
->explainForConflict(conflict
);
779 //d_tableau.debugPrintIsBasic(e);
780 //d_tableau.printBasicRow(e, cout);
782 for(Tableau::RowIterator i
= d_tableau
.basicRowIterator(d_soiVar
); !i
.atEnd(); ++i
){
783 const Tableau::Entry
& entry
= *i
;
784 ArithVar v
= entry
.getColVar();
785 if(v
== d_soiVar
){ continue; }
786 const Rational
& coeff
= entry
.getCoefficient();
788 Constraint c
= (coeff
.sgn() > 0) ?
789 d_variables
.getUpperBoundConstraint(v
) :
790 d_variables
.getLowerBoundConstraint(v
);
792 //cout << "nb : " << c << endl;
793 c
->explainForConflict(conflict
);
796 Node conf
= conflict
;
797 tearDownInfeasiblityFunction(d_statistics
.d_soiConflictMinimization
, d_soiVar
);
798 d_soiVar
= ARITHVAR_SENTINEL
;
803 WitnessImprovement
SumOfInfeasibilitiesSPD::SOIConflict(){
804 static int instance
= 0;
806 //cout << "SOI conflict " << instance << ": |E| = " << d_errorSize << endl;
807 //d_errorSet.debugPrint(cout);
810 tearDownInfeasiblityFunction(d_statistics
.d_soiConflictMinimization
, d_soiVar
);
811 d_soiVar
= ARITHVAR_SENTINEL
;
813 if(options::soiQuickExplain()){
815 Node conflict
= generateSOIConflict(d_qeConflict
);
816 //cout << conflict << endl;
817 d_conflictChannel(conflict
);
820 vector
<ArithVarVec
> subsets
= greedyConflictSubsets();
821 Assert( d_soiVar
== ARITHVAR_SENTINEL
);
823 Assert(!subsets
.empty());
824 for(vector
<ArithVarVec
>::const_iterator i
= subsets
.begin(), end
= subsets
.end(); i
!= end
; ++i
){
825 const ArithVarVec
& subset
= *i
;
826 Node conflict
= generateSOIConflict(subset
);
827 //cout << conflict << endl;
829 //reportConflict(conf); do not do this. We need a custom explanations!
830 d_conflictChannel(conflict
);
833 Assert( d_soiVar
== ARITHVAR_SENTINEL
);
834 d_soiVar
= constructInfeasiblityFunction(d_statistics
.d_soiConflictMinimization
);
836 //reportConflict(conf); do not do this. We need a custom explanations!
837 d_conflictVariables
.add(d_soiVar
);
839 //cout << "SOI conflict " << instance << "end" << endl;
840 return ConflictFound
;
843 WitnessImprovement
SumOfInfeasibilitiesSPD::soiRound() {
844 Assert(d_soiVar
!= ARITHVAR_SENTINEL
);
846 bool useBlands
= degeneratePivotsInARow() >= s_maxDegeneratePivotsBeforeBlandsOnLeaving
;
847 LinearEqualityModule::UpdatePreferenceFunction upf
;
849 upf
= &LinearEqualityModule::preferWitness
<false>;
851 upf
= &LinearEqualityModule::preferWitness
<true>;
854 LinearEqualityModule::VarPreferenceFunction bpf
= useBlands
?
855 &LinearEqualityModule::minVarOrder
:
856 &LinearEqualityModule::minRowLength
;
857 bpf
= &LinearEqualityModule::minVarOrder
;
859 UpdateInfo selected
= selectUpdate(upf
, bpf
);
861 if(selected
.uninitialized()){
862 Debug("selectFocusImproving") << "SOI is optimum, but we don't have sat/conflict yet" << endl
;
863 return SOIConflict();
865 Assert(!selected
.uninitialized());
866 WitnessImprovement w
= selected
.getWitness(false);
867 Assert(debugCheckWitness(selected
, w
, false));
869 updateAndSignal(selected
, w
);
875 bool SumOfInfeasibilitiesSPD::debugSOI(WitnessImprovement w
, ostream
& out
, int instance
) const{
876 //#warning "Redo SOI"
878 // out << "DLV("<<instance<<") ";
880 // case ConflictFound:
881 // out << "found conflict" << endl;
882 // return !d_conflictVariables.empty();
883 // case ErrorDropped:
885 // // out << "dropped " << prevErrorSize - d_errorSize << endl;
886 // // return d_errorSize < prevErrorSize;
887 // case FocusImproved:
888 // out << "focus improved"<< endl;
889 // return d_errorSize == prevErrorSize;
893 // case BlandsDegenerate:
894 // out << "bland degenerate"<< endl;
896 // case HeuristicDegenerate:
897 // out << "heuristic degenerate"<< endl;
899 // case AntiProductive:
906 Result::Sat
SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){
907 static int instance
= 0;
908 static bool verbose
= false;
910 TimerStat::CodeTimer
codeTimer(d_statistics
.d_soiTimer
);
912 Assert(d_sgnDisagreements
.empty());
913 Assert(d_pivotBudget
!= 0);
914 Assert(d_errorSize
== d_errorSet
.errorSize());
915 Assert(d_errorSize
> 0);
916 Assert(d_conflictVariables
.empty());
917 Assert(d_soiVar
== ARITHVAR_SENTINEL
);
921 d_soiVar
= constructInfeasiblityFunction(d_statistics
.d_soiFocusConstructionTimer
);
924 while(d_pivotBudget
!= 0 && d_errorSize
> 0 && d_conflictVariables
.empty()){
926 Debug("dualLike") << "dualLike " << instance
<< endl
;
928 Assert(d_errorSet
.noSignals());
929 // Possible outcomes:
931 // - budget was exhausted
933 Debug("dualLike") << "selectFocusImproving " << endl
;
934 WitnessImprovement w
= soiRound();
936 Assert(d_errorSize
== d_errorSet
.errorSize());
939 debugSOI(w
, Message(), instance
);
941 Assert(debugSOI(w
, Debug("dualLike"), instance
));
945 if(d_soiVar
!= ARITHVAR_SENTINEL
){
946 tearDownInfeasiblityFunction(d_statistics
.d_soiFocusConstructionTimer
, d_soiVar
);
947 d_soiVar
= ARITHVAR_SENTINEL
;
950 Assert(d_soiVar
== ARITHVAR_SENTINEL
);
951 if(!d_conflictVariables
.empty()){
952 return Result::UNSAT
;
953 }else if(d_errorSet
.errorEmpty()){
954 Assert(d_errorSet
.noSignals());
957 Assert(d_pivotBudget
== 0);
958 return Result::SAT_UNKNOWN
;
962 }/* CVC4::theory::arith namespace */
963 }/* CVC4::theory namespace */
964 }/* CVC4 namespace */