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/linear/arithvar.h"
32 : : #include "theory/arith/linear/constraint_forward.h"
33 : : #include "theory/arith/delta_rational.h"
34 : :
35 : : namespace cvc5::internal {
36 : : namespace theory {
37 : : namespace arith::linear {
38 : :
39 : : enum WitnessImprovement {
40 : : ConflictFound = 0,
41 : : ErrorDropped = 1,
42 : : FocusImproved = 2,
43 : : FocusShrank = 3,
44 : : Degenerate = 4,
45 : : BlandsDegenerate = 5,
46 : : HeuristicDegenerate = 6,
47 : : AntiProductive = 7
48 : : };
49 : :
50 : 7410 : inline bool strongImprovement(WitnessImprovement w){
51 : 7410 : return w <= FocusImproved;
52 : : }
53 : :
54 : 21436 : inline bool improvement(WitnessImprovement w){
55 : 21436 : return w <= FocusShrank;
56 : : }
57 : :
58 : 0 : inline bool degenerate(WitnessImprovement w){
59 [ - - ]: 0 : switch(w){
60 : 0 : case Degenerate:
61 : : case BlandsDegenerate:
62 : : case HeuristicDegenerate:
63 : 0 : return true;
64 : 0 : default:
65 : 0 : 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 operations.
76 : : * These require slightly different pieces of information at different points
77 : : * so they are a bit verbose and paranoid.
78 : : */
79 : : class UpdateInfo {
80 : : private:
81 : :
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 conflict(...) method.
115 : : */
116 : : bool d_foundConflict;
117 : :
118 : : /** This is the change in the size of the error set. */
119 : : std::optional<int> d_errorsChange;
120 : :
121 : : /** This is the sgn of the change in the value of the focus set.*/
122 : : std::optional<int> d_focusDirection;
123 : :
124 : : /** This is the sgn of the change in the value of the focus set.*/
125 : : std::optional<DeltaRational> d_focusChange;
126 : :
127 : : /** This is the coefficient in the tableau for the entry.*/
128 : : std::optional<const Rational*> d_tableauCoefficient;
129 : :
130 : : /**
131 : : * This is the constraint that nonbasic is basic is updating s.t. its variable is against it.
132 : : * This has 3 different possibilities:
133 : : * - Unbounded : then this is NullConstraint and unbounded() is true.
134 : : * - Pivot-And-Update: then this is not NullConstraint and the variable is not d_nonbasic.
135 : : * - Update: then this is not NullConstraint and the variable is d_nonbasic.
136 : : */
137 : : ConstraintP d_limiting;
138 : :
139 : : WitnessImprovement d_witness;
140 : :
141 : : /**
142 : : * This returns true if
143 : : * d_nonbasicDelta is zero() or its sgn() must agree with d_nonbasicDirection.
144 : : */
145 : 82931 : bool debugSgnAgreement() const {
146 : 82931 : int deltaSgn = d_nonbasicDelta.value().sgn();
147 [ + + ][ + - ]: 82931 : return deltaSgn == 0 || deltaSgn == d_nonbasicDirection;
148 : : }
149 : :
150 : : /** This private constructor allows for setting conflict to true. */
151 : : UpdateInfo(bool conflict, ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP lim);
152 : :
153 : : public:
154 : :
155 : : /** This constructs an uninitialized UpdateInfo. */
156 : : UpdateInfo();
157 : :
158 : : /**
159 : : * This constructs an initialized UpdateInfo.
160 : : * dir must be 1 or -1.
161 : : */
162 : : UpdateInfo(ArithVar nb, int dir);
163 : :
164 : : /**
165 : : * This updates the nonBasicDelta to d and limiting to NullConstraint.
166 : : * This describes an unbounded() update.
167 : : */
168 : : void updateUnbounded(const DeltaRational& d, int ec, int f);
169 : :
170 : :
171 : : void updatePureFocus(const DeltaRational& d, ConstraintP c);
172 : : //void updatePureError(const DeltaRational& d, Constraint c, int e);
173 : : //void updatePure(const DeltaRational& d, Constraint c, int e, int f);
174 : :
175 : : /**
176 : : * This updates the nonBasicDelta to d and limiting to c.
177 : : * This clears errorChange() and focusDir().
178 : : */
179 : : void updatePivot(const DeltaRational& d, ConstraintP c);
180 : :
181 : : /**
182 : : * This updates the nonBasicDelta to d, limiting to c, and errorChange to e.
183 : : * This clears focusDir().
184 : : */
185 : : void updatePivot(const DeltaRational& d, const Rational& r, ConstraintP c, int e);
186 : :
187 : : /**
188 : : * This updates the nonBasicDelta to d, limiting to c, errorChange to e and
189 : : * focusDir to f.
190 : : */
191 : : void witnessedUpdate(const DeltaRational& d, ConstraintP c, int e, int f);
192 : : void update(const DeltaRational& d, const Rational& r, ConstraintP c, int e, int f);
193 : :
194 : :
195 : : static UpdateInfo conflict(ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP lim);
196 : :
197 : 422088 : inline ArithVar nonbasic() const { return d_nonbasic; }
198 : 66728 : inline bool uninitialized() const {
199 : 66728 : return d_nonbasic == ARITHVAR_SENTINEL;
200 : : }
201 : :
202 : : /**
203 : : * There is no limiting value to the improvement of the focus.
204 : : * If this is true, this never describes an update.
205 : : */
206 : 1154499 : inline bool unbounded() const {
207 : 1154499 : return d_limiting == NullConstraint;
208 : : }
209 : :
210 : : /**
211 : : * The update either describes a pivotAndUpdate operation
212 : : * or it describes just an update.
213 : : */
214 : : bool describesPivot() const;
215 : :
216 : : /** Returns the . describesPivot() must be true. */
217 : : ArithVar leaving() const;
218 : :
219 : : /**
220 : : * Returns true if this is *known* to find a conflict.
221 : : * If true, this must have been made through the static conflict(...) function.
222 : : */
223 : 67 : bool foundConflict() const { return d_foundConflict; }
224 : :
225 : : /** Returns the direction nonbasic is supposed to move. */
226 : 87236 : inline int nonbasicDirection() const{ return d_nonbasicDirection; }
227 : :
228 : : /** Requires errorsChange to be set through setErrorsChange or updateProposal. */
229 : 78667 : inline int errorsChange() const { return d_errorsChange.value(); }
230 : :
231 : : /**
232 : : * If errorsChange has been set, return errorsChange().
233 : : * Otherwise, return def.
234 : : */
235 : 25868 : inline int errorsChangeSafe(int def) const {
236 [ + - ]: 25868 : if (d_errorsChange)
237 : : {
238 : 25868 : return d_errorsChange.value();
239 : : }
240 : : else
241 : : {
242 : 0 : return def;
243 : : }
244 : : }
245 : :
246 : : /** Sets the errorChange. */
247 : : void setErrorsChange(int ec){
248 : : d_errorsChange = ec;
249 : : updateWitness();
250 : : }
251 : :
252 : :
253 : : /** Requires errorsChange to be set through setErrorsChange or updateProposal. */
254 : 50459 : inline int focusDirection() const { return d_focusDirection.value(); }
255 : :
256 : : /** Sets the focusDirection. */
257 : : void setFocusDirection(int fd){
258 : : Assert(-1 <= fd && fd <= 1);
259 : : d_focusDirection = fd;
260 : : updateWitness();
261 : : }
262 : :
263 : : /**
264 : : * nonbasicDirection must be the same as the sign for the focus function's
265 : : * coefficient for this to be safe.
266 : : * The burden for this being safe is on the user!
267 : : */
268 : : void determineFocusDirection(){
269 : : const int deltaSgn = d_nonbasicDelta.value().sgn();
270 : : setFocusDirection(deltaSgn * d_nonbasicDirection);
271 : : }
272 : :
273 : : /** Requires nonbasicDelta to be set through updateProposal(...). */
274 : 134 : const DeltaRational& nonbasicDelta() const { return d_nonbasicDelta.value(); }
275 : 87236 : const Rational& getCoefficient() const {
276 [ - + ][ - + ]: 87236 : Assert(describesPivot());
[ - - ]
277 [ - + ][ - + ]: 87236 : Assert(d_tableauCoefficient.value() != NULL);
[ - - ]
278 : 87236 : return *(d_tableauCoefficient.value());
279 : : }
280 : : int basicDirection() const {
281 : : return nonbasicDirection() * (getCoefficient().sgn());
282 : : }
283 : :
284 : : /** Returns the limiting constraint. */
285 : 94512 : inline ConstraintP limiting() const {
286 : 94512 : return d_limiting;
287 : : }
288 : :
289 : 185540 : WitnessImprovement getWitness(bool useBlands = false) const{
290 [ - + ][ - + ]: 185540 : Assert(d_witness == computeWitness());
[ - - ]
291 : :
292 [ + + ]: 185540 : if(d_witness == Degenerate){
293 [ - + ]: 65036 : if(useBlands){
294 : 0 : return BlandsDegenerate;
295 : : }else{
296 : 65036 : return HeuristicDegenerate;
297 : : }
298 : : }else{
299 : 120504 : return d_witness;
300 : : }
301 : : }
302 : :
303 : : const DeltaRational& focusChange() const { return d_focusChange.value(); }
304 : : void setFocusChange(const DeltaRational& fc) {
305 : : d_focusChange = fc;
306 : : }
307 : :
308 : : /** Outputs the UpdateInfo into out. */
309 : : void output(std::ostream& out) const;
310 : :
311 : : private:
312 : 82931 : void updateWitness() {
313 : 82931 : d_witness = computeWitness();
314 [ + + ][ + - ]: 82931 : Assert(describesPivot() || improvement(d_witness));
[ - + ][ - + ]
[ - - ]
315 : 82931 : }
316 : :
317 : : /**
318 : : * Determines the appropriate WitnessImprovement for the update.
319 : : * useBlands breaks ties for degenerate pivots.
320 : : *
321 : : * This is safe if:
322 : : * - d_foundConflict is true, or
323 : : * - d_foundConflict is false and d_errorsChange has been set and d_errorsChange < 0, or
324 : : * - d_foundConflict is false and d_errorsChange has been set and d_errorsChange >= 0 and d_focusDirection has been set.
325 : : */
326 : 268471 : WitnessImprovement computeWitness() const {
327 [ + + ]: 268471 : if(d_foundConflict){
328 : 211 : return ConflictFound;
329 : : }
330 [ + - ][ + + ]: 268260 : else if (d_errorsChange && d_errorsChange.value() < 0)
[ + + ]
331 : : {
332 : 128790 : return ErrorDropped;
333 : : }
334 [ + + ]: 139470 : else if (d_errorsChange.value_or(0) == 0)
335 : : {
336 [ + - ]: 134744 : if (d_focusDirection)
337 : : {
338 [ + + ]: 134744 : if (*d_focusDirection > 0)
339 : : {
340 : 37753 : return FocusImproved;
341 : : }
342 [ + + ]: 96991 : else if (*d_focusDirection == 0)
343 : : {
344 : 96853 : return Degenerate;
345 : : }
346 : : }
347 : : }
348 : 4864 : return AntiProductive;
349 : : }
350 : :
351 : : };
352 : :
353 : : std::ostream& operator<<(std::ostream& out, const UpdateInfo& up);
354 : :
355 : : } // namespace arith
356 : : } // namespace theory
357 : : } // namespace cvc5::internal
|
