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