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