GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/simplex_update.h Lines: 0 57 0.0 %
Date: 2021-03-23 Branches: 0 102 0.0 %

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