Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * This is an implementation of the Simplex Module for the Simplex for
11 : : * DPLL(T) decision procedure.
12 : : */
13 : : #include "theory/arith/linear/soi_simplex.h"
14 : :
15 : : #include <algorithm>
16 : :
17 : : #include "base/output.h"
18 : : #include "options/arith_options.h"
19 : : #include "theory/arith/linear/constraint.h"
20 : : #include "theory/arith/linear/error_set.h"
21 : : #include "theory/arith/linear/tableau.h"
22 : : #include "util/statistics_registry.h"
23 : : #include "util/statistics_stats.h"
24 : :
25 : : using namespace std;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : : namespace arith::linear {
30 : :
31 : 28777 : SumOfInfeasibilitiesSPD::SumOfInfeasibilitiesSPD(Env& env,
32 : : LinearEqualityModule& linEq,
33 : : ErrorSet& errors,
34 : : RaiseConflict conflictChannel,
35 : 28777 : TempVarMalloc tvmalloc)
36 : : : SimplexDecisionProcedure(env, linEq, errors, conflictChannel, tvmalloc),
37 : 28777 : d_soiVar(ARITHVAR_SENTINEL),
38 : 28777 : d_pivotBudget(0),
39 : 28777 : d_prevWitnessImprovement(AntiProductive),
40 : 28777 : d_witnessImprovementInARow(0),
41 : 28777 : d_sgnDisagreements(),
42 : 57554 : d_statistics(statisticsRegistry(), "theory::arith::SOI", d_pivots)
43 : : {
44 : 28777 : }
45 : :
46 : 28777 : SumOfInfeasibilitiesSPD::Statistics::Statistics(StatisticsRegistry& sr,
47 : : const std::string& name,
48 : 28777 : uint32_t& pivots)
49 : 28777 : : d_initialSignalsTime(sr.registerTimer(name + "initialProcessTime")),
50 : 28777 : d_initialConflicts(sr.registerInt(name + "UpdateConflicts")),
51 : 28777 : d_soiFoundUnsat(sr.registerInt(name + "FoundUnsat")),
52 : 28777 : d_soiFoundSat(sr.registerInt(name + "FoundSat")),
53 : 28777 : d_soiMissed(sr.registerInt(name + "Missed")),
54 : 28777 : d_soiConflicts(sr.registerInt(name + "ConfMin::num")),
55 : 28777 : d_hasToBeMinimal(sr.registerInt(name + "HasToBeMin")),
56 : 28777 : d_maybeNotMinimal(sr.registerInt(name + "MaybeNotMin")),
57 : 28777 : d_soiTimer(sr.registerTimer(name + "Time")),
58 : 28777 : d_soiFocusConstructionTimer(sr.registerTimer(name + "Construction")),
59 : : d_soiConflictMinimization(
60 : 28777 : sr.registerTimer(name + "Conflict::Minimization")),
61 : 28777 : d_selectUpdateForSOI(sr.registerTimer(name + "selectSOI")),
62 : 28777 : d_finalCheckPivotCounter(
63 : 57554 : sr.registerReference<uint32_t>(name + "lastPivots", pivots))
64 : : {
65 : 28777 : }
66 : :
67 : 16933 : Result::Status SumOfInfeasibilitiesSPD::findModel(bool exactResult)
68 : : {
69 [ - + ][ - + ]: 16933 : Assert(d_conflictVariables.empty());
[ - - ]
70 [ - + ][ - + ]: 16933 : Assert(d_sgnDisagreements.empty());
[ - - ]
71 : :
72 : 16933 : d_pivots = 0;
73 : :
74 [ + + ][ + + ]: 16933 : if (d_errorSet.errorEmpty() && !d_errorSet.moreSignals())
[ + + ]
75 : : {
76 [ + - ]: 3465 : Trace("soi::findModel") << "soiFindModel() trivial" << endl;
77 [ - + ][ - + ]: 3465 : Assert(d_conflictVariables.empty());
[ - - ]
78 : 3465 : return Result::SAT;
79 : : }
80 : :
81 : : // We need to reduce this because of
82 : 13468 : d_errorSet.reduceToSignals();
83 : :
84 : : // We must start tracking NOW
85 : 13468 : d_errorSet.setSelectionRule(options::ErrorSelectionRule::SUM_METRIC);
86 : :
87 [ + + ]: 13468 : if (initialProcessSignals())
88 : : {
89 : 357 : d_conflictVariables.purge();
90 [ + - ]: 357 : Trace("soi::findModel") << "fcFindModel() early conflict" << endl;
91 [ - + ][ - + ]: 357 : Assert(d_conflictVariables.empty());
[ - - ]
92 : 357 : return Result::UNSAT;
93 : : }
94 [ + + ]: 13111 : else if (d_errorSet.errorEmpty())
95 : : {
96 [ + - ]: 9377 : Trace("soi::findModel") << "fcFindModel() fixed itself" << endl;
97 [ - + ][ - + ]: 9377 : Assert(!d_errorSet.moreSignals());
[ - - ]
98 [ - + ][ - + ]: 9377 : Assert(d_conflictVariables.empty());
[ - - ]
99 : 9377 : return Result::SAT;
100 : : }
101 : :
102 [ + - ]: 3734 : Trace("soi::findModel") << "fcFindModel() start non-trivial" << endl;
103 : :
104 : 3734 : exactResult |= d_varOrderPivotLimit < 0;
105 : :
106 : 3734 : d_prevWitnessImprovement = HeuristicDegenerate;
107 : 3734 : d_witnessImprovementInARow = 0;
108 : :
109 : 3734 : Result::Status result = Result::UNKNOWN;
110 : :
111 [ + - ]: 3734 : if (result == Result::UNKNOWN)
112 : : {
113 [ - + ]: 3734 : if (exactResult)
114 : : {
115 : 0 : d_pivotBudget = -1;
116 : : }
117 : : else
118 : : {
119 : 3734 : d_pivotBudget = d_varOrderPivotLimit;
120 : : }
121 : :
122 : 3734 : result = sumOfInfeasibilities();
123 : :
124 [ + + ]: 3734 : if (result == Result::UNSAT)
125 : : {
126 : 983 : ++(d_statistics.d_soiFoundUnsat);
127 : : }
128 [ + - ]: 2751 : else if (d_errorSet.errorEmpty())
129 : : {
130 : 2751 : ++(d_statistics.d_soiFoundSat);
131 : : }
132 : : else
133 : : {
134 : 0 : ++(d_statistics.d_soiMissed);
135 : : }
136 : : }
137 : :
138 [ - + ][ - + ]: 3734 : Assert(!d_errorSet.moreSignals());
[ - - ]
139 [ - + ][ - - ]: 3734 : if (result == Result::UNKNOWN && d_errorSet.errorEmpty())
[ - + ]
140 : : {
141 : 0 : result = Result::SAT;
142 : : }
143 : :
144 : : // ensure that the conflict variable is still in the queue.
145 : 3734 : d_conflictVariables.purge();
146 : :
147 [ + - ]: 3734 : Trace("soi::findModel") << "end findModel() " << result << endl;
148 : :
149 [ - + ][ - + ]: 3734 : Assert(d_conflictVariables.empty());
[ - - ]
150 : 3734 : return result;
151 : : }
152 : :
153 : 7279 : void SumOfInfeasibilitiesSPD::logPivot(WitnessImprovement w)
154 : : {
155 [ + - ]: 7279 : if (d_pivotBudget > 0)
156 : : {
157 : 7279 : --d_pivotBudget;
158 : : }
159 [ - + ][ - + ]: 7279 : Assert(w != AntiProductive);
[ - - ]
160 : :
161 [ + + ]: 7279 : if (w == d_prevWitnessImprovement)
162 : : {
163 : 2599 : ++d_witnessImprovementInARow;
164 [ - + ]: 2599 : if (d_witnessImprovementInARow == 0)
165 : : {
166 : 0 : --d_witnessImprovementInARow;
167 : : }
168 : : }
169 : : else
170 : : {
171 [ + - ]: 4680 : if (w != BlandsDegenerate)
172 : : {
173 : 4680 : d_witnessImprovementInARow = 1;
174 : : }
175 : 4680 : d_prevWitnessImprovement = w;
176 : : }
177 [ + + ]: 7279 : if (strongImprovement(w))
178 : : {
179 : 5427 : d_leavingCountSinceImprovement.purge();
180 : : }
181 : :
182 [ + - ]: 14558 : Trace("logPivot") << "logPivot " << d_prevWitnessImprovement << " "
183 : 7279 : << d_witnessImprovementInARow << endl;
184 : 7279 : }
185 : :
186 : 7332 : uint32_t SumOfInfeasibilitiesSPD::degeneratePivotsInARow() const
187 : : {
188 [ + + ][ - - ]: 7332 : switch (d_prevWitnessImprovement)
189 : : {
190 : 2184 : case ConflictFound:
191 : : case ErrorDropped:
192 : 2184 : case FocusImproved: return 0;
193 : 5148 : case HeuristicDegenerate:
194 : 5148 : case BlandsDegenerate: return d_witnessImprovementInARow;
195 : : // Degenerate is unreachable for its own reasons
196 : 0 : case Degenerate:
197 : : case FocusShrank:
198 : 0 : case AntiProductive: Unreachable(); return -1;
199 : : }
200 : 0 : Unreachable();
201 : : }
202 : :
203 : 7279 : void SumOfInfeasibilitiesSPD::adjustFocusAndError(
204 : : const AVIntPairVec& focusChanges)
205 : : {
206 : 7279 : uint32_t newErrorSize = d_errorSet.errorSize();
207 : 7279 : adjustInfeasFunc(
208 : 7279 : d_statistics.d_soiFocusConstructionTimer, d_soiVar, focusChanges);
209 : 7279 : d_errorSize = newErrorSize;
210 : 7279 : }
211 : :
212 : 7332 : UpdateInfo SumOfInfeasibilitiesSPD::selectUpdate(
213 : : LinearEqualityModule::UpdatePreferenceFunction upf)
214 : : {
215 : 7332 : UpdateInfo selected;
216 : :
217 [ + - ]: 14664 : Trace("soi::selectPrimalUpdate")
218 : 0 : << "selectPrimalUpdate " << endl
219 : 0 : << d_soiVar << " " << d_tableau.basicRowLength(d_soiVar) << " "
220 : 7332 : << d_linEq.debugBasicAtBoundCount(d_soiVar) << endl;
221 : :
222 : : typedef std::vector<Cand> CandVector;
223 : 7332 : CandVector candidates;
224 : :
225 : 7332 : for (Tableau::RowIterator ri = d_tableau.basicRowIterator(d_soiVar);
226 [ + + ]: 99574 : !ri.atEnd();
227 : 92242 : ++ri)
228 : : {
229 : 92242 : const Tableau::Entry& e = *ri;
230 : 92242 : ArithVar curr = e.getColVar();
231 [ + + ]: 92242 : if (curr == d_soiVar)
232 : : {
233 : 7332 : continue;
234 : : }
235 : :
236 : 84910 : int sgn = e.getCoefficient().sgn();
237 : : bool candidate =
238 [ + + ]: 43054 : (sgn > 0 && d_variables.cmpAssignmentUpperBound(curr) < 0)
239 [ + + ][ + + ]: 127964 : || (sgn < 0 && d_variables.cmpAssignmentLowerBound(curr) > 0);
[ + + ]
240 : :
241 [ + - ]: 169820 : Trace("soi::selectPrimalUpdate")
242 : 0 : << "storing " << d_soiVar << " " << curr << " " << candidate << " "
243 : 84910 : << e.getCoefficient() << " " << sgn << endl;
244 : :
245 [ + + ]: 84910 : if (candidate)
246 : : {
247 : 21789 : candidates.push_back(Cand(curr, 0, sgn, &e.getCoefficient()));
248 : : }
249 : : }
250 : :
251 : 7332 : CompPenaltyColLength colCmp(&d_linEq, options().arith.havePenalties);
252 : 7332 : CandVector::iterator i = candidates.begin();
253 : 7332 : CandVector::iterator end = candidates.end();
254 : 7332 : std::make_heap(i, end, colCmp);
255 : :
256 : : // For the first 3 pivots take the best
257 : : // After that, once an improvement is found on look at a
258 : : // small number of pivots after finding an improvement
259 : : // the longer the search to more willing we are to look at more candidates
260 : : int maxCandidatesAfterImprove =
261 [ + + ]: 7332 : (d_pivots <= 2) ? std::numeric_limits<int>::max() : d_pivots / 5;
262 : :
263 : 7332 : int candidatesAfterFocusImprove = 0;
264 [ + + ][ + + ]: 28892 : while (i != end && candidatesAfterFocusImprove <= maxCandidatesAfterImprove)
[ + + ]
265 : : {
266 : 21601 : std::pop_heap(i, end, colCmp);
267 : 21601 : --end;
268 : 21601 : Cand& cand = (*end);
269 : 21601 : ArithVar curr = cand.d_nb;
270 : 21601 : const Rational& coeff = *cand.d_coeff;
271 : :
272 : : LinearEqualityModule::UpdatePreferenceFunction leavingPrefFunc =
273 : 21601 : selectLeavingFunction(curr);
274 : : UpdateInfo currProposal =
275 : 21601 : d_linEq.speculativeUpdate(curr, coeff, leavingPrefFunc);
276 : :
277 [ + - ]: 43202 : Trace("soi::selectPrimalUpdate") << "selected " << selected << endl
278 : 0 : << "currProp " << currProposal << endl
279 : 21601 : << "coeff " << coeff << endl;
280 : :
281 [ - + ][ - + ]: 21601 : Assert(!currProposal.uninitialized());
[ - - ]
282 : :
283 [ + + ]: 21601 : if (candidatesAfterFocusImprove > 0)
284 : : {
285 : 3502 : candidatesAfterFocusImprove++;
286 : : }
287 : :
288 [ + + ][ - + ]: 21601 : if (selected.uninitialized() || (d_linEq.*upf)(selected, currProposal))
[ + + ][ + + ]
289 : : {
290 : 16926 : selected = currProposal;
291 : 16926 : WitnessImprovement w = selected.getWitness(false);
292 [ + - ]: 16926 : Trace("soi::selectPrimalUpdate") << "selected " << w << endl;
293 : : // setPenalty(curr, w);
294 [ + + ]: 16926 : if (improvement(w))
295 : : {
296 : : bool exitEarly;
297 [ + + ][ + ]: 11702 : switch (w)
298 : : {
299 : 41 : case ConflictFound: exitEarly = true; break;
300 : 2734 : case FocusImproved:
301 : 2734 : candidatesAfterFocusImprove = 1;
302 : 2734 : exitEarly = false;
303 : 2734 : break;
304 : 8927 : default: exitEarly = false; break;
305 : : }
306 [ + + ]: 11702 : if (exitEarly)
307 : : {
308 : 41 : break;
309 : : }
310 : : }
311 : : }
312 : : else
313 : : {
314 [ + - ]: 4675 : Trace("soi::selectPrimalUpdate") << "dropped " << endl;
315 : : }
316 [ + + ]: 21601 : }
317 : 14664 : return selected;
318 : 7332 : }
319 : :
320 : 7279 : bool debugCheckWitness(const UpdateInfo& inf,
321 : : WitnessImprovement w,
322 : : bool useBlands)
323 : : {
324 [ + - ]: 7279 : if (inf.getWitness(useBlands) == w)
325 : : {
326 [ + + ][ + - ]: 7279 : switch (w)
[ - - ][ + - ]
[ - ]
327 : : {
328 : 41 : case ConflictFound: return inf.foundConflict();
329 : 4258 : case ErrorDropped: return inf.errorsChange() < 0;
330 : 1128 : case FocusImproved: return inf.focusDirection() > 0;
331 : 0 : case FocusShrank: return false; // This is not a valid output
332 : 0 : case Degenerate: return false; // This is not a valid output
333 : 0 : case BlandsDegenerate: return useBlands;
334 : 1852 : case HeuristicDegenerate: return !useBlands;
335 : 0 : case AntiProductive: return false;
336 : : }
337 : : }
338 : 0 : return false;
339 : : }
340 : :
341 : 0 : void SumOfInfeasibilitiesSPD::debugPrintSignal(ArithVar updated) const
342 : : {
343 [ - - ]: 0 : Trace("updateAndSignal") << "updated basic " << updated;
344 [ - - ]: 0 : Trace("updateAndSignal") << " length " << d_tableau.basicRowLength(updated);
345 [ - - ]: 0 : Trace("updateAndSignal") << " consistent "
346 : 0 : << d_variables.assignmentIsConsistent(updated);
347 : 0 : int dir = !d_variables.assignmentIsConsistent(updated)
348 [ - - ]: 0 : ? d_errorSet.getSgn(updated)
349 : 0 : : 0;
350 [ - - ]: 0 : Trace("updateAndSignal") << " dir " << dir;
351 [ - - ]: 0 : Trace("updateAndSignal") << " debugBasicAtBoundCount "
352 : 0 : << d_linEq.debugBasicAtBoundCount(updated) << endl;
353 : 0 : }
354 : :
355 : 7279 : void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected)
356 : : {
357 : 7279 : ArithVar nonbasic = selected.nonbasic();
358 : :
359 [ + - ]: 7279 : Trace("updateAndSignal") << "updateAndSignal " << selected << endl;
360 : :
361 [ + + ]: 7279 : if (selected.describesPivot())
362 : : {
363 : 7158 : ConstraintP limiting = selected.limiting();
364 : 7158 : ArithVar basic = limiting->getVariable();
365 [ - + ][ - + ]: 7158 : Assert(d_linEq.basicIsTracked(basic));
[ - - ]
366 : 7158 : d_linEq.pivotAndUpdate(basic, nonbasic, limiting->getValue());
367 : : }
368 : : else
369 : : {
370 [ - + ][ - - ]: 121 : Assert(!selected.unbounded() || selected.errorsChange() < 0);
[ - + ][ - + ]
[ - - ]
371 : :
372 : : DeltaRational newAssignment =
373 : 121 : d_variables.getAssignment(nonbasic) + selected.nonbasicDelta();
374 : :
375 : 121 : d_linEq.updateTracked(nonbasic, newAssignment);
376 : 121 : }
377 : 7279 : d_pivots++;
378 : :
379 : 7279 : increaseLeavingCount(nonbasic);
380 : :
381 : 7279 : vector<pair<ArithVar, int> > focusChanges;
382 [ + + ]: 287534 : while (d_errorSet.moreSignals())
383 : : {
384 : 280255 : ArithVar updated = d_errorSet.topSignal();
385 : 280255 : int prevFocusSgn = d_errorSet.popSignal();
386 : :
387 [ + + ]: 280255 : if (d_tableau.isBasic(updated))
388 : : {
389 [ - + ][ - + ]: 273097 : Assert(!d_variables.assignmentIsConsistent(updated)
[ - - ]
390 : : == d_errorSet.inError(updated));
391 [ - + ]: 273097 : if (TraceIsOn("updateAndSignal"))
392 : : {
393 : 0 : debugPrintSignal(updated);
394 : : }
395 [ + + ]: 273097 : if (!d_variables.assignmentIsConsistent(updated))
396 : : {
397 [ + + ]: 4723 : if (checkBasicForConflict(updated))
398 : : {
399 : 1118 : reportConflict(updated);
400 : : // Assert(debugUpdatedBasic(selected, updated));
401 : : }
402 : : }
403 : : }
404 : : else
405 : : {
406 [ + - ]: 7158 : Trace("updateAndSignal") << "updated nonbasic " << updated << endl;
407 : : }
408 : 280255 : int currFocusSgn = d_errorSet.focusSgn(updated);
409 [ + + ]: 280255 : if (currFocusSgn != prevFocusSgn)
410 : : {
411 : 8138 : int change = currFocusSgn - prevFocusSgn;
412 : 8138 : focusChanges.push_back(make_pair(updated, change));
413 : : }
414 : : }
415 : :
416 [ - + ]: 7279 : if (TraceIsOn("error"))
417 : : {
418 [ - - ]: 0 : d_errorSet.debugPrint(Trace("error"));
419 : : }
420 : :
421 : : // Assert(debugSelectedErrorDropped(selected, d_errorSize,
422 : : // d_errorSet.errorSize()));
423 : :
424 : 7279 : adjustFocusAndError(focusChanges);
425 : 7279 : }
426 : :
427 : 0 : void SumOfInfeasibilitiesSPD::qeAddRange(uint32_t begin, uint32_t end)
428 : : {
429 : 0 : Assert(!d_qeInSoi.empty());
430 [ - - ]: 0 : for (uint32_t i = begin; i != end; ++i)
431 : : {
432 : 0 : ArithVar v = d_qeConflict[i];
433 : 0 : addToInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, v);
434 : 0 : d_qeInSoi.add(v);
435 : : }
436 : 0 : }
437 : :
438 : 0 : void SumOfInfeasibilitiesSPD::qeRemoveRange(uint32_t begin, uint32_t end)
439 : : {
440 [ - - ]: 0 : for (uint32_t i = begin; i != end; ++i)
441 : : {
442 : 0 : ArithVar v = d_qeConflict[i];
443 : 0 : removeFromInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, v);
444 : 0 : d_qeInSoi.remove(v);
445 : : }
446 : 0 : Assert(!d_qeInSoi.empty());
447 : 0 : }
448 : :
449 : 0 : void SumOfInfeasibilitiesSPD::qeSwapRange(uint32_t N, uint32_t r, uint32_t s)
450 : : {
451 [ - - ]: 0 : for (uint32_t i = 0; i < N; ++i)
452 : : {
453 : 0 : std::swap(d_qeConflict[r + i], d_qeConflict[s + i]);
454 : : }
455 : 0 : }
456 : :
457 : : /**
458 : : * Region notation:
459 : : * A region is either
460 : : * - A single element X@i with the name X at the position i
461 : : * - A sequence of indices X@[i,j) with the name X and the elements between i
462 : : * [inclusive] and j exclusive
463 : : * - A concatenation of regions R1 and R2, R1;R2
464 : : *
465 : : * Given the fixed assumptions C @ [0,cEnd) and a set of candidate minimizations
466 : : * U@[cEnd, uEnd) s.t. C \cup U is known to be in conflict ([0,uEnd) has a
467 : : * conflict), find a minimal subset of U, Delta, s.t. C \cup Delta is in
468 : : * conflict.
469 : : *
470 : : * Pre:
471 : : * [0, uEnd) is a set and is in conflict.
472 : : * uEnd <= assumptions.size()
473 : : * [0, cEnd) is in d_inSoi.
474 : : *
475 : : * Invariants: [0,cEnd) is never modified
476 : : *
477 : : * Post:
478 : : * [0, cEnd); [cEnd, deltaEnd) is in conflict
479 : : * [0, deltaEnd) is a set
480 : : * [0, deltaEnd) is in d_inSoi
481 : : */
482 : 0 : uint32_t SumOfInfeasibilitiesSPD::quickExplainRec(uint32_t cEnd, uint32_t uEnd)
483 : : {
484 : 0 : Assert(cEnd <= uEnd);
485 : 0 : Assert(d_qeInUAndNotInSoi.empty());
486 : 0 : Assert(d_qeGreedyOrder.empty());
487 : :
488 : 0 : const Tableau::Entry* spoiler = nullptr;
489 : :
490 : 0 : if (d_soiVar != ARITHVAR_SENTINEL
491 [ - - ][ - - ]: 0 : && d_linEq.selectSlackEntry(d_soiVar, false) == nullptr)
[ - - ]
492 : : {
493 : : // already in conflict
494 : 0 : return cEnd;
495 : : }
496 : :
497 : 0 : Assert(cEnd < uEnd);
498 : :
499 : : // Phase 1 : Construct the conflict greedily
500 : :
501 [ - - ]: 0 : for (uint32_t i = cEnd; i < uEnd; ++i)
502 : : {
503 : 0 : d_qeInUAndNotInSoi.add(d_qeConflict[i]);
504 : : }
505 [ - - ]: 0 : if (d_soiVar == ARITHVAR_SENTINEL)
506 : : { // special case for d_soiVar being empty
507 : 0 : ArithVar first = d_qeConflict[cEnd];
508 : 0 : d_soiVar = constructInfeasiblityFunction(
509 : 0 : d_statistics.d_soiConflictMinimization, first);
510 : 0 : d_qeInSoi.add(first);
511 : 0 : d_qeInUAndNotInSoi.remove(first);
512 : 0 : d_qeGreedyOrder.push_back(first);
513 : : }
514 [ - - ]: 0 : while ((spoiler = d_linEq.selectSlackEntry(d_soiVar, false)) != nullptr)
515 : : {
516 : 0 : Assert(!d_qeInUAndNotInSoi.empty());
517 : :
518 : 0 : ArithVar nb = spoiler->getColVar();
519 : 0 : int oppositeSgn = -(spoiler->getCoefficient().sgn());
520 : 0 : Assert(oppositeSgn != 0);
521 : :
522 : : ArithVar basicWithOp =
523 : 0 : find_basic_in_sgns(d_qeSgns, nb, oppositeSgn, d_qeInUAndNotInSoi, true);
524 : 0 : Assert(basicWithOp != ARITHVAR_SENTINEL);
525 : :
526 : 0 : addToInfeasFunc(
527 : 0 : d_statistics.d_soiConflictMinimization, d_soiVar, basicWithOp);
528 : 0 : d_qeInSoi.add(basicWithOp);
529 : 0 : d_qeInUAndNotInSoi.remove(basicWithOp);
530 : 0 : d_qeGreedyOrder.push_back(basicWithOp);
531 : : }
532 : 0 : Assert(spoiler == nullptr);
533 : :
534 : : // Compact the set u
535 : 0 : uint32_t newEnd = cEnd + d_qeGreedyOrder.size();
536 : 0 : std::copy(d_qeGreedyOrder.begin(),
537 : : d_qeGreedyOrder.end(),
538 : 0 : d_qeConflict.begin() + cEnd);
539 : :
540 : 0 : d_qeInUAndNotInSoi.purge();
541 : 0 : d_qeGreedyOrder.clear();
542 : :
543 : : // Phase 2 : Recursively determine the minimal set of rows
544 : :
545 : 0 : uint32_t xPos = cEnd;
546 : 0 : std::swap(d_qeGreedyOrder[xPos], d_qeGreedyOrder[newEnd - 1]);
547 : 0 : uint32_t uBegin = xPos + 1;
548 : 0 : uint32_t split = (newEnd - uBegin) / 2 + uBegin;
549 : :
550 : : // assumptions : C @ [0, cEnd); X @ xPos; U1 @ [u1Begin, split); U2 @ [split,
551 : : // newEnd)
552 : : // [0, newEnd) == d_inSoi
553 : :
554 : : uint32_t compactU2;
555 [ - - ]: 0 : if (split == newEnd)
556 : : { // U2 is empty
557 : 0 : compactU2 = newEnd;
558 : : }
559 : : else
560 : : {
561 : : // Remove U2 from Soi
562 : 0 : qeRemoveRange(split, newEnd);
563 : : // [0, split) == d_inSoi
564 : :
565 : : // pre assumptions: C + X + U1 @ [0,split); U2 [split, newEnd)
566 : 0 : compactU2 = quickExplainRec(split, newEnd);
567 : : // post:
568 : : // assumptions: C + X + U1 @ [0, split); delta2 @ [split - compactU2)
569 : : // d_inSoi = [0, compactU2)
570 : : }
571 : 0 : uint32_t deltaSize = compactU2 - split;
572 : 0 : qeSwapRange(deltaSize, uBegin, split);
573 : 0 : uint32_t d2End = uBegin + deltaSize;
574 : : // assumptions : C @ [0, cEnd); X @ xPos; delta2 @ [uBegin, d2End); U1 @
575 : : // [d2End, compactU2)
576 : : // d_inSoi == [0, compactU2)
577 : :
578 : : uint32_t d1End;
579 [ - - ]: 0 : if (d2End == compactU2)
580 : : { // U1 is empty
581 : 0 : d1End = d2End;
582 : : }
583 : : else
584 : : {
585 : 0 : qeRemoveRange(d2End, compactU2);
586 : :
587 : : // pre assumptions : C + X + delta2 @ [0, d2End); U1 @ [d2End, compactU2);
588 : 0 : d1End = quickExplainRec(d2End, compactU2);
589 : : // post:
590 : : // assumptions : C + X + delta2 @ [0, d2End); delta1 @ [d2End, d1End);
591 : : // d_inSoi = [0, d1End)
592 : : }
593 : : // After both:
594 : : // d_inSoi == [0, d1End), C @ [0, cEnd); X + delta2 + delta 1 @ [xPos,
595 : : // d1End);
596 : :
597 : 0 : Assert(d_qeInUAndNotInSoi.empty());
598 : 0 : Assert(d_qeGreedyOrder.empty());
599 : 0 : return d1End;
600 : : }
601 : :
602 : 0 : void SumOfInfeasibilitiesSPD::quickExplain()
603 : : {
604 : 0 : Assert(d_qeInSoi.empty());
605 : 0 : Assert(d_qeInUAndNotInSoi.empty());
606 : 0 : Assert(d_qeGreedyOrder.empty());
607 : 0 : Assert(d_soiVar == ARITHVAR_SENTINEL);
608 : 0 : Assert(d_qeSgns.empty());
609 : :
610 : 0 : d_qeConflict.clear();
611 : 0 : d_errorSet.pushFocusInto(d_qeConflict);
612 : :
613 : 0 : uint32_t size = d_qeConflict.size();
614 : :
615 [ - - ]: 0 : if (size > 2)
616 : : {
617 : 0 : for (ErrorSet::focus_iterator iter = d_errorSet.focusBegin(),
618 : 0 : end = d_errorSet.focusEnd();
619 [ - - ]: 0 : iter != end;
620 : 0 : ++iter)
621 : : {
622 : 0 : ArithVar e = *iter;
623 : 0 : addRowSgns(d_qeSgns, e, d_errorSet.getSgn(e));
624 : : }
625 : 0 : uint32_t end = quickExplainRec(0u, size);
626 : 0 : Assert(end <= d_qeConflict.size());
627 : 0 : Assert(d_soiVar != ARITHVAR_SENTINEL);
628 : 0 : Assert(!d_qeInSoi.empty());
629 : :
630 : 0 : d_qeConflict.resize(end);
631 : 0 : tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization,
632 : : d_soiVar);
633 : 0 : d_soiVar = ARITHVAR_SENTINEL;
634 : 0 : d_qeInSoi.purge();
635 : 0 : d_qeSgns.clear();
636 : : }
637 : :
638 : 0 : Assert(d_qeInSoi.empty());
639 : 0 : Assert(d_qeInUAndNotInSoi.empty());
640 : 0 : Assert(d_qeGreedyOrder.empty());
641 : 0 : Assert(d_soiVar == ARITHVAR_SENTINEL);
642 : 0 : Assert(d_qeSgns.empty());
643 : 0 : }
644 : :
645 : 24 : unsigned SumOfInfeasibilitiesSPD::trySet(const ArithVarVec& set)
646 : : {
647 [ - + ][ - + ]: 24 : Assert(d_soiVar == ARITHVAR_SENTINEL);
[ - - ]
648 : 24 : bool success = false;
649 [ + - ]: 24 : if (set.size() >= 2)
650 : : {
651 : 48 : d_soiVar = constructInfeasiblityFunction(
652 : 24 : d_statistics.d_soiConflictMinimization, set);
653 : 24 : success = d_linEq.selectSlackEntry(d_soiVar, false) == nullptr;
654 : :
655 : 24 : tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization,
656 : : d_soiVar);
657 : 24 : d_soiVar = ARITHVAR_SENTINEL;
658 : : }
659 [ + + ]: 24 : return success ? set.size() : std::numeric_limits<int>::max();
660 : : }
661 : :
662 : 53 : std::vector<ArithVarVec> SumOfInfeasibilitiesSPD::greedyConflictSubsets()
663 : : {
664 [ + - ]: 106 : Trace("arith::greedyConflictSubsets")
665 : 53 : << "greedyConflictSubsets start" << endl;
666 : :
667 : 53 : std::vector<ArithVarVec> subsets;
668 [ - + ][ - + ]: 53 : Assert(d_soiVar == ARITHVAR_SENTINEL);
[ - - ]
669 : :
670 [ + + ]: 53 : if (d_errorSize <= 2)
671 : : {
672 : 45 : ArithVarVec inError;
673 : 45 : d_errorSet.pushFocusInto(inError);
674 : :
675 [ - + ][ - + ]: 45 : Assert(debugIsASet(inError));
[ - - ]
676 : 45 : subsets.push_back(inError);
677 : 45 : return subsets;
678 : 45 : }
679 [ - + ][ - + ]: 8 : Assert(d_errorSize > 2);
[ - - ]
680 : :
681 : : // sgns_table< <nonbasic,sgn>, [basics] >;
682 : : // Phase 0: Construct the sgns table
683 : 8 : sgn_table sgns;
684 : 8 : DenseSet hasParticipated; // Has participated in a conflict
685 : 16 : for (ErrorSet::focus_iterator iter = d_errorSet.focusBegin(),
686 : 8 : end = d_errorSet.focusEnd();
687 [ + + ]: 38 : iter != end;
688 : 30 : ++iter)
689 : : {
690 : 30 : ArithVar e = *iter;
691 : 30 : addRowSgns(sgns, e, d_errorSet.getSgn(e));
692 : :
693 [ + - ]: 30 : Trace("arith::greedyConflictSubsets") << "basic error var: " << e << endl;
694 [ - + ]: 30 : if (TraceIsOn("arith::greedyConflictSubsets"))
695 : : {
696 : 0 : d_tableau.debugPrintIsBasic(e);
697 [ - - ]: 0 : d_tableau.printBasicRow(e, Trace("arith::greedyConflictSubsets"));
698 : : }
699 : : }
700 : :
701 : : // Phase 1: Try to find at least 1 pair for every element
702 : 8 : ArithVarVec tmp;
703 : 8 : tmp.push_back(0);
704 : 8 : tmp.push_back(0);
705 : 16 : for (ErrorSet::focus_iterator iter = d_errorSet.focusBegin(),
706 : 8 : end = d_errorSet.focusEnd();
707 [ + + ]: 38 : iter != end;
708 : 30 : ++iter)
709 : : {
710 : 30 : ArithVar e = *iter;
711 : 30 : tmp[0] = e;
712 : :
713 : 30 : int errSgn = d_errorSet.getSgn(e);
714 : 30 : bool decreasing = errSgn < 0;
715 : 30 : const Tableau::Entry* spoiler = d_linEq.selectSlackEntry(e, decreasing);
716 [ - + ][ - + ]: 30 : Assert(spoiler != nullptr);
[ - - ]
717 : 30 : ArithVar nb = spoiler->getColVar();
718 : 30 : int oppositeSgn = -(errSgn * (spoiler->getCoefficient().sgn()));
719 : :
720 : 30 : sgn_table::const_iterator opposites = find_sgns(sgns, nb, oppositeSgn);
721 [ - + ][ - + ]: 30 : Assert(opposites != sgns.end());
[ - - ]
722 : :
723 : 30 : const ArithVarVec& choices = (*opposites).second;
724 : 30 : for (ArithVarVec::const_iterator j = choices.begin(), jend = choices.end();
725 [ + + ]: 76 : j != jend;
726 : 46 : ++j)
727 : : {
728 : 46 : ArithVar b = *j;
729 [ + + ]: 46 : if (b < e)
730 : : {
731 : 22 : continue;
732 : : }
733 : 24 : tmp[0] = e;
734 : 24 : tmp[1] = b;
735 [ + + ]: 24 : if (trySet(tmp) == 2)
736 : : {
737 [ + - ]: 20 : Trace("arith::greedyConflictSubsets")
738 : 10 : << "found a pair " << b << " " << e << endl;
739 : 10 : hasParticipated.softAdd(b);
740 : 10 : hasParticipated.softAdd(e);
741 [ - + ][ - + ]: 10 : Assert(debugIsASet(tmp));
[ - - ]
742 : 10 : subsets.push_back(tmp);
743 : 10 : ++(d_statistics.d_soiConflicts);
744 : 10 : ++(d_statistics.d_hasToBeMinimal);
745 : : }
746 : : }
747 : : }
748 : :
749 : : // Phase 2: If there is a variable that has not participated attempt to start
750 : : // a conflict
751 : 8 : ArithVarVec possibleStarts; // List of elements that can be tried for starts.
752 : 8 : d_errorSet.pushFocusInto(possibleStarts);
753 [ + + ]: 38 : while (!possibleStarts.empty())
754 : : {
755 [ - + ][ - + ]: 30 : Assert(d_soiVar == ARITHVAR_SENTINEL);
[ - - ]
756 : :
757 : 30 : ArithVar v = possibleStarts.back();
758 : 30 : possibleStarts.pop_back();
759 [ + + ]: 30 : if (hasParticipated.isMember(v))
760 : : {
761 : 22 : continue;
762 : : }
763 : :
764 : 8 : hasParticipated.add(v);
765 : :
766 [ - + ][ - + ]: 8 : Assert(d_soiVar == ARITHVAR_SENTINEL);
[ - - ]
767 : : // d_soiVar's row = \sumofinfeasibilites underConstruction
768 : 8 : ArithVarVec underConstruction;
769 : 8 : underConstruction.push_back(v);
770 : 16 : d_soiVar = constructInfeasiblityFunction(
771 : 8 : d_statistics.d_soiConflictMinimization, v);
772 : :
773 [ + - ]: 8 : Trace("arith::greedyConflictSubsets") << "trying " << v << endl;
774 : :
775 : 8 : const Tableau::Entry* spoiler = nullptr;
776 [ + + ]: 18 : while ((spoiler = d_linEq.selectSlackEntry(d_soiVar, false)) != nullptr)
777 : : {
778 : 14 : ArithVar nb = spoiler->getColVar();
779 : 14 : int oppositeSgn = -(spoiler->getCoefficient().sgn());
780 [ - + ][ - + ]: 14 : Assert(oppositeSgn != 0);
[ - - ]
781 : :
782 [ + - ]: 28 : Trace("arith::greedyConflictSubsets")
783 : 14 : << "looking for " << nb << " " << oppositeSgn << endl;
784 : :
785 : : ArithVar basicWithOp =
786 : 14 : find_basic_in_sgns(sgns, nb, oppositeSgn, hasParticipated, false);
787 : :
788 [ + + ]: 14 : if (basicWithOp == ARITHVAR_SENTINEL)
789 : : {
790 [ + - ]: 8 : Trace("arith::greedyConflictSubsets")
791 : 4 : << "search did not work for " << nb << endl;
792 : : // greedy construction has failed
793 : 4 : break;
794 : : }
795 : : else
796 : : {
797 [ + - ]: 20 : Trace("arith::greedyConflictSubsets")
798 : 10 : << "found " << basicWithOp << endl;
799 : :
800 : 10 : addToInfeasFunc(
801 : 10 : d_statistics.d_soiConflictMinimization, d_soiVar, basicWithOp);
802 : 10 : hasParticipated.softAdd(basicWithOp);
803 : 10 : underConstruction.push_back(basicWithOp);
804 : : }
805 : : }
806 [ + + ]: 8 : if (spoiler == nullptr)
807 : : {
808 [ + - ]: 4 : Trace("arith::greedyConflictSubsets") << "success" << endl;
809 : : // then underConstruction contains a conflicting subset
810 [ - + ][ - + ]: 4 : Assert(debugIsASet(underConstruction));
[ - - ]
811 : 4 : subsets.push_back(underConstruction);
812 : 4 : ++d_statistics.d_soiConflicts;
813 [ + + ]: 4 : if (underConstruction.size() == 3)
814 : : {
815 : 2 : ++d_statistics.d_hasToBeMinimal;
816 : : }
817 : : else
818 : : {
819 : 2 : ++d_statistics.d_maybeNotMinimal;
820 : : }
821 : : }
822 : : else
823 : : {
824 [ + - ]: 4 : Trace("arith::greedyConflictSubsets") << "failure" << endl;
825 : : }
826 : 8 : tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization,
827 : : d_soiVar);
828 : 8 : d_soiVar = ARITHVAR_SENTINEL;
829 : 8 : }
830 : :
831 [ - + ][ - + ]: 8 : Assert(d_soiVar == ARITHVAR_SENTINEL);
[ - - ]
832 [ + - ]: 8 : Trace("arith::greedyConflictSubsets") << "greedyConflictSubsets done" << endl;
833 : 8 : return subsets;
834 : 8 : }
835 : :
836 : 59 : bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset)
837 : : {
838 [ - + ][ - + ]: 59 : Assert(d_soiVar == ARITHVAR_SENTINEL);
[ - - ]
839 : 118 : d_soiVar = constructInfeasiblityFunction(
840 : 59 : d_statistics.d_soiConflictMinimization, subset);
841 [ - + ][ - + ]: 59 : Assert(!subset.empty());
[ - - ]
842 [ - + ][ - + ]: 59 : Assert(!d_conflictBuilder->underConstruction());
[ - - ]
843 : :
844 [ + - ]: 118 : Trace("arith::generateSOIConflict")
845 : 59 : << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) start" << endl;
846 : :
847 : 59 : bool success = false;
848 : :
849 : 59 : for (ArithVarVec::const_iterator iter = subset.begin(), end = subset.end();
850 [ + + ]: 183 : iter != end;
851 : 124 : ++iter)
852 : : {
853 : 124 : ArithVar e = *iter;
854 : 124 : ConstraintP violated = d_errorSet.getViolated(e);
855 [ - + ][ - + ]: 124 : Assert(violated != NullConstraint);
[ - - ]
856 : :
857 : 124 : int sgn = d_errorSet.getSgn(e);
858 [ + + ]: 124 : const Rational& violatedCoeff = sgn > 0 ? d_negOne : d_posOne;
859 [ + - ]: 248 : Trace("arith::generateSOIConflict") << "basic error var: "
860 : 0 : << "(" << violatedCoeff << ")"
861 : 124 : << " " << violated << endl;
862 : :
863 : 124 : d_conflictBuilder->addConstraint(violated, violatedCoeff);
864 [ - + ][ - + ]: 124 : Assert(violated->hasProof());
[ - - ]
865 [ + + ][ + + ]: 124 : if (!success && !violated->negationHasProof())
[ + + ]
866 : : {
867 : 57 : success = true;
868 : 57 : d_conflictBuilder->makeLastConsequent();
869 : : }
870 : : }
871 : :
872 [ + + ]: 59 : if (!success)
873 : : {
874 : : // failure
875 : 2 : d_conflictBuilder->reset();
876 : : }
877 : : else
878 : : {
879 : : // pick a violated constraint arbitrarily. any of them may be selected for
880 : : // the conflict
881 [ - + ][ - + ]: 57 : Assert(d_conflictBuilder->underConstruction());
[ - - ]
882 [ - + ][ - + ]: 57 : Assert(d_conflictBuilder->consequentIsSet());
[ - - ]
883 : :
884 : 57 : for (Tableau::RowIterator i = d_tableau.basicRowIterator(d_soiVar);
885 [ + + ]: 798 : !i.atEnd();
886 : 741 : ++i)
887 : : {
888 : 741 : const Tableau::Entry& entry = *i;
889 : 741 : ArithVar v = entry.getColVar();
890 [ + + ]: 741 : if (v == d_soiVar)
891 : : {
892 : 57 : continue;
893 : : }
894 : 684 : const Rational& coeff = entry.getCoefficient();
895 : :
896 : 684 : ConstraintP c = (coeff.sgn() > 0)
897 [ + + ]: 684 : ? d_variables.getUpperBoundConstraint(v)
898 : 321 : : d_variables.getLowerBoundConstraint(v);
899 : :
900 [ + - ]: 1368 : Trace("arith::generateSOIConflict") << "non-basic var: "
901 : 0 : << "(" << coeff << ")"
902 : 684 : << " " << c << endl;
903 : 684 : d_conflictBuilder->addConstraint(c, coeff);
904 : : }
905 : 57 : ConstraintCP conflicted = d_conflictBuilder->commitConflict(nodeManager());
906 : 57 : d_conflictChannel.raiseConflict(conflicted,
907 : : InferenceId::ARITH_CONF_SOI_SIMPLEX);
908 : : }
909 : :
910 : 59 : tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization,
911 : : d_soiVar);
912 : 59 : d_soiVar = ARITHVAR_SENTINEL;
913 [ + - ]: 118 : Trace("arith::generateSOIConflict")
914 : 59 : << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) done" << endl;
915 [ - + ][ - + ]: 59 : Assert(d_soiVar == ARITHVAR_SENTINEL);
[ - - ]
916 [ - + ][ - + ]: 59 : Assert(!d_conflictBuilder->underConstruction());
[ - - ]
917 : 59 : return success;
918 : : }
919 : :
920 : 53 : WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict()
921 : : {
922 [ + - ]: 106 : Trace("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() start "
923 : 53 : << ": |E| = " << d_errorSize << endl;
924 [ - + ]: 53 : if (TraceIsOn("arith::SOIConflict"))
925 : : {
926 [ - - ]: 0 : d_errorSet.debugPrint(Trace("arith::SOIConflict"));
927 [ - - ]: 0 : Trace("arith::SOIConflict") << endl;
928 : : }
929 : :
930 : 53 : tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization,
931 : : d_soiVar);
932 : 53 : d_soiVar = ARITHVAR_SENTINEL;
933 : :
934 [ - + ]: 53 : if (options().arith.soiQuickExplain)
935 : : {
936 : 0 : quickExplain();
937 : 0 : generateSOIConflict(d_qeConflict);
938 : : }
939 : : else
940 : : {
941 : 53 : vector<ArithVarVec> subsets = greedyConflictSubsets();
942 [ - + ][ - + ]: 53 : Assert(d_soiVar == ARITHVAR_SENTINEL);
[ - - ]
943 : 53 : bool anySuccess = false;
944 [ - + ][ - + ]: 53 : Assert(!subsets.empty());
[ - - ]
945 : 53 : for (vector<ArithVarVec>::const_iterator i = subsets.begin(),
946 : 53 : end = subsets.end();
947 [ + + ]: 112 : i != end;
948 : 59 : ++i)
949 : : {
950 : 59 : const ArithVarVec& subset = *i;
951 [ - + ][ - + ]: 59 : Assert(debugIsASet(subset));
[ - - ]
952 [ + + ][ + - ]: 59 : anySuccess = generateSOIConflict(subset) || anySuccess;
953 : : // reportConflict(conf); do not do this. We need a custom explanations!
954 : : // d_conflictChannel(conflict);
955 : : }
956 [ - + ][ - + ]: 53 : Assert(anySuccess);
[ - - ]
957 : 53 : }
958 [ - + ][ - + ]: 53 : Assert(d_soiVar == ARITHVAR_SENTINEL);
[ - - ]
959 : 53 : d_soiVar =
960 : 53 : constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization);
961 : :
962 : : // reportConflict(conf); do not do this. We need a custom explanations!
963 : 53 : d_conflictVariables.add(d_soiVar);
964 : :
965 [ + - ]: 106 : Trace("arith::SOIConflict")
966 : 53 : << "SumOfInfeasibilitiesSPD::SOIConflict() end" << endl;
967 : 53 : return ConflictFound;
968 : : }
969 : :
970 : 7332 : WitnessImprovement SumOfInfeasibilitiesSPD::soiRound()
971 : : {
972 [ - + ][ - + ]: 7332 : Assert(d_soiVar != ARITHVAR_SENTINEL);
[ - - ]
973 : :
974 : : bool useBlands =
975 : 7332 : degeneratePivotsInARow() >= s_maxDegeneratePivotsBeforeBlandsOnLeaving;
976 : : LinearEqualityModule::UpdatePreferenceFunction upf;
977 [ - + ]: 7332 : if (useBlands)
978 : : {
979 : 0 : upf = &LinearEqualityModule::preferWitness<false>;
980 : : }
981 : : else
982 : : {
983 : 7332 : upf = &LinearEqualityModule::preferWitness<true>;
984 : : }
985 : :
986 : 7332 : UpdateInfo selected = selectUpdate(upf);
987 : :
988 [ + + ]: 7332 : if (selected.uninitialized())
989 : : {
990 [ + - ]: 106 : Trace("selectFocusImproving")
991 : 53 : << "SOI is optimum, but we don't have sat/conflict yet" << endl;
992 : 53 : return SOIConflict();
993 : : }
994 : : else
995 : : {
996 [ - + ][ - + ]: 7279 : Assert(!selected.uninitialized());
[ - - ]
997 : 7279 : WitnessImprovement w = selected.getWitness(false);
998 [ - + ][ - + ]: 7279 : Assert(debugCheckWitness(selected, w, false));
[ - - ]
999 : :
1000 : 7279 : updateAndSignal(selected);
1001 : 7279 : logPivot(w);
1002 : 7279 : return w;
1003 : : }
1004 : 7332 : }
1005 : :
1006 : 3734 : Result::Status SumOfInfeasibilitiesSPD::sumOfInfeasibilities()
1007 : : {
1008 : 3734 : TimerStat::CodeTimer codeTimer(d_statistics.d_soiTimer);
1009 : :
1010 [ - + ][ - + ]: 3734 : Assert(d_sgnDisagreements.empty());
[ - - ]
1011 [ - + ][ - + ]: 3734 : Assert(d_pivotBudget != 0);
[ - - ]
1012 [ - + ][ - + ]: 3734 : Assert(d_errorSize == d_errorSet.errorSize());
[ - - ]
1013 [ - + ][ - + ]: 3734 : Assert(d_errorSize > 0);
[ - - ]
1014 [ - + ][ - + ]: 3734 : Assert(d_conflictVariables.empty());
[ - - ]
1015 [ - + ][ - + ]: 3734 : Assert(d_soiVar == ARITHVAR_SENTINEL);
[ - - ]
1016 : :
1017 : : // d_scores.purge();
1018 : 3734 : d_soiVar =
1019 : 3734 : constructInfeasiblityFunction(d_statistics.d_soiFocusConstructionTimer);
1020 : :
1021 [ + - ][ + + ]: 11066 : while (d_pivotBudget != 0 && d_errorSize > 0 && d_conflictVariables.empty())
[ + + ][ + + ]
1022 : : {
1023 [ + - ]: 7332 : Trace("dualLike") << "dualLike" << endl;
1024 : :
1025 [ - + ][ - + ]: 7332 : Assert(d_errorSet.noSignals());
[ - - ]
1026 : : // Possible outcomes:
1027 : : // - conflict
1028 : : // - budget was exhausted
1029 : : // - focus went down
1030 : 7332 : WitnessImprovement w = soiRound();
1031 [ + - ]: 7332 : Trace("dualLike") << "selectFocusImproving -> " << w << endl;
1032 : :
1033 [ - + ][ - + ]: 7332 : Assert(d_errorSize == d_errorSet.errorSize());
[ - - ]
1034 : : }
1035 : :
1036 [ + - ]: 3734 : if (d_soiVar != ARITHVAR_SENTINEL)
1037 : : {
1038 : 3734 : tearDownInfeasiblityFunction(d_statistics.d_soiFocusConstructionTimer,
1039 : : d_soiVar);
1040 : 3734 : d_soiVar = ARITHVAR_SENTINEL;
1041 : : }
1042 : :
1043 [ - + ][ - + ]: 3734 : Assert(d_soiVar == ARITHVAR_SENTINEL);
[ - - ]
1044 [ + + ]: 3734 : if (!d_conflictVariables.empty())
1045 : : {
1046 : 983 : return Result::UNSAT;
1047 : : }
1048 [ + - ]: 2751 : else if (d_errorSet.errorEmpty())
1049 : : {
1050 [ - + ][ - + ]: 2751 : Assert(d_errorSet.noSignals());
[ - - ]
1051 : 2751 : return Result::SAT;
1052 : : }
1053 : : else
1054 : : {
1055 : 0 : Assert(d_pivotBudget == 0);
1056 : 0 : return Result::UNKNOWN;
1057 : : }
1058 : 3734 : }
1059 : :
1060 : : } // namespace arith::linear
1061 : : } // namespace theory
1062 : : } // namespace cvc5::internal
|
