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 provides a class for summarizing pivot proposals.
11 : : *
12 : : * This shares with the theory a Tableau, and a PartialModel that:
13 : : * - satisfies the equalities in the Tableau, and
14 : : * - the assignment for the non-basic variables satisfies their bounds.
15 : : * This maintains the relationship needed by the SimplexDecisionProcedure.
16 : : *
17 : : * In the language of Simplex for DPLL(T), this provides:
18 : : * - update()
19 : : * - pivotAndUpdate()
20 : : *
21 : : * This class also provides utility functions that require
22 : : * using both the Tableau and PartialModel.
23 : : */
24 : :
25 : : #include "cvc5_private.h"
26 : :
27 : : #pragma once
28 : :
29 : : #include <optional>
30 : :
31 : : #include "theory/arith/delta_rational.h"
32 : : #include "theory/arith/linear/arithvar.h"
33 : : #include "theory/arith/linear/constraint_forward.h"
34 : :
35 : : namespace cvc5::internal {
36 : : namespace theory {
37 : : namespace arith::linear {
38 : :
39 : : enum WitnessImprovement
40 : : {
41 : : ConflictFound = 0,
42 : : ErrorDropped = 1,
43 : : FocusImproved = 2,
44 : : FocusShrank = 3,
45 : : Degenerate = 4,
46 : : BlandsDegenerate = 5,
47 : : HeuristicDegenerate = 6,
48 : : AntiProductive = 7
49 : : };
50 : :
51 : 7918 : inline bool strongImprovement(WitnessImprovement w)
52 : : {
53 : 7918 : return w <= FocusImproved;
54 : : }
55 : :
56 : 23010 : inline bool improvement(WitnessImprovement w) { return w <= FocusShrank; }
57 : :
58 : 0 : inline bool degenerate(WitnessImprovement w)
59 : : {
60 [ - - ]: 0 : switch (w)
61 : : {
62 : 0 : case Degenerate:
63 : : case BlandsDegenerate:
64 : 0 : case HeuristicDegenerate: return true;
65 : 0 : default: return false;
66 : : }
67 : : }
68 : :
69 : : std::ostream& operator<<(std::ostream& out, WitnessImprovement w);
70 : :
71 : : /**
72 : : * This class summarizes both potential:
73 : : * - pivot-and-update operations or
74 : : * - a pure update operation.
75 : : * This stores enough information for the various algorithms hat consider these
76 : : * operations. These require slightly different pieces of information at
77 : : * different points so they are a bit verbose and paranoid.
78 : : */
79 : : class UpdateInfo
80 : : {
81 : : private:
82 : : /**
83 : : * The nonbasic variables under consideration.
84 : : * This is either the entering variable on a pivot and update
85 : : * or the variable being updated.
86 : : * This can only be set in the constructor or assignment.
87 : : *
88 : : * If this uninitialized, then this is ARITHVAR_SENTINEL.
89 : : */
90 : : ArithVar d_nonbasic;
91 : :
92 : : /**
93 : : * The sgn of the "intended" derivative (delta) of the update to d_nonbasic.
94 : : * This is either 1, -1, or 0.
95 : : * It is "intended" as the delta is always allowed to be 0.
96 : : * (See debugSgnAgreement().)
97 : : *
98 : : * If this uninitialized, then this is 0.
99 : : * If this is initialized, then it is -1 or 1.
100 : : *
101 : : * This can only be set in the constructor or assignment.
102 : : */
103 : : int d_nonbasicDirection;
104 : :
105 : : /**
106 : : * The change in the assignment of d_nonbasic.
107 : : * This is changed via the updateProposal(...) methods.
108 : : * The value needs to satisfy debugSgnAgreement() or it is in conflict.
109 : : */
110 : : std::optional<DeltaRational> d_nonbasicDelta;
111 : :
112 : : /**
113 : : * This is true if the pivot-and-update is *known* to cause a conflict.
114 : : * This can only be true if it was constructed through the static
115 : : * conflict(...) method.
116 : : */
117 : : bool d_foundConflict;
118 : :
119 : : /** This is the change in the size of the error set. */
120 : : std::optional<int> d_errorsChange;
121 : :
122 : : /** This is the sgn of the change in the value of the focus set.*/
123 : : std::optional<int> d_focusDirection;
124 : :
125 : : /** This is the sgn of the change in the value of the focus set.*/
126 : : std::optional<DeltaRational> d_focusChange;
127 : :
128 : : /** This is the coefficient in the tableau for the entry.*/
129 : : std::optional<const Rational*> d_tableauCoefficient;
130 : :
131 : : /**
132 : : * This is the constraint that nonbasic is basic is updating s.t. its variable
133 : : * is against it. This has 3 different possibilities:
134 : : * - Unbounded : then this is NullConstraint and unbounded() is true.
135 : : * - Pivot-And-Update: then this is not NullConstraint and the variable is not
136 : : * d_nonbasic.
137 : : * - Update: then this is not NullConstraint and the variable is d_nonbasic.
138 : : */
139 : : ConstraintP d_limiting;
140 : :
141 : : WitnessImprovement d_witness;
142 : :
143 : : /**
144 : : * This returns true if
145 : : * d_nonbasicDelta is zero() or its sgn() must agree with d_nonbasicDirection.
146 : : */
147 : 96275 : bool debugSgnAgreement() const
148 : : {
149 : 96275 : int deltaSgn = d_nonbasicDelta.value().sgn();
150 [ + + ][ + - ]: 96275 : return deltaSgn == 0 || deltaSgn == d_nonbasicDirection;
151 : : }
152 : :
153 : : /** This private constructor allows for setting conflict to true. */
154 : : UpdateInfo(bool conflict,
155 : : ArithVar nb,
156 : : const DeltaRational& delta,
157 : : const Rational& r,
158 : : ConstraintP lim);
159 : :
160 : : public:
161 : : /** This constructs an uninitialized UpdateInfo. */
162 : : UpdateInfo();
163 : :
164 : : /**
165 : : * This constructs an initialized UpdateInfo.
166 : : * dir must be 1 or -1.
167 : : */
168 : : UpdateInfo(ArithVar nb, int dir);
169 : :
170 : : /**
171 : : * This updates the nonBasicDelta to d and limiting to NullConstraint.
172 : : * This describes an unbounded() update.
173 : : */
174 : : void updateUnbounded(const DeltaRational& d, int ec, int f);
175 : :
176 : : void updatePureFocus(const DeltaRational& d, ConstraintP c);
177 : : // void updatePureError(const DeltaRational& d, Constraint c, int e);
178 : : // void updatePure(const DeltaRational& d, Constraint c, int e, int f);
179 : :
180 : : /**
181 : : * This updates the nonBasicDelta to d and limiting to c.
182 : : * This clears errorChange() and focusDir().
183 : : */
184 : : void updatePivot(const DeltaRational& d, ConstraintP c);
185 : :
186 : : /**
187 : : * This updates the nonBasicDelta to d, limiting to c, and errorChange to e.
188 : : * This clears focusDir().
189 : : */
190 : : void updatePivot(const DeltaRational& d,
191 : : const Rational& r,
192 : : ConstraintP c,
193 : : int e);
194 : :
195 : : /**
196 : : * This updates the nonBasicDelta to d, limiting to c, errorChange to e and
197 : : * focusDir to f.
198 : : */
199 : : void witnessedUpdate(const DeltaRational& d, ConstraintP c, int e, int f);
200 : : void update(
201 : : const DeltaRational& d, const Rational& r, ConstraintP c, int e, int f);
202 : :
203 : : static UpdateInfo conflict(ArithVar nb,
204 : : const DeltaRational& delta,
205 : : const Rational& r,
206 : : ConstraintP lim);
207 : :
208 : 506325 : inline ArithVar nonbasic() const { return d_nonbasic; }
209 : 72587 : inline bool uninitialized() const { return d_nonbasic == ARITHVAR_SENTINEL; }
210 : :
211 : : /**
212 : : * There is no limiting value to the improvement of the focus.
213 : : * If this is true, this never describes an update.
214 : : */
215 : 1392798 : inline bool unbounded() const { return d_limiting == NullConstraint; }
216 : :
217 : : /**
218 : : * The update either describes a pivotAndUpdate operation
219 : : * or it describes just an update.
220 : : */
221 : : bool describesPivot() const;
222 : :
223 : : /** Returns the . describesPivot() must be true. */
224 : : ArithVar leaving() const;
225 : :
226 : : /**
227 : : * Returns true if this is *known* to find a conflict.
228 : : * If true, this must have been made through the static conflict(...)
229 : : * function.
230 : : */
231 : 27 : bool foundConflict() const { return d_foundConflict; }
232 : :
233 : : /** Returns the direction nonbasic is supposed to move. */
234 : 106452 : inline int nonbasicDirection() const { return d_nonbasicDirection; }
235 : :
236 : : /** Requires errorsChange to be set through setErrorsChange or updateProposal.
237 : : */
238 : 88626 : inline int errorsChange() const { return d_errorsChange.value(); }
239 : :
240 : : /**
241 : : * If errorsChange has been set, return errorsChange().
242 : : * Otherwise, return def.
243 : : */
244 : 28322 : inline int errorsChangeSafe(int def) const
245 : : {
246 [ + - ]: 28322 : if (d_errorsChange)
247 : : {
248 : 28322 : return d_errorsChange.value();
249 : : }
250 : : else
251 : : {
252 : 0 : return def;
253 : : }
254 : : }
255 : :
256 : : /** Sets the errorChange. */
257 : : void setErrorsChange(int ec)
258 : : {
259 : : d_errorsChange = ec;
260 : : updateWitness();
261 : : }
262 : :
263 : : /** Requires errorsChange to be set through setErrorsChange or updateProposal.
264 : : */
265 : 65524 : inline int focusDirection() const { return d_focusDirection.value(); }
266 : :
267 : : /** Sets the focusDirection. */
268 : : void setFocusDirection(int fd)
269 : : {
270 : : Assert(-1 <= fd && fd <= 1);
271 : : d_focusDirection = fd;
272 : : updateWitness();
273 : : }
274 : :
275 : : /**
276 : : * nonbasicDirection must be the same as the sign for the focus function's
277 : : * coefficient for this to be safe.
278 : : * The burden for this being safe is on the user!
279 : : */
280 : : void determineFocusDirection()
281 : : {
282 : : const int deltaSgn = d_nonbasicDelta.value().sgn();
283 : : setFocusDirection(deltaSgn * d_nonbasicDirection);
284 : : }
285 : :
286 : : /** Requires nonbasicDelta to be set through updateProposal(...). */
287 : 139 : const DeltaRational& nonbasicDelta() const { return d_nonbasicDelta.value(); }
288 : 106452 : const Rational& getCoefficient() const
289 : : {
290 [ - + ][ - + ]: 106452 : Assert(describesPivot());
[ - - ]
291 [ - + ][ - + ]: 106452 : Assert(d_tableauCoefficient.value() != nullptr);
[ - - ]
292 : 106452 : return *(d_tableauCoefficient.value());
293 : : }
294 : : int basicDirection() const
295 : : {
296 : : return nonbasicDirection() * (getCoefficient().sgn());
297 : : }
298 : :
299 : : /** Returns the limiting constraint. */
300 : 114231 : inline ConstraintP limiting() const { return d_limiting; }
301 : :
302 : 214172 : WitnessImprovement getWitness(bool useBlands = false) const
303 : : {
304 [ - + ][ - + ]: 214172 : Assert(d_witness == computeWitness());
[ - - ]
305 : :
306 [ + + ]: 214172 : if (d_witness == Degenerate)
307 : : {
308 [ - + ]: 83226 : if (useBlands)
309 : : {
310 : 0 : return BlandsDegenerate;
311 : : }
312 : : else
313 : : {
314 : 83226 : return HeuristicDegenerate;
315 : : }
316 : : }
317 : : else
318 : : {
319 : 130946 : return d_witness;
320 : : }
321 : : }
322 : :
323 : : const DeltaRational& focusChange() const { return d_focusChange.value(); }
324 : : void setFocusChange(const DeltaRational& fc) { d_focusChange = fc; }
325 : :
326 : : /** Outputs the UpdateInfo into out. */
327 : : void output(std::ostream& out) const;
328 : :
329 : : private:
330 : 96275 : void updateWitness()
331 : : {
332 : 96275 : d_witness = computeWitness();
333 [ + + ][ + - ]: 96275 : Assert(describesPivot() || improvement(d_witness));
[ - + ][ - + ]
[ - - ]
334 : 96275 : }
335 : :
336 : : /**
337 : : * Determines the appropriate WitnessImprovement for the update.
338 : : * useBlands breaks ties for degenerate pivots.
339 : : *
340 : : * This is safe if:
341 : : * - d_foundConflict is true, or
342 : : * - d_foundConflict is false and d_errorsChange has been set and
343 : : * d_errorsChange < 0, or
344 : : * - d_foundConflict is false and d_errorsChange has been set and
345 : : * d_errorsChange >= 0 and d_focusDirection has been set.
346 : : */
347 : 310447 : WitnessImprovement computeWitness() const
348 : : {
349 [ + + ]: 310447 : if (d_foundConflict)
350 : : {
351 : 81 : return ConflictFound;
352 : : }
353 [ + - ][ + + ]: 310366 : else if (d_errorsChange && d_errorsChange.value() < 0)
[ + + ]
354 : : {
355 : 145352 : return ErrorDropped;
356 : : }
357 [ + + ]: 165014 : else if (d_errorsChange.value_or(0) == 0)
358 : : {
359 [ + - ]: 160948 : if (d_focusDirection)
360 : : {
361 [ + + ]: 160948 : if (*d_focusDirection > 0)
362 : : {
363 : 36997 : return FocusImproved;
364 : : }
365 [ + + ]: 123951 : else if (*d_focusDirection == 0)
366 : : {
367 : 123873 : return Degenerate;
368 : : }
369 : : }
370 : : }
371 : 4144 : return AntiProductive;
372 : : }
373 : : };
374 : :
375 : : std::ostream& operator<<(std::ostream& out, const UpdateInfo& up);
376 : :
377 : : } // namespace arith::linear
378 : : } // namespace theory
379 : : } // namespace cvc5::internal
|
