Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/simplex_update.h	Lines:	0	57	0.0 %
Date:	2021-05-22	Branches:	0	102	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * This provides a class for summarizing pivot proposals.
 *
 * This shares with the theory a Tableau, and a PartialModel that:
 *  - satisfies the equalities in the Tableau, and
 *  - the assignment for the non-basic variables satisfies their bounds.
 * This maintains the relationship needed by the SimplexDecisionProcedure.
 *
 * In the language of Simplex for DPLL(T), this provides:
 * - update()
 * - pivotAndUpdate()
 *
 * This class also provides utility functions that require
 * using both the Tableau and PartialModel.
 */

#include "cvc5_private.h"

#pragma once

#include "theory/arith/delta_rational.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/constraint_forward.h"
#include "util/maybe.h"

namespace cvc5 {
namespace theory {
namespace arith {

enum WitnessImprovement {
  ConflictFound = 0,
  ErrorDropped = 1,
  FocusImproved = 2,
  FocusShrank = 3,
  Degenerate = 4,
  BlandsDegenerate = 5,
  HeuristicDegenerate = 6,
  AntiProductive = 7
};

inline bool strongImprovement(WitnessImprovement w){
  return w <= FocusImproved;
}

inline bool improvement(WitnessImprovement w){
  return w <= FocusShrank;
}

inline bool degenerate(WitnessImprovement w){
  switch(w){
  case Degenerate:
  case BlandsDegenerate:
  case HeuristicDegenerate:
    return true;
  default:
    return false;
  }
}

std::ostream& operator<<(std::ostream& out,  WitnessImprovement w);

/**
 * This class summarizes both potential:
 * - pivot-and-update operations or
 * - a pure update operation.
 * This stores enough information for the various algorithms  hat consider these operations.
 * These require slightly different pieces of information at different points
 * so they are a bit verbose and paranoid.
 */
class UpdateInfo {
private:

  /**
   * The nonbasic variables under consideration.
   * This is either the entering variable on a pivot and update
   * or the variable being updated.
   * This can only be set in the constructor or assignment.
   *
   * If this uninitialized, then this is ARITHVAR_SENTINEL.
   */
  ArithVar d_nonbasic;

  /**
   * The sgn of the "intended" derivative (delta) of the update to d_nonbasic.
   * This is either 1, -1, or 0.
   * It is "intended" as the delta is always allowed to be 0.
   * (See debugSgnAgreement().)
   *
   * If this uninitialized, then this is 0.
   * If this is initialized, then it is -1 or 1.
   *
   * This can only be set in the constructor or assignment.
   */
  int d_nonbasicDirection;

  /**
   * The change in the assignment of d_nonbasic.
   * This is changed via the updateProposal(...) methods.
   * The value needs to satisfy debugSgnAgreement() or it is in conflict.
   */
  Maybe<DeltaRational> d_nonbasicDelta;

  /**
   * This is true if the pivot-and-update is *known* to cause a conflict.
   * This can only be true if it was constructed through the static conflict(...) method.
   */
  bool d_foundConflict;

  /** This is the change in the size of the error set. */
  Maybe<int> d_errorsChange;

  /** This is the sgn of the change in the value of the focus set.*/
  Maybe<int> d_focusDirection;

  /** This is the sgn of the change in the value of the focus set.*/
  Maybe<DeltaRational> d_focusChange;

  /** This is the coefficient in the tableau for the entry.*/
  Maybe<const Rational*> d_tableauCoefficient;

  /**
   * This is the constraint that nonbasic is basic is updating s.t. its variable is against it.
   * This has 3 different possibilities:
   * - Unbounded : then this is NullConstraint and unbounded() is true.
   * - Pivot-And-Update: then this is not NullConstraint and the variable is not d_nonbasic.
   * - Update: then this is not NullConstraint and the variable is d_nonbasic.
   */
  ConstraintP d_limiting;

  WitnessImprovement d_witness;

  /**
   * This returns true if
   * d_nonbasicDelta is zero() or its sgn() must agree with d_nonbasicDirection.
   */
  bool debugSgnAgreement() const {
    int deltaSgn = d_nonbasicDelta.value().sgn();
    return deltaSgn == 0 || deltaSgn == d_nonbasicDirection;
  }

  /** This private constructor allows for setting conflict to true. */
  UpdateInfo(bool conflict, ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP lim);

public:

  /** This constructs an uninitialized UpdateInfo. */
  UpdateInfo();

  /**
   * This constructs an initialized UpdateInfo.
   * dir must be 1 or -1.
   */
  UpdateInfo(ArithVar nb, int dir);

  /**
   * This updates the nonBasicDelta to d and limiting to NullConstraint.
   * This describes an unbounded() update.
   */
  void updateUnbounded(const DeltaRational& d, int ec, int f);


  void updatePureFocus(const DeltaRational& d, ConstraintP c);
  //void updatePureError(const DeltaRational& d, Constraint c, int e);
  //void updatePure(const DeltaRational& d, Constraint c, int e, int f);

