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/fc_simplex.h"
14 : :
15 : : #include "base/output.h"
16 : : #include "options/arith_options.h"
17 : : #include "theory/arith/linear/constraint.h"
18 : : #include "theory/arith/linear/error_set.h"
19 : : #include "util/statistics_registry.h"
20 : : #include "util/statistics_stats.h"
21 : :
22 : : using namespace std;
23 : :
24 : : namespace cvc5::internal {
25 : : namespace theory {
26 : : namespace arith::linear {
27 : :
28 : 51329 : FCSimplexDecisionProcedure::FCSimplexDecisionProcedure(
29 : : Env& env,
30 : : LinearEqualityModule& linEq,
31 : : ErrorSet& errors,
32 : : RaiseConflict conflictChannel,
33 : 51329 : TempVarMalloc tvmalloc)
34 : : : SimplexDecisionProcedure(env, linEq, errors, conflictChannel, tvmalloc),
35 : 51329 : d_focusSize(0),
36 : 51329 : d_focusErrorVar(ARITHVAR_SENTINEL),
37 : 51329 : d_focusCoefficients(),
38 : 51329 : d_pivotBudget(0),
39 : 51329 : d_prevWitnessImprovement(AntiProductive),
40 : 51329 : d_witnessImprovementInARow(0),
41 : 51329 : d_sgnDisagreements(),
42 : 153987 : d_statistics(statisticsRegistry(), "theory::arith::FC::", d_pivots)
43 : : {
44 : 51329 : }
45 : :
46 : 51329 : FCSimplexDecisionProcedure::Statistics::Statistics(StatisticsRegistry& sr,
47 : : const std::string& name,
48 : 51329 : uint32_t& pivots)
49 : 51329 : : d_initialSignalsTime(sr.registerTimer(name + "initialProcessTime")),
50 : 51329 : d_initialConflicts(sr.registerInt(name + "UpdateConflicts")),
51 : 51329 : d_fcFoundUnsat(sr.registerInt(name + "FoundUnsat")),
52 : 51329 : d_fcFoundSat(sr.registerInt(name + "FoundSat")),
53 : 51329 : d_fcMissed(sr.registerInt(name + "Missed")),
54 : 51329 : d_fcTimer(sr.registerTimer(name + "Timer")),
55 : 51329 : d_fcFocusConstructionTimer(sr.registerTimer(name + "Construction")),
56 : : d_selectUpdateForDualLike(
57 : 51329 : sr.registerTimer(name + "selectUpdateForDualLike")),
58 : 51329 : d_selectUpdateForPrimal(sr.registerTimer(name + "selectUpdateForPrimal")),
59 : 51329 : d_finalCheckPivotCounter(
60 : 102658 : sr.registerReference<uint32_t>(name + "lastPivots", pivots))
61 : : {
62 : 51329 : }
63 : :
64 : 0 : Result::Status FCSimplexDecisionProcedure::findModel(bool exactResult)
65 : : {
66 : 0 : Assert(d_conflictVariables.empty());
67 : 0 : Assert(d_sgnDisagreements.empty());
68 : :
69 : 0 : d_pivots = 0;
70 : :
71 : 0 : if (d_errorSet.errorEmpty() && !d_errorSet.moreSignals())
72 : : {
73 [ - - ]: 0 : Trace("arith::findModel") << "fcFindModel() trivial" << endl;
74 : 0 : Assert(d_conflictVariables.empty());
75 : 0 : return Result::SAT;
76 : : }
77 : :
78 : : // We need to reduce this because of
79 : 0 : d_errorSet.reduceToSignals();
80 : :
81 : : // We must start tracking NOW
82 : 0 : d_errorSet.setSelectionRule(options::ErrorSelectionRule::SUM_METRIC);
83 : :
84 [ - - ]: 0 : if (initialProcessSignals())
85 : : {
86 : 0 : d_conflictVariables.purge();
87 [ - - ]: 0 : Trace("arith::findModel") << "fcFindModel() early conflict" << endl;
88 : 0 : Assert(d_conflictVariables.empty());
89 : 0 : return Result::UNSAT;
90 : : }
91 [ - - ]: 0 : else if (d_errorSet.errorEmpty())
92 : : {
93 [ - - ]: 0 : Trace("arith::findModel") << "fcFindModel() fixed itself" << endl;
94 : 0 : Assert(d_conflictVariables.empty());
95 : 0 : return Result::SAT;
96 : : }
97 : :
98 [ - - ]: 0 : Trace("arith::findModel") << "fcFindModel() start non-trivial" << endl;
99 : :
100 : 0 : exactResult |= d_varOrderPivotLimit < 0;
101 : :
102 : 0 : d_prevWitnessImprovement = HeuristicDegenerate;
103 : 0 : d_witnessImprovementInARow = 0;
104 : :
105 : 0 : Result::Status result = Result::UNKNOWN;
106 : :
107 [ - - ]: 0 : if (result == Result::UNKNOWN)
108 : : {
109 [ - - ]: 0 : if (exactResult)
110 : : {
111 : 0 : d_pivotBudget = -1;
112 : : }
113 : : else
114 : : {
115 : 0 : d_pivotBudget = d_varOrderPivotLimit;
116 : : }
117 : :
118 : 0 : result = dualLike();
119 : :
120 [ - - ]: 0 : if (result == Result::UNSAT)
121 : : {
122 : 0 : ++(d_statistics.d_fcFoundUnsat);
123 : : }
124 [ - - ]: 0 : else if (d_errorSet.errorEmpty())
125 : : {
126 : 0 : ++(d_statistics.d_fcFoundSat);
127 : : }
128 : : else
129 : : {
130 : 0 : ++(d_statistics.d_fcMissed);
131 : : }
132 : : }
133 : :
134 : 0 : Assert(!d_errorSet.moreSignals());
135 : 0 : if (result == Result::UNKNOWN && d_errorSet.errorEmpty())
136 : : {
137 : 0 : result = Result::SAT;
138 : : }
139 : :
140 : : // ensure that the conflict variable is still in the queue.
141 : 0 : d_conflictVariables.purge();
142 : :
143 [ - - ]: 0 : Trace("arith::findModel") << "end findModel() " << result << endl;
144 : :
145 : 0 : Assert(d_conflictVariables.empty());
146 : 0 : return result;
147 : : }
148 : :
149 : 0 : void FCSimplexDecisionProcedure::logPivot(WitnessImprovement w)
150 : : {
151 [ - - ]: 0 : if (d_pivotBudget > 0)
152 : : {
153 : 0 : --d_pivotBudget;
154 : : }
155 : 0 : Assert(w != AntiProductive);
156 : :
157 [ - - ]: 0 : if (w == d_prevWitnessImprovement)
158 : : {
159 : 0 : ++d_witnessImprovementInARow;
160 : : // ignore overflow : probably never reached
161 [ - - ]: 0 : if (d_witnessImprovementInARow == 0)
162 : : {
163 : 0 : --d_witnessImprovementInARow;
164 : : }
165 : : }
166 : : else
167 : : {
168 [ - - ]: 0 : if (w != BlandsDegenerate)
169 : : {
170 : 0 : d_witnessImprovementInARow = 1;
171 : : }
172 : : // if w == BlandsDegenerate do not reset the counter
173 : 0 : d_prevWitnessImprovement = w;
174 : : }
175 [ - - ]: 0 : if (strongImprovement(w))
176 : : {
177 : 0 : d_leavingCountSinceImprovement.purge();
178 : : }
179 : :
180 [ - - ]: 0 : Trace("logPivot") << "logPivot " << d_prevWitnessImprovement << " "
181 : 0 : << d_witnessImprovementInARow << endl;
182 : 0 : }
183 : :
184 : 0 : uint32_t FCSimplexDecisionProcedure::degeneratePivotsInARow() const
185 : : {
186 [ - - ][ - - ]: 0 : switch (d_prevWitnessImprovement)
187 : : {
188 : 0 : case ConflictFound:
189 : : case ErrorDropped:
190 : 0 : case FocusImproved: return 0;
191 : 0 : case HeuristicDegenerate:
192 : 0 : case BlandsDegenerate: return d_witnessImprovementInARow;
193 : : // Degenerate is unreachable for its own reasons
194 : 0 : case Degenerate:
195 : : case FocusShrank:
196 : 0 : case AntiProductive: Unreachable(); return -1;
197 : : }
198 : 0 : Unreachable();
199 : : }
200 : :
201 : 0 : void FCSimplexDecisionProcedure::adjustFocusAndError(
202 : : const AVIntPairVec& focusChanges)
203 : : {
204 : 0 : uint32_t newErrorSize = d_errorSet.errorSize();
205 : 0 : uint32_t newFocusSize = d_errorSet.focusSize();
206 : :
207 : : // Assert(!d_conflictVariables.empty() || newFocusSize <= d_focusSize);
208 : 0 : Assert(!d_conflictVariables.empty() || newErrorSize <= d_errorSize);
209 : :
210 [ - - ][ - - ]: 0 : if (newFocusSize == 0 || !d_conflictVariables.empty())
[ - - ]
211 : : {
212 : 0 : tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer,
213 : : d_focusErrorVar);
214 : 0 : d_focusErrorVar = ARITHVAR_SENTINEL;
215 : : }
216 [ - - ]: 0 : else if (2 * newFocusSize < d_focusSize)
217 : : {
218 : 0 : tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer,
219 : : d_focusErrorVar);
220 : 0 : d_focusErrorVar =
221 : 0 : constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer);
222 : : }
223 : : else
224 : : {
225 : 0 : adjustInfeasFunc(
226 : 0 : d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar, focusChanges);
227 : : }
228 : :
229 : 0 : d_errorSize = newErrorSize;
230 : 0 : d_focusSize = newFocusSize;
231 : 0 : }
232 : :
233 : 0 : WitnessImprovement FCSimplexDecisionProcedure::adjustFocusShrank(
234 : : const ArithVarVec& dropped)
235 : : {
236 : 0 : Assert(dropped.size() > 0);
237 : 0 : Assert(d_errorSet.focusSize() == d_focusSize);
238 : 0 : Assert(d_errorSet.focusSize() > dropped.size());
239 : :
240 : 0 : uint32_t newFocusSize = d_focusSize - dropped.size();
241 : 0 : Assert(newFocusSize > 0);
242 : :
243 [ - - ]: 0 : if (2 * newFocusSize <= d_focusSize)
244 : : {
245 : 0 : d_errorSet.dropFromFocusAll(dropped);
246 : 0 : tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer,
247 : : d_focusErrorVar);
248 : 0 : d_focusErrorVar =
249 : 0 : constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer);
250 : : }
251 : : else
252 : : {
253 : 0 : shrinkInfeasFunc(
254 : 0 : d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar, dropped);
255 : 0 : d_errorSet.dropFromFocusAll(dropped);
256 : : }
257 : :
258 : 0 : d_focusSize = newFocusSize;
259 : 0 : Assert(d_errorSet.focusSize() == d_focusSize);
260 : 0 : return FocusShrank;
261 : : }
262 : :
263 : 0 : WitnessImprovement FCSimplexDecisionProcedure::focusDownToJust(ArithVar v)
264 : : {
265 : : // uint32_t newErrorSize = d_errorSet.errorSize();
266 : : // uint32_t newFocusSize = d_errorSet.focusSize();
267 : 0 : Assert(d_focusSize == d_errorSet.focusSize());
268 : 0 : Assert(d_focusSize > 1);
269 : 0 : Assert(d_errorSet.inFocus(v));
270 : :
271 : 0 : d_errorSet.focusDownToJust(v);
272 : 0 : Assert(d_errorSet.focusSize() == 1);
273 : 0 : d_focusSize = 1;
274 : :
275 : 0 : tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer,
276 : : d_focusErrorVar);
277 : 0 : d_focusErrorVar =
278 : 0 : constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer);
279 : :
280 : 0 : return FocusShrank;
281 : : }
282 : :
283 : 0 : UpdateInfo FCSimplexDecisionProcedure::selectPrimalUpdate(
284 : : ArithVar basic, LinearEqualityModule::UpdatePreferenceFunction upf)
285 : : {
286 : 0 : UpdateInfo selected;
287 : :
288 [ - - ]: 0 : Trace("arith::selectPrimalUpdate")
289 : 0 : << "selectPrimalUpdate" << endl
290 : 0 : << basic << " " << d_tableau.basicRowLength(basic) << " "
291 : 0 : << d_linEq.debugBasicAtBoundCount(basic) << endl;
292 : :
293 : : static constexpr int s_maxCandidatesAfterImprove = 3;
294 : 0 : bool isFocus = basic == d_focusErrorVar;
295 : 0 : Assert(isFocus || d_errorSet.inError(basic));
296 [ - - ]: 0 : int basicDir = isFocus ? 1 : d_errorSet.getSgn(basic);
297 [ - - ][ - - ]: 0 : bool dualLike = !isFocus && d_focusSize > 1;
298 : :
299 [ - - ]: 0 : if (!isFocus)
300 : : {
301 : 0 : loadFocusSigns();
302 : : }
303 : :
304 : 0 : decreasePenalties();
305 : :
306 : : typedef std::vector<Cand> CandVector;
307 : 0 : CandVector candidates;
308 : :
309 [ - - ]: 0 : for (Tableau::RowIterator ri = d_tableau.basicRowIterator(basic); !ri.atEnd();
310 : 0 : ++ri)
311 : : {
312 : 0 : const Tableau::Entry& e = *ri;
313 : 0 : ArithVar curr = e.getColVar();
314 [ - - ]: 0 : if (curr == basic)
315 : : {
316 : 0 : continue;
317 : : }
318 : :
319 : 0 : int sgn = e.getCoefficient().sgn();
320 : 0 : int curr_movement = basicDir * sgn;
321 : :
322 : : bool candidate =
323 [ - - ]: 0 : (curr_movement > 0 && d_variables.cmpAssignmentUpperBound(curr) < 0)
324 : 0 : || (curr_movement < 0 && d_variables.cmpAssignmentLowerBound(curr) > 0);
325 : :
326 [ - - ]: 0 : Trace("arith::selectPrimalUpdate")
327 : 0 : << "storing " << basic << " " << curr << " " << candidate << " "
328 : 0 : << e.getCoefficient() << " " << curr_movement << " "
329 : 0 : << focusCoefficient(curr) << endl;
330 : :
331 [ - - ]: 0 : if (!candidate)
332 : : {
333 : 0 : continue;
334 : : }
335 : :
336 [ - - ]: 0 : if (!isFocus)
337 : : {
338 : 0 : const Rational& focusC = focusCoefficient(curr);
339 : 0 : Assert(dualLike || !focusC.isZero());
340 : 0 : if (dualLike && curr_movement != focusC.sgn())
341 : : {
342 [ - - ]: 0 : Trace("arith::selectPrimalUpdate")
343 : 0 : << "sgn disagreement " << curr << endl;
344 : 0 : d_sgnDisagreements.push_back(curr);
345 : 0 : continue;
346 : : }
347 : : else
348 : : {
349 : 0 : candidates.push_back(Cand(curr, penalty(curr), curr_movement, &focusC));
350 : : }
351 : : }
352 : : else
353 : : {
354 : 0 : candidates.push_back(
355 : 0 : Cand(curr, penalty(curr), curr_movement, &e.getCoefficient()));
356 : : }
357 : : }
358 : :
359 : 0 : CompPenaltyColLength colCmp(&d_linEq, options().arith.havePenalties);
360 : 0 : CandVector::iterator i = candidates.begin();
361 : 0 : CandVector::iterator end = candidates.end();
362 : 0 : std::make_heap(i, end, colCmp);
363 : :
364 : 0 : bool checkEverything = d_pivots == 0;
365 : :
366 : 0 : int candidatesAfterFocusImprove = 0;
367 : 0 : while (i != end
368 [ - - ][ - - ]: 0 : && (checkEverything
[ - - ]
369 [ - - ]: 0 : || candidatesAfterFocusImprove <= s_maxCandidatesAfterImprove))
370 : : {
371 : 0 : std::pop_heap(i, end, colCmp);
372 : 0 : --end;
373 : 0 : Cand& cand = (*end);
374 : 0 : ArithVar curr = cand.d_nb;
375 : 0 : const Rational& coeff = *cand.d_coeff;
376 : :
377 : : LinearEqualityModule::UpdatePreferenceFunction leavingPrefFunc =
378 : 0 : selectLeavingFunction(curr);
379 : : UpdateInfo currProposal =
380 : 0 : d_linEq.speculativeUpdate(curr, coeff, leavingPrefFunc);
381 : :
382 [ - - ]: 0 : Trace("arith::selectPrimalUpdate") << "selected " << selected << endl
383 : 0 : << "currProp " << currProposal << endl
384 : 0 : << "coeff " << coeff << endl;
385 : :
386 : 0 : Assert(!currProposal.uninitialized());
387 : :
388 [ - - ]: 0 : if (candidatesAfterFocusImprove > 0)
389 : : {
390 : 0 : candidatesAfterFocusImprove++;
391 : : }
392 : :
393 : 0 : if (selected.uninitialized() || (d_linEq.*upf)(selected, currProposal))
394 : : {
395 : 0 : selected = currProposal;
396 : 0 : WitnessImprovement w = selected.getWitness(false);
397 [ - - ]: 0 : Trace("arith::selectPrimalUpdate") << "selected " << w << endl;
398 : 0 : setPenalty(curr, w);
399 [ - - ]: 0 : if (improvement(w))
400 : : {
401 : : bool exitEarly;
402 [ - - ][ - - ]: 0 : switch (w)
403 : : {
404 : 0 : case ConflictFound: exitEarly = true; break;
405 : 0 : case ErrorDropped:
406 [ - - ]: 0 : if (checkEverything)
407 : : {
408 : 0 : exitEarly = d_errorSize + selected.errorsChange() == 0;
409 [ - - ]: 0 : Trace("arith::selectPrimalUpdate")
410 : 0 : << "ee " << d_errorSize << " " << selected.errorsChange()
411 : 0 : << " " << d_errorSize + selected.errorsChange() << endl;
412 : : }
413 : : else
414 : : {
415 : 0 : exitEarly = true;
416 : : }
417 : 0 : break;
418 : 0 : case FocusImproved:
419 : 0 : candidatesAfterFocusImprove = 1;
420 : 0 : exitEarly = false;
421 : 0 : break;
422 : 0 : default: exitEarly = false; break;
423 : : }
424 [ - - ]: 0 : if (exitEarly)
425 : : {
426 : 0 : break;
427 : : }
428 : : }
429 : : }
430 : : else
431 : : {
432 [ - - ]: 0 : Trace("arith::selectPrimalUpdate") << "dropped " << endl;
433 : : }
434 [ - - ]: 0 : }
435 : :
436 [ - - ]: 0 : if (!isFocus)
437 : : {
438 : 0 : unloadFocusSigns();
439 : : }
440 : 0 : return selected;
441 : 0 : }
442 : :
443 : 0 : bool FCSimplexDecisionProcedure::debugCheckWitness(const UpdateInfo& inf,
444 : : WitnessImprovement w,
445 : : bool useBlands)
446 : : {
447 [ - - ]: 0 : if (inf.getWitness(useBlands) == w)
448 : : {
449 [ - - ][ - - ]: 0 : switch (w)
[ - - ][ - - ]
[ - ]
450 : : {
451 : 0 : case ConflictFound: return inf.foundConflict();
452 : 0 : case ErrorDropped: return inf.errorsChange() < 0;
453 : 0 : case FocusImproved: return inf.focusDirection() > 0;
454 : 0 : case FocusShrank: return false; // This is not a valid output
455 : 0 : case Degenerate: return false; // This is not a valid output
456 : 0 : case BlandsDegenerate: return useBlands;
457 : 0 : case HeuristicDegenerate: return !useBlands;
458 : 0 : case AntiProductive: return false;
459 : : }
460 : : }
461 : 0 : return false;
462 : : }
463 : :
464 : 0 : WitnessImprovement FCSimplexDecisionProcedure::primalImproveError(
465 : : ArithVar errorVar)
466 : : {
467 : : bool useBlands =
468 : 0 : degeneratePivotsInARow() >= s_maxDegeneratePivotsBeforeBlandsOnLeaving;
469 : 0 : UpdateInfo selected = selectUpdateForPrimal(errorVar, useBlands);
470 : 0 : Assert(!selected.uninitialized());
471 : 0 : WitnessImprovement w = selected.getWitness(useBlands);
472 : 0 : Assert(debugCheckWitness(selected, w, useBlands));
473 : :
474 : 0 : updateAndSignal(selected);
475 : 0 : logPivot(w);
476 : 0 : return w;
477 : 0 : }
478 : :
479 : 0 : WitnessImprovement FCSimplexDecisionProcedure::focusUsingSignDisagreements(
480 : : ArithVar basic)
481 : : {
482 : 0 : Assert(!d_sgnDisagreements.empty());
483 : 0 : Assert(d_errorSet.focusSize() >= 2);
484 : :
485 [ - - ]: 0 : if (TraceIsOn("arith::focus"))
486 : : {
487 [ - - ]: 0 : d_errorSet.debugPrint(Trace("arith::focus"));
488 : : }
489 : :
490 : : ArithVar nb =
491 : 0 : d_linEq.minBy(d_sgnDisagreements, &LinearEqualityModule::minColLength);
492 : 0 : const Tableau::Entry& e_evar_nb = d_tableau.basicFindEntry(basic, nb);
493 : 0 : int oppositeSgn = -(e_evar_nb.getCoefficient().sgn());
494 [ - - ]: 0 : Trace("arith::focus") << "focusUsingSignDisagreements " << basic << " "
495 : 0 : << oppositeSgn << endl;
496 : :
497 : 0 : ArithVarVec dropped;
498 : :
499 : 0 : Tableau::ColIterator colIter = d_tableau.colIterator(nb);
500 [ - - ]: 0 : for (; !colIter.atEnd(); ++colIter)
501 : : {
502 : 0 : const Tableau::Entry& entry = *colIter;
503 : 0 : Assert(entry.getColVar() == nb);
504 : :
505 : 0 : int sgn = entry.getCoefficient().sgn();
506 [ - - ]: 0 : Trace("arith::focus") << "on row "
507 : 0 : << d_tableau.rowIndexToBasic(entry.getRowIndex())
508 : 0 : << " " << entry.getCoefficient() << endl;
509 : 0 : ArithVar currRow = d_tableau.rowIndexToBasic(entry.getRowIndex());
510 : 0 : if (d_errorSet.inError(currRow) && d_errorSet.inFocus(currRow))
511 : : {
512 : 0 : int errSgn = d_errorSet.getSgn(currRow);
513 : :
514 [ - - ]: 0 : if (errSgn * sgn == oppositeSgn)
515 : : {
516 : 0 : dropped.push_back(currRow);
517 [ - - ]: 0 : Trace("arith::focus") << "dropping from focus " << currRow << endl;
518 : : }
519 : : }
520 : : }
521 : :
522 : 0 : d_sgnDisagreements.clear();
523 : 0 : return adjustFocusShrank(dropped);
524 : 0 : }
525 : :
526 : 0 : bool debugSelectedErrorDropped(const UpdateInfo& selected,
527 : : int32_t prevErrorSize,
528 : : int32_t currErrorSize)
529 : : {
530 : 0 : int diff = currErrorSize - prevErrorSize;
531 [ - - ][ - - ]: 0 : return selected.foundConflict() || diff == selected.errorsChange();
532 : : }
533 : :
534 : 0 : void FCSimplexDecisionProcedure::debugPrintSignal(ArithVar updated) const
535 : : {
536 [ - - ]: 0 : Trace("updateAndSignal") << "updated basic " << updated;
537 [ - - ]: 0 : Trace("updateAndSignal") << " length " << d_tableau.basicRowLength(updated);
538 [ - - ]: 0 : Trace("updateAndSignal") << " consistent "
539 : 0 : << d_variables.assignmentIsConsistent(updated);
540 : 0 : int dir = !d_variables.assignmentIsConsistent(updated)
541 [ - - ]: 0 : ? d_errorSet.getSgn(updated)
542 : 0 : : 0;
543 [ - - ]: 0 : Trace("updateAndSignal") << " dir " << dir;
544 [ - - ]: 0 : Trace("updateAndSignal") << " debugBasicAtBoundCount "
545 : 0 : << d_linEq.debugBasicAtBoundCount(updated) << endl;
546 : 0 : }
547 : :
548 : 0 : bool debugUpdatedBasic(const UpdateInfo& selected, ArithVar updated)
549 : : {
550 [ - - ][ - - ]: 0 : if (selected.describesPivot() && updated == selected.leaving())
[ - - ]
551 : : {
552 : 0 : return selected.foundConflict();
553 : : }
554 : : else
555 : : {
556 : 0 : return true;
557 : : }
558 : : }
559 : :
560 : 0 : void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected)
561 : : {
562 : 0 : ArithVar nonbasic = selected.nonbasic();
563 : :
564 [ - - ]: 0 : Trace("updateAndSignal") << "updateAndSignal " << selected << endl;
565 : :
566 : 0 : stringstream ss;
567 : :
568 [ - - ]: 0 : if (selected.describesPivot())
569 : : {
570 : 0 : ConstraintP limiting = selected.limiting();
571 : 0 : ArithVar basic = limiting->getVariable();
572 : 0 : Assert(d_linEq.basicIsTracked(basic));
573 : 0 : d_linEq.pivotAndUpdate(basic, nonbasic, limiting->getValue());
574 : : }
575 : : else
576 : : {
577 : 0 : Assert(!selected.unbounded() || selected.errorsChange() < 0);
578 : :
579 : : DeltaRational newAssignment =
580 : 0 : d_variables.getAssignment(nonbasic) + selected.nonbasicDelta();
581 : :
582 : 0 : d_linEq.updateTracked(nonbasic, newAssignment);
583 : 0 : }
584 : 0 : d_pivots++;
585 : :
586 : 0 : increaseLeavingCount(nonbasic);
587 : :
588 : 0 : vector<pair<ArithVar, int> > focusChanges;
589 [ - - ]: 0 : while (d_errorSet.moreSignals())
590 : : {
591 : 0 : ArithVar updated = d_errorSet.topSignal();
592 : 0 : int prevFocusSgn = d_errorSet.popSignal();
593 : :
594 [ - - ]: 0 : if (d_tableau.isBasic(updated))
595 : : {
596 : 0 : Assert(!d_variables.assignmentIsConsistent(updated)
597 : : == d_errorSet.inError(updated));
598 [ - - ]: 0 : if (TraceIsOn("updateAndSignal"))
599 : : {
600 : 0 : debugPrintSignal(updated);
601 : : }
602 [ - - ]: 0 : if (!d_variables.assignmentIsConsistent(updated))
603 : : {
604 [ - - ]: 0 : if (checkBasicForConflict(updated))
605 : : {
606 : 0 : reportConflict(updated);
607 : 0 : Assert(debugUpdatedBasic(selected, updated));
608 : : }
609 : : }
610 : : }
611 : : else
612 : : {
613 [ - - ]: 0 : Trace("updateAndSignal") << "updated nonbasic " << updated << endl;
614 : : }
615 : 0 : int currFocusSgn = d_errorSet.focusSgn(updated);
616 [ - - ]: 0 : if (currFocusSgn != prevFocusSgn)
617 : : {
618 : 0 : int change = currFocusSgn - prevFocusSgn;
619 : 0 : focusChanges.push_back(make_pair(updated, change));
620 : : }
621 : : }
622 : :
623 [ - - ]: 0 : if (TraceIsOn("error"))
624 : : {
625 [ - - ]: 0 : d_errorSet.debugPrint(Trace("error"));
626 : : }
627 : :
628 : 0 : Assert(
629 : : debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize()));
630 : :
631 : 0 : adjustFocusAndError(focusChanges);
632 : 0 : }
633 : :
634 : 0 : WitnessImprovement FCSimplexDecisionProcedure::dualLikeImproveError(
635 : : ArithVar errorVar)
636 : : {
637 : 0 : Assert(d_sgnDisagreements.empty());
638 : 0 : Assert(d_focusSize > 1);
639 : :
640 : 0 : UpdateInfo selected = selectUpdateForDualLike(errorVar);
641 : :
642 [ - - ]: 0 : if (selected.uninitialized())
643 : : {
644 : : // we found no proposals
645 : : // If this is empty, there must be an error on this variable!
646 : : // this should not be possible. It Should have been caught as a signal
647 : : // earlier
648 : 0 : WitnessImprovement dropped = focusUsingSignDisagreements(errorVar);
649 : 0 : Assert(d_sgnDisagreements.empty());
650 : :
651 : 0 : return dropped;
652 : : }
653 : : else
654 : : {
655 : 0 : d_sgnDisagreements.clear();
656 : : }
657 : :
658 : 0 : Assert(d_sgnDisagreements.empty());
659 : 0 : Assert(!selected.uninitialized());
660 : :
661 : 0 : if (selected.focusDirection() == 0
662 [ - - ]: 0 : && d_prevWitnessImprovement == HeuristicDegenerate
663 [ - - ][ - - ]: 0 : && d_witnessImprovementInARow >= s_focusThreshold)
[ - - ]
664 : : {
665 [ - - ]: 0 : Trace("focusDownToJust") << "focusDownToJust " << errorVar << endl;
666 : :
667 : 0 : return focusDownToJust(errorVar);
668 : : }
669 : : else
670 : : {
671 : 0 : WitnessImprovement w = selected.getWitness(false);
672 : 0 : Assert(debugCheckWitness(selected, w, false));
673 : 0 : updateAndSignal(selected);
674 : 0 : logPivot(w);
675 : 0 : return w;
676 : : }
677 : 0 : }
678 : :
679 : 0 : WitnessImprovement FCSimplexDecisionProcedure::focusDownToLastHalf()
680 : : {
681 : 0 : Assert(d_focusSize >= 2);
682 : :
683 [ - - ]: 0 : Trace("focusDownToLastHalf")
684 : 0 : << "focusDownToLastHalf " << d_errorSet.errorSize() << " "
685 : 0 : << d_errorSet.focusSize() << " ";
686 : :
687 : 0 : uint32_t half = d_focusSize / 2;
688 : 0 : ArithVarVec buf;
689 : 0 : for (ErrorSet::focus_iterator i = d_errorSet.focusBegin(),
690 : 0 : i_end = d_errorSet.focusEnd();
691 [ - - ]: 0 : i != i_end;
692 : 0 : ++i)
693 : : {
694 [ - - ]: 0 : if (half > 0)
695 : : {
696 : 0 : --half;
697 : : }
698 : : else
699 : : {
700 : 0 : buf.push_back(*i);
701 : : }
702 : : }
703 : 0 : WitnessImprovement w = adjustFocusShrank(buf);
704 [ - - ]: 0 : Trace("focusDownToLastHalf") << "-> " << d_errorSet.focusSize() << endl;
705 : 0 : return w;
706 : 0 : }
707 : :
708 : 0 : WitnessImprovement FCSimplexDecisionProcedure::selectFocusImproving()
709 : : {
710 : 0 : Assert(d_focusErrorVar != ARITHVAR_SENTINEL);
711 : 0 : Assert(d_focusSize >= 2);
712 : :
713 : 0 : LinearEqualityModule::UpdatePreferenceFunction upf =
714 : : &LinearEqualityModule::preferWitness<true>;
715 : :
716 : 0 : UpdateInfo selected = selectPrimalUpdate(d_focusErrorVar, upf);
717 : :
718 [ - - ]: 0 : if (selected.uninitialized())
719 : : {
720 [ - - ]: 0 : Trace("selectFocusImproving")
721 : 0 : << "focus is optimum, but we don't have sat/conflict yet" << endl;
722 : :
723 : 0 : return focusDownToLastHalf();
724 : : }
725 : 0 : Assert(!selected.uninitialized());
726 : 0 : WitnessImprovement w = selected.getWitness(false);
727 : 0 : Assert(debugCheckWitness(selected, w, false));
728 : :
729 [ - - ]: 0 : if (degenerate(w))
730 : : {
731 [ - - ]: 0 : Trace("selectFocusImproving") << "only degenerate" << endl;
732 [ - - ]: 0 : if (d_prevWitnessImprovement == HeuristicDegenerate
733 [ - - ]: 0 : && d_witnessImprovementInARow >= s_focusThreshold)
734 : : {
735 [ - - ]: 0 : Trace("selectFocusImproving")
736 : 0 : << "focus down been degenerate too long" << endl;
737 : 0 : return focusDownToLastHalf();
738 : : }
739 : : else
740 : : {
741 [ - - ]: 0 : Trace("selectFocusImproving") << "taking degenerate" << endl;
742 : : }
743 : : }
744 [ - - ]: 0 : Trace("selectFocusImproving")
745 : 0 : << "selectFocusImproving did this " << selected << endl;
746 : :
747 : 0 : updateAndSignal(selected);
748 : 0 : logPivot(w);
749 : 0 : return w;
750 : 0 : }
751 : :
752 : 0 : bool FCSimplexDecisionProcedure::debugDualLike(WitnessImprovement w,
753 : : ostream& out,
754 : : uint32_t prevFocusSize,
755 : : uint32_t prevErrorSize) const
756 : : {
757 : 0 : out << "DLV() ";
758 [ - - ][ - - ]: 0 : switch (w)
[ - - ][ - - ]
[ - ]
759 : : {
760 : 0 : case ConflictFound:
761 : 0 : out << "found conflict" << endl;
762 : 0 : return !d_conflictVariables.empty();
763 : 0 : case ErrorDropped:
764 : 0 : out << "dropped " << prevErrorSize - d_errorSize << endl;
765 : 0 : return d_errorSize < prevErrorSize;
766 : 0 : case FocusImproved:
767 : 0 : out << "focus improved" << endl;
768 : 0 : return d_errorSize == prevErrorSize;
769 : 0 : case FocusShrank:
770 : 0 : out << "focus shrank" << endl;
771 [ - - ][ - - ]: 0 : return d_errorSize == prevErrorSize && prevFocusSize > d_focusSize;
772 : 0 : case BlandsDegenerate: out << "bland degenerate" << endl; return true;
773 : 0 : case HeuristicDegenerate:
774 : 0 : out << "heuristic degenerate" << endl;
775 : 0 : return true;
776 : 0 : case AntiProductive: out << "focus blur" << endl; return prevFocusSize == 0;
777 : 0 : case Degenerate: return false;
778 : : }
779 : 0 : return false;
780 : : }
781 : :
782 : 0 : Result::Status FCSimplexDecisionProcedure::dualLike()
783 : : {
784 : 0 : TimerStat::CodeTimer codeTimer(d_statistics.d_fcTimer);
785 : :
786 : 0 : Assert(d_sgnDisagreements.empty());
787 : 0 : Assert(d_pivotBudget != 0);
788 : 0 : Assert(d_errorSize == d_errorSet.errorSize());
789 : 0 : Assert(d_errorSize > 0);
790 : 0 : Assert(d_focusSize == d_errorSet.focusSize());
791 : 0 : Assert(d_focusSize > 0);
792 : 0 : Assert(d_conflictVariables.empty());
793 : 0 : Assert(d_focusErrorVar == ARITHVAR_SENTINEL);
794 : :
795 : 0 : d_scores.purge();
796 : 0 : d_focusErrorVar =
797 : 0 : constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer);
798 : :
799 : 0 : while (d_pivotBudget != 0 && d_errorSize > 0 && d_conflictVariables.empty())
800 : : {
801 [ - - ]: 0 : Trace("dualLike") << "dualLike " << endl;
802 : :
803 : 0 : Assert(d_errorSet.noSignals());
804 : :
805 : 0 : WitnessImprovement w = AntiProductive;
806 : 0 : uint32_t prevFocusSize = d_focusSize;
807 : 0 : uint32_t prevErrorSize = d_errorSize;
808 : :
809 [ - - ]: 0 : if (d_focusSize == 0)
810 : : {
811 : 0 : Assert(d_errorSize == d_errorSet.errorSize());
812 : 0 : Assert(d_focusErrorVar == ARITHVAR_SENTINEL);
813 : :
814 : 0 : d_errorSet.blur();
815 : :
816 : 0 : d_focusSize = d_errorSet.focusSize();
817 : :
818 : 0 : Assert(d_errorSize == d_focusSize);
819 : 0 : Assert(d_errorSize >= 1);
820 : :
821 : 0 : d_focusErrorVar = constructInfeasiblityFunction(
822 : 0 : d_statistics.d_fcFocusConstructionTimer);
823 : :
824 [ - - ]: 0 : Trace("dualLike") << "blur " << d_focusSize << endl;
825 : : }
826 [ - - ]: 0 : else if (d_focusSize == 1)
827 : : {
828 : : // Possible outcomes:
829 : : // - errorSet size shrunk
830 : : // -- fixed v
831 : : // -- fixed something other than v
832 : : // - conflict
833 : : // - budget was exhausted
834 : :
835 : 0 : ArithVar e = d_errorSet.topFocusVariable();
836 [ - - ]: 0 : Trace("dualLike") << "primalImproveError " << e << endl;
837 : 0 : w = primalImproveError(e);
838 : : }
839 : : else
840 : : {
841 : : // Possible outcomes:
842 : : // - errorSet size shrunk
843 : : // -- fixed v
844 : : // -- fixed something other than v
845 : : // - conflict
846 : : // - budget was exhausted
847 : : // - focus went down
848 : 0 : Assert(d_focusSize > 1);
849 : 0 : ArithVar e = d_errorSet.topFocusVariable();
850 : : static constexpr unsigned s_sumMetricThreshold = 1;
851 [ - - ]: 0 : if (d_errorSet.sumMetric(e) <= s_sumMetricThreshold)
852 : : {
853 [ - - ]: 0 : Trace("dualLike") << "dualLikeImproveError " << e << endl;
854 : 0 : w = dualLikeImproveError(e);
855 : : }
856 : : else
857 : : {
858 [ - - ]: 0 : Trace("dualLike") << "selectFocusImproving " << endl;
859 : 0 : w = selectFocusImproving();
860 : : }
861 : : }
862 [ - - ]: 0 : Trace("dualLike") << "witnessImprovement: " << w << endl;
863 : 0 : Assert(d_focusSize == d_errorSet.focusSize());
864 : 0 : Assert(d_errorSize == d_errorSet.errorSize());
865 : :
866 : 0 : Assert(debugDualLike(w, Trace("dualLike"), prevFocusSize, prevErrorSize));
867 [ - - ]: 0 : Trace("dualLike") << "Focus size " << d_focusSize << " (was "
868 : 0 : << prevFocusSize << ")" << endl;
869 [ - - ]: 0 : Trace("dualLike") << "Error size " << d_errorSize << " (was "
870 : 0 : << prevErrorSize << ")" << endl;
871 : : }
872 : :
873 [ - - ]: 0 : if (d_focusErrorVar != ARITHVAR_SENTINEL)
874 : : {
875 : 0 : tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer,
876 : : d_focusErrorVar);
877 : 0 : d_focusErrorVar = ARITHVAR_SENTINEL;
878 : : }
879 : :
880 : 0 : Assert(d_focusErrorVar == ARITHVAR_SENTINEL);
881 [ - - ]: 0 : if (!d_conflictVariables.empty())
882 : : {
883 : 0 : return Result::UNSAT;
884 : : }
885 [ - - ]: 0 : else if (d_errorSet.errorEmpty())
886 : : {
887 : 0 : Assert(d_errorSet.noSignals());
888 : 0 : return Result::SAT;
889 : : }
890 : : else
891 : : {
892 : 0 : Assert(d_pivotBudget == 0);
893 : 0 : return Result::UNKNOWN;
894 : : }
895 : 0 : }
896 : :
897 : 0 : void FCSimplexDecisionProcedure::loadFocusSigns()
898 : : {
899 : 0 : Assert(d_focusCoefficients.empty());
900 : 0 : Assert(d_focusErrorVar != ARITHVAR_SENTINEL);
901 : 0 : for (Tableau::RowIterator ri = d_tableau.basicRowIterator(d_focusErrorVar);
902 [ - - ]: 0 : !ri.atEnd();
903 : 0 : ++ri)
904 : : {
905 : 0 : const Tableau::Entry& e = *ri;
906 : 0 : ArithVar curr = e.getColVar();
907 : 0 : d_focusCoefficients.set(curr, &e.getCoefficient());
908 : : }
909 : 0 : }
910 : :
911 : 0 : void FCSimplexDecisionProcedure::unloadFocusSigns()
912 : : {
913 : 0 : d_focusCoefficients.purge();
914 : 0 : }
915 : :
916 : 0 : const Rational& FCSimplexDecisionProcedure::focusCoefficient(ArithVar nb) const
917 : : {
918 [ - - ]: 0 : if (d_focusCoefficients.isKey(nb))
919 : : {
920 : 0 : return *(d_focusCoefficients[nb]);
921 : : }
922 : : else
923 : : {
924 : 0 : return d_zero;
925 : : }
926 : : }
927 : :
928 : : } // namespace arith::linear
929 : : } // namespace theory
930 : : } // namespace cvc5::internal
|
