1 /********************* */
2 /*! \file linear_equality.h
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): mdeters
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief This provides a class for summarizing pivot proposals.
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.
19 ** In the language of Simplex for DPLL(T), this provides:
23 ** This class also provides utility functions that require
24 ** using both the Tableau and PartialModel.
28 #include "cvc4_private.h"
32 #include "theory/arith/delta_rational.h"
33 #include "theory/arith/arithvar.h"
34 #include "theory/arith/constraint_forward.h"
35 #include "util/maybe.h"
41 enum WitnessImprovement
{
48 HeuristicDegenerate
= 6,
52 inline bool strongImprovement(WitnessImprovement w
){
53 return w
<= FocusImproved
;
56 inline bool improvement(WitnessImprovement w
){
57 return w
<= FocusShrank
;
60 inline bool degenerate(WitnessImprovement w
){
63 case BlandsDegenerate
:
64 case HeuristicDegenerate
:
71 std::ostream
& operator<<(std::ostream
& out
, WitnessImprovement w
);
74 * This class summarizes both potential:
75 * - pivot-and-update operations or
76 * - a pure update operation.
77 * This stores enough information for the various algorithms hat consider these operations.
78 * These require slightly different pieces of information at different points
79 * so they are a bit verbose and paranoid.
85 * The nonbasic variables under consideration.
86 * This is either the entering variable on a pivot and update
87 * or the variable being updated.
88 * This can only be set in the constructor or assignment.
90 * If this uninitialized, then this is ARITHVAR_SENTINEL.
95 * The sgn of the "intended" derivative (delta) of the update to d_nonbasic.
96 * This is either 1, -1, or 0.
97 * It is "intended" as the delta is always allowed to be 0.
98 * (See debugSgnAgreement().)
100 * If this uninitialized, then this is 0.
101 * If this is initialized, then it is -1 or 1.
103 * This can only be set in the constructor or assignment.
105 int d_nonbasicDirection
;
108 * The change in the assignment of d_nonbasic.
109 * This is changed via the updateProposal(...) methods.
110 * The value needs to satisfy debugSgnAgreement() or it is in conflict.
112 Maybe
<DeltaRational
> d_nonbasicDelta
;
115 * This is true if the pivot-and-update is *known* to cause a conflict.
116 * This can only be true if it was constructed through the static conflict(...) method.
118 bool d_foundConflict
;
120 /** This is the change in the size of the error set. */
121 Maybe
<int> d_errorsChange
;
123 /** This is the sgn of the change in the value of the focus set.*/
124 Maybe
<int> d_focusDirection
;
126 /** This is the sgn of the change in the value of the focus set.*/
127 Maybe
<DeltaRational
> d_focusChange
;
129 /** This is the coefficient in the tableau for the entry.*/
130 Maybe
<const Rational
*> d_tableauCoefficient
;
133 * This is the constraint that nonbasic is basic is updating s.t. its variable is against it.
134 * This has 3 different possibilities:
135 * - Unbounded : then this is NullConstraint and unbounded() is true.
136 * - Pivot-And-Update: then this is not NullConstraint and the variable is not d_nonbasic.
137 * - Update: then this is not NullConstraint and the variable is d_nonbasic.
139 Constraint d_limiting
;
141 WitnessImprovement d_witness
;
144 * This returns true if
145 * d_nonbasicDelta is zero() or its sgn() must agree with d_nonbasicDirection.
147 bool debugSgnAgreement() const {
148 int deltaSgn
= d_nonbasicDelta
.constValue().sgn();
149 return deltaSgn
== 0 || deltaSgn
== d_nonbasicDirection
;
152 /** This private constructor allows for setting conflict to true. */
153 UpdateInfo(bool conflict
, ArithVar nb
, const DeltaRational
& delta
, const Rational
& r
, Constraint lim
);
157 /** This constructs an uninitialized UpdateInfo. */
161 * This constructs an initialized UpdateInfo.
162 * dir must be 1 or -1.
164 UpdateInfo(ArithVar nb
, int dir
);
167 * This updates the nonBasicDelta to d and limiting to NullConstraint.
168 * This describes an unbounded() update.
170 void updateUnbounded(const DeltaRational
& d
, int ec
, int f
);
173 void updatePureFocus(const DeltaRational
& d
, Constraint c
);
174 //void updatePureError(const DeltaRational& d, Constraint c, int e);
175 //void updatePure(const DeltaRational& d, Constraint c, int e, int f);
178 * This updates the nonBasicDelta to d and limiting to c.
179 * This clears errorChange() and focusDir().
181 void updatePivot(const DeltaRational
& d
, const Rational
& r
, Constraint c
);
184 * This updates the nonBasicDelta to d, limiting to c, and errorChange to e.
185 * This clears focusDir().
187 void updatePivot(const DeltaRational
& d
, const Rational
& r
, Constraint c
, int e
);
190 * This updates the nonBasicDelta to d, limiting to c, errorChange to e and
193 void witnessedUpdate(const DeltaRational
& d
, Constraint c
, int e
, int f
);
194 void update(const DeltaRational
& d
, const Rational
& r
, Constraint c
, int e
, int f
);
197 static UpdateInfo
conflict(ArithVar nb
, const DeltaRational
& delta
, const Rational
& r
, Constraint lim
);
199 inline ArithVar
nonbasic() const { return d_nonbasic
; }
200 inline bool uninitialized() const {
201 return d_nonbasic
== ARITHVAR_SENTINEL
;
205 * There is no limiting value to the improvement of the focus.
206 * If this is true, this never describes an update.
208 inline bool unbounded() const {
209 return d_limiting
== NullConstraint
;
213 * The update either describes a pivotAndUpdate operation
214 * or it describes just an update.
216 bool describesPivot() const;
218 /** Returns the . describesPivot() must be true. */
219 ArithVar
leaving() const;
222 * Returns true if this is *known* to find a conflict.
223 * If true, this must have been made through the static conflict(...) function.
225 bool foundConflict() const { return d_foundConflict
; }
227 /** Returns the direction nonbasic is supposed to move. */
228 inline int nonbasicDirection() const{ return d_nonbasicDirection
; }
230 /** Requires errorsChange to be set through setErrorsChange or updateProposal. */
231 inline int errorsChange() const { return d_errorsChange
; }
234 * If errorsChange has been set, return errorsChange().
235 * Otherwise, return def.
237 inline int errorsChangeSafe(int def
) const {
238 if(d_errorsChange
.just()){
239 return d_errorsChange
;
245 /** Sets the errorChange. */
246 void setErrorsChange(int ec
){
252 /** Requires errorsChange to be set through setErrorsChange or updateProposal. */
253 inline int focusDirection() const{ return d_focusDirection
; }
255 /** Sets the focusDirection. */
256 void setFocusDirection(int fd
){
257 Assert(-1 <= fd
&& fd
<= 1);
258 d_focusDirection
= fd
;
263 * nonbasicDirection must be the same as the sign for the focus function's
264 * coefficient for this to be safe.
265 * The burden for this being safe is on the user!
267 void determineFocusDirection(){
268 int deltaSgn
= d_nonbasicDelta
.constValue().sgn();
269 setFocusDirection(deltaSgn
* d_nonbasicDirection
);
272 /** Requires nonbasicDelta to be set through updateProposal(...). */
273 const DeltaRational
& nonbasicDelta() const {
274 return d_nonbasicDelta
;
276 const Rational
& getCoefficient() const {
277 Assert(describesPivot());
278 Assert(d_tableauCoefficient
.constValue() != NULL
);
279 return *(d_tableauCoefficient
.constValue());
281 int basicDirection() const {
282 return nonbasicDirection() * (getCoefficient().sgn());
285 /** Returns the limiting constraint. */
286 inline Constraint
limiting() const {
290 WitnessImprovement
getWitness(bool useBlands
= false) const{
291 Assert(d_witness
== computeWitness());
293 if(d_witness
== Degenerate
){
295 return BlandsDegenerate
;
297 return HeuristicDegenerate
;
304 const DeltaRational
& focusChange() const {
305 return d_focusChange
;
307 void setFocusChange(const DeltaRational
& fc
) {
311 /** Outputs the UpdateInfo into out. */
312 void output(std::ostream
& out
) const;
315 void updateWitness() {
316 d_witness
= computeWitness();
317 Assert(describesPivot() || improvement(d_witness
));
321 * Determines the appropraite WitnessImprovement for the update.
322 * useBlands breaks ties for degenerate pivots.
325 * - d_foundConflict is true, or
326 * - d_foundConflict is false and d_errorsChange has been set and d_errorsChange < 0, or
327 * - d_foundConflict is false and d_errorsChange has been set and d_errorsChange >= 0 and d_focusDirection has been set.
329 WitnessImprovement
computeWitness() const {
331 return ConflictFound
;
332 }else if(d_errorsChange
.just() && d_errorsChange
< 0){
334 }else if(d_errorsChange
.nothing() || d_errorsChange
== 0){
335 if(d_focusDirection
.just()){
336 if(d_focusDirection
> 0){
337 return FocusImproved
;
338 }else if(d_focusDirection
== 0){
343 return AntiProductive
;
348 std::ostream
& operator<<(std::ostream
& out
, const UpdateInfo
& up
);
350 }/* CVC4::theory::arith namespace */
351 }/* CVC4::theory namespace */
352 }/* CVC4 namespace */