  /**
   * This updates the nonBasicDelta to d and limiting to c.
   * This clears errorChange() and focusDir().
   */
  void updatePivot(const DeltaRational& d, const Rational& r,  ConstraintP c);

  /**
   * This updates the nonBasicDelta to d, limiting to c, and errorChange to e.
   * This clears focusDir().
   */
  void updatePivot(const DeltaRational& d, const Rational& r, ConstraintP c, int e);

  /**
   * This updates the nonBasicDelta to d, limiting to c, errorChange to e and
   * focusDir to f.
   */
  void witnessedUpdate(const DeltaRational& d, ConstraintP c, int e, int f);
  void update(const DeltaRational& d, const Rational& r, ConstraintP c, int e, int f);


  static UpdateInfo conflict(ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP lim);

  inline ArithVar nonbasic() const { return d_nonbasic; }
  inline bool uninitialized() const {
    return d_nonbasic == ARITHVAR_SENTINEL;
  }

  /**
   * There is no limiting value to the improvement of the focus.
   * If this is true, this never describes an update.
   */
  inline bool unbounded() const {
    return d_limiting == NullConstraint;
  }

  /**
   * The update either describes a pivotAndUpdate operation
   * or it describes just an update.
   */
  bool describesPivot() const;

  /** Returns the . describesPivot() must be true. */
  ArithVar leaving() const;

  /**
   * Returns true if this is *known* to find a conflict.
   * If true, this must have been made through the static conflict(...) function.
   */
  bool foundConflict() const { return d_foundConflict; }

  /** Returns the direction nonbasic is supposed to move. */
  inline int nonbasicDirection() const{  return d_nonbasicDirection; }

  /** Requires errorsChange to be set through setErrorsChange or updateProposal. */
  inline int errorsChange() const { return d_errorsChange.value(); }

  /**
   * If errorsChange has been set, return errorsChange().
   * Otherwise, return def.
   */
  inline int errorsChangeSafe(int def) const {
    if (d_errorsChange)
    {
      return d_errorsChange.value();
    }
    else
    {
      return def;
    }
  }

  /** Sets the errorChange. */
  void setErrorsChange(int ec){
    d_errorsChange = ec;
    updateWitness();
  }


  /** Requires errorsChange to be set through setErrorsChange or updateProposal. */
  inline int focusDirection() const { return d_focusDirection.value(); }

  /** Sets the focusDirection. */
  void setFocusDirection(int fd){
    Assert(-1 <= fd && fd <= 1);
    d_focusDirection = fd;
    updateWitness();
  }

  /**
   * nonbasicDirection must be the same as the sign for the focus function's
   * coefficient for this to be safe.
   * The burden for this being safe is on the user!
   */
  void determineFocusDirection(){
    const int deltaSgn = d_nonbasicDelta.value().sgn();
    setFocusDirection(deltaSgn * d_nonbasicDirection);
  }

  /** Requires nonbasicDelta to be set through updateProposal(...). */
  const DeltaRational& nonbasicDelta() const { return d_nonbasicDelta.value(); }
  const Rational& getCoefficient() const {
    Assert(describesPivot());
    Assert(d_tableauCoefficient.value() != NULL);
    return *(d_tableauCoefficient.value());
  }
  int basicDirection() const {
    return nonbasicDirection() * (getCoefficient().sgn());
  }

  /** Returns the limiting constraint. */
  inline ConstraintP limiting() const {
    return d_limiting;
  }

  WitnessImprovement getWitness(bool useBlands = false) const{
    Assert(d_witness == computeWitness());

    if(d_witness == Degenerate){
      if(useBlands){
        return BlandsDegenerate;
      }else{
        return HeuristicDegenerate;
      }
    }else{
      return d_witness;
    }
  }

  const DeltaRational& focusChange() const { return d_focusChange.value(); }
  void setFocusChange(const DeltaRational& fc) {
    d_focusChange = fc;
  }

  /** Outputs the UpdateInfo into out. */
  void output(std::ostream& out) const;

private:
  void updateWitness() {
    d_witness = computeWitness();
    Assert(describesPivot() || improvement(d_witness));
  }

  /**
   * Determines the appropriate WitnessImprovement for the update.
   * useBlands breaks ties for degenerate pivots.
   *
   * This is safe if:
   * - d_foundConflict is true, or
   * - d_foundConflict is false and d_errorsChange has been set and d_errorsChange < 0, or
   * - d_foundConflict is false and d_errorsChange has been set and d_errorsChange >= 0 and d_focusDirection has been set.
   */
  WitnessImprovement computeWitness() const {
    if(d_foundConflict){
      return ConflictFound;
    }
    else if (d_errorsChange.just() && d_errorsChange.value() < 0)
    {
      return ErrorDropped;
    }
    else if (d_errorsChange.nothing() || d_errorsChange.value() == 0)
    {
      if(d_focusDirection.just()){
        if (d_focusDirection.value() > 0)
        {
          return FocusImproved;
        }
        else if (d_focusDirection.value() == 0)
        {
          return Degenerate;
        }
      }
    }
    return AntiProductive;
  }

};

std::ostream& operator<<(std::ostream& out, const UpdateInfo& up);

}  // namespace arith
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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