Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/bound_counts.h	Lines:	83	97	85.6 %
Date:	2021-09-19	Branches:	48	162	29.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Clark Barrett
 *
 * 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "cvc5_private.h"
#pragma once

#include "base/check.h"
#include "theory/arith/arithvar.h"
#include "util/dense_map.h"

namespace cvc5 {
namespace theory {
namespace arith {

class BoundCounts {
private:
  uint32_t d_lowerBoundCount;
  uint32_t d_upperBoundCount;

public:
  BoundCounts() : d_lowerBoundCount(0), d_upperBoundCount(0) {}
  BoundCounts(uint32_t lbs, uint32_t ubs)
  : d_lowerBoundCount(lbs), d_upperBoundCount(ubs) {}

  bool operator==(BoundCounts bc) const {
    return d_lowerBoundCount == bc.d_lowerBoundCount
      && d_upperBoundCount == bc.d_upperBoundCount;
  }
  bool operator!=(BoundCounts bc) const {
    return  d_lowerBoundCount != bc.d_lowerBoundCount
      || d_upperBoundCount != bc.d_upperBoundCount;
  }
  /** This is not a total order! */
  bool operator>=(BoundCounts bc) const {
    return d_lowerBoundCount >= bc.d_lowerBoundCount &&
      d_upperBoundCount >= bc.d_upperBoundCount;
  }

  inline bool isZero() const{ return d_lowerBoundCount == 0 && d_upperBoundCount == 0; }
  inline uint32_t lowerBoundCount() const{
    return d_lowerBoundCount;
  }
  inline uint32_t upperBoundCount() const{
    return d_upperBoundCount;
  }

  inline BoundCounts operator+(BoundCounts bc) const{
    return BoundCounts(d_lowerBoundCount + bc.d_lowerBoundCount,
                       d_upperBoundCount + bc.d_upperBoundCount);
  }

  inline BoundCounts operator-(BoundCounts bc) const {
    Assert(*this >= bc);
    return BoundCounts(d_lowerBoundCount - bc.d_lowerBoundCount,
                       d_upperBoundCount - bc.d_upperBoundCount);
  }


  inline BoundCounts& operator+=(BoundCounts bc) {
    d_upperBoundCount += bc.d_upperBoundCount;
    d_lowerBoundCount += bc.d_lowerBoundCount;
    return *this;
  }

  inline BoundCounts& operator-=(BoundCounts bc) {
    Assert(d_lowerBoundCount >= bc.d_lowerBoundCount);
    Assert(d_upperBoundCount >= bc.d_upperBoundCount);
    d_upperBoundCount -= bc.d_upperBoundCount;
    d_lowerBoundCount -= bc.d_lowerBoundCount;

    return *this;
  }

  /** Based on the sign coefficient a variable is multiplied by,
   * the effects the bound counts either has no effect (sgn == 0),
   * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
   */
  inline BoundCounts multiplyBySgn(int sgn) const{
    if(sgn > 0){
      return *this;
    }else if(sgn == 0){
      return BoundCounts(0,0);
    }else{
      return BoundCounts(d_upperBoundCount, d_lowerBoundCount);
    }
  }

  inline void addInChange(int sgn, BoundCounts before, BoundCounts after){
    if(before == after){
      return;
    }else if(sgn < 0){
      Assert(d_upperBoundCount >= before.d_lowerBoundCount);
      Assert(d_lowerBoundCount >= before.d_upperBoundCount);
      d_upperBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
      d_lowerBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
    }else if(sgn > 0){
      Assert(d_upperBoundCount >= before.d_upperBoundCount);
      Assert(d_lowerBoundCount >= before.d_lowerBoundCount);
      d_upperBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
      d_lowerBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
    }
  }

  inline void addInSgn(BoundCounts bc, int before, int after){
    Assert(before != after);
    Assert(!bc.isZero());

    if(before < 0){
      d_upperBoundCount -= bc.d_lowerBoundCount;
      d_lowerBoundCount -= bc.d_upperBoundCount;
    }else if(before > 0){
      d_upperBoundCount -= bc.d_upperBoundCount;
      d_lowerBoundCount -= bc.d_lowerBoundCount;
    }
    if(after < 0){
      d_upperBoundCount += bc.d_lowerBoundCount;
      d_lowerBoundCount += bc.d_upperBoundCount;
    }else if(after > 0){
      d_upperBoundCount += bc.d_upperBoundCount;
      d_lowerBoundCount += bc.d_lowerBoundCount;
    }
  }
};

class BoundsInfo {
private:

  /**
   * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j
   *
   * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)}
   * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)}
   */
  BoundCounts d_atBounds;

  /** This is for counting how many upper and lower bounds a row has. */
  BoundCounts d_hasBounds;

public:
  BoundsInfo() : d_atBounds(), d_hasBounds() {}
  BoundsInfo(BoundCounts atBounds, BoundCounts hasBounds)
    : d_atBounds(atBounds), d_hasBounds(hasBounds) {}

  BoundCounts atBounds() const { return d_atBounds; }
  BoundCounts hasBounds() const { return d_hasBounds; }

  /** This corresponds to adding in another variable to the row. */
  inline BoundsInfo operator+(const BoundsInfo& bc) const{
    return BoundsInfo(d_atBounds + bc.d_atBounds,
                      d_hasBounds + bc.d_hasBounds);
  }
  /** This corresponds to removing a variable from the row. */
  inline BoundsInfo operator-(const BoundsInfo& bc) const {
    Assert(*this >= bc);
    return BoundsInfo(d_atBounds - bc.d_atBounds,
                      d_hasBounds - bc.d_hasBounds);
  }

  inline BoundsInfo& operator+=(const BoundsInfo& bc) {
    d_atBounds += bc.d_atBounds;
    d_hasBounds += bc.d_hasBounds;
    return (*this);
  }

  /** Based on the sign coefficient a variable is multiplied by,
   * the effects the bound counts either has no effect (sgn == 0),
   * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
   */
  inline BoundsInfo multiplyBySgn(int sgn) const{
    return BoundsInfo(d_atBounds.multiplyBySgn(sgn), d_hasBounds.multiplyBySgn(sgn));
  }

  bool operator==(const BoundsInfo& other) const{
    return d_atBounds == other.d_atBounds && d_hasBounds == other.d_hasBounds;
  }
  bool operator!=(const BoundsInfo& other) const{
    return !(*this == other);
  }
  /** This is not a total order! */
  bool operator>=(const BoundsInfo& other) const{
    return d_atBounds >= other.d_atBounds && d_hasBounds >= other.d_hasBounds;
  }
  void addInChange(int sgn, const BoundsInfo& before, const BoundsInfo& after){
    addInAtBoundChange(sgn, before.d_atBounds, after.d_atBounds);
    addInHasBoundChange(sgn, before.d_hasBounds, after.d_hasBounds);
  }
  void addInAtBoundChange(int sgn, BoundCounts before, BoundCounts after){
    d_atBounds.addInChange(sgn, before, after);
  }
  void addInHasBoundChange(int sgn, BoundCounts before, BoundCounts after){
    d_hasBounds.addInChange(sgn, before, after);
  }

  inline void addInSgn(const BoundsInfo& bc, int before, int after){
    if(!bc.d_atBounds.isZero()){ d_atBounds.addInSgn(bc.d_atBounds, before, after);}
    if(!bc.d_hasBounds.isZero()){ d_hasBounds.addInSgn(bc.d_hasBounds, before, after);}
  }
};

/** This is intended to map each row to its relevant bound information. */
typedef DenseMap<BoundsInfo> BoundInfoMap;

inline std::ostream& operator<<(std::ostream& os, const BoundCounts& bc){
  os << "[bc " << bc.lowerBoundCount() << ", " << bc.upperBoundCount() << "]";
  return os;
}

inline std::ostream& operator<<(std::ostream& os, const BoundsInfo& inf){
  os << "[bi : @ " << inf.atBounds() << ", " << inf.hasBounds() << "]";
  return os;
}
class BoundUpdateCallback {
public:
  virtual ~BoundUpdateCallback() {}
  virtual void operator()(ArithVar v, const BoundsInfo&  up) = 0;
};

}  // 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, Clark Barrett
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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18
19		#include "cvc5_private.h"
20		#pragma once
21
22		#include "base/check.h"
23		#include "theory/arith/arithvar.h"
24		#include "util/dense_map.h"
25
26		namespace cvc5 {
27		namespace theory {
28		namespace arith {
29
30		class BoundCounts {
31		private:
32		uint32_t d_lowerBoundCount;
33		uint32_t d_upperBoundCount;
34
35		public:
36	41551114	BoundCounts() : d_lowerBoundCount(0), d_upperBoundCount(0) {}
37	162161408	BoundCounts(uint32_t lbs, uint32_t ubs)
38	162161408	: d_lowerBoundCount(lbs), d_upperBoundCount(ubs) {}
39
40	63997134	bool operator==(BoundCounts bc) const {
41	63997134	return d_lowerBoundCount == bc.d_lowerBoundCount
42	63997134	&& d_upperBoundCount == bc.d_upperBoundCount;
43		}
44	4578798	bool operator!=(BoundCounts bc) const {
45	4578798	return d_lowerBoundCount != bc.d_lowerBoundCount
46	4578798	\|\| d_upperBoundCount != bc.d_upperBoundCount;
47		}
48		/** This is not a total order! */
49		bool operator>=(BoundCounts bc) const {
50		return d_lowerBoundCount >= bc.d_lowerBoundCount &&
51		d_upperBoundCount >= bc.d_upperBoundCount;
52		}
53
54	220239793	inline bool isZero() const{ return d_lowerBoundCount == 0 && d_upperBoundCount == 0; }
55	19109083	inline uint32_t lowerBoundCount() const{
56	19109083	return d_lowerBoundCount;
57		}
58	18895743	inline uint32_t upperBoundCount() const{
59	18895743	return d_upperBoundCount;
60		}
61
62		inline BoundCounts operator+(BoundCounts bc) const{
63		return BoundCounts(d_lowerBoundCount + bc.d_lowerBoundCount,
64		d_upperBoundCount + bc.d_upperBoundCount);
65		}
66
67		inline BoundCounts operator-(BoundCounts bc) const {
68		Assert(*this >= bc);
69		return BoundCounts(d_lowerBoundCount - bc.d_lowerBoundCount,
70		d_upperBoundCount - bc.d_upperBoundCount);
71		}
72
73
74	933986	inline BoundCounts& operator+=(BoundCounts bc) {
75	933986	d_upperBoundCount += bc.d_upperBoundCount;
76	933986	d_lowerBoundCount += bc.d_lowerBoundCount;
77	933986	return *this;
78		}
79
80		inline BoundCounts& operator-=(BoundCounts bc) {
81		Assert(d_lowerBoundCount >= bc.d_lowerBoundCount);
82		Assert(d_upperBoundCount >= bc.d_upperBoundCount);
83		d_upperBoundCount -= bc.d_upperBoundCount;
84		d_lowerBoundCount -= bc.d_lowerBoundCount;
85
86		return *this;
87		}
88
89		/** Based on the sign coefficient a variable is multiplied by,
90		* the effects the bound counts either has no effect (sgn == 0),
91		* the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
92		*/
93	1170814	inline BoundCounts multiplyBySgn(int sgn) const{
94	1170814	if(sgn > 0){
95	408168	return *this;
96	762646	}else if(sgn == 0){
97		return BoundCounts(0,0);
98		}else{
99	762646	return BoundCounts(d_upperBoundCount, d_lowerBoundCount);
100		}
101		}
102
103	51284842	inline void addInChange(int sgn, BoundCounts before, BoundCounts after){
104	51284842	if(before == after){
105	3513993	return;
106	47770849	}else if(sgn < 0){
107	26463591	Assert(d_upperBoundCount >= before.d_lowerBoundCount);
108	26463591	Assert(d_lowerBoundCount >= before.d_upperBoundCount);
109	26463591	d_upperBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
110	26463591	d_lowerBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
111	21307258	}else if(sgn > 0){
112	21307258	Assert(d_upperBoundCount >= before.d_upperBoundCount);
113	21307258	Assert(d_lowerBoundCount >= before.d_lowerBoundCount);
114	21307258	d_upperBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
115	21307258	d_lowerBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
116		}
117		}
118
119	106537569	inline void addInSgn(BoundCounts bc, int before, int after){
120	106537569	Assert(before != after);
121	106537569	Assert(!bc.isZero());
122
123	106537569	if(before < 0){
124	27133678	d_upperBoundCount -= bc.d_lowerBoundCount;
125	27133678	d_lowerBoundCount -= bc.d_upperBoundCount;
126	79403891	}else if(before > 0){
127	27149676	d_upperBoundCount -= bc.d_upperBoundCount;
128	27149676	d_lowerBoundCount -= bc.d_lowerBoundCount;
129		}
130	106537569	if(after < 0){
131	31624621	d_upperBoundCount += bc.d_lowerBoundCount;
132	31624621	d_lowerBoundCount += bc.d_upperBoundCount;
133	74912948	}else if(after > 0){
134	28863403	d_upperBoundCount += bc.d_upperBoundCount;
135	28863403	d_lowerBoundCount += bc.d_lowerBoundCount;
136		}
137	106537569	}
138		};
139
140		class BoundsInfo {
141		private:
142
143		/**
144		* x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j
145		*
146		* AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)}
147		* AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)}
148		*/
149		BoundCounts d_atBounds;
150
151		/** This is for counting how many upper and lower bounds a row has. */
152		BoundCounts d_hasBounds;
153
154		public:
155	20775557	BoundsInfo() : d_atBounds(), d_hasBounds() {}
156	76705990	BoundsInfo(BoundCounts atBounds, BoundCounts hasBounds)
157	76705990	: d_atBounds(atBounds), d_hasBounds(hasBounds) {}
158
159	967547	BoundCounts atBounds() const { return d_atBounds; }
160	10005778	BoundCounts hasBounds() const { return d_hasBounds; }
161
162		/** This corresponds to adding in another variable to the row. */
163		inline BoundsInfo operator+(const BoundsInfo& bc) const{
164		return BoundsInfo(d_atBounds + bc.d_atBounds,
165		d_hasBounds + bc.d_hasBounds);
166		}
167		/** This corresponds to removing a variable from the row. */
168		inline BoundsInfo operator-(const BoundsInfo& bc) const {
169		Assert(*this >= bc);
170		return BoundsInfo(d_atBounds - bc.d_atBounds,
171		d_hasBounds - bc.d_hasBounds);
172		}
173
174	466993	inline BoundsInfo& operator+=(const BoundsInfo& bc) {
175	466993	d_atBounds += bc.d_atBounds;
176	466993	d_hasBounds += bc.d_hasBounds;
177	466993	return (*this);
178		}
179
180		/** Based on the sign coefficient a variable is multiplied by,
181		* the effects the bound counts either has no effect (sgn == 0),
182		* the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
183		*/
184	585407	inline BoundsInfo multiplyBySgn(int sgn) const{
185	585407	return BoundsInfo(d_atBounds.multiplyBySgn(sgn), d_hasBounds.multiplyBySgn(sgn));
186		}
187
188	9939912	bool operator==(const BoundsInfo& other) const{
189	9939912	return d_atBounds == other.d_atBounds && d_hasBounds == other.d_hasBounds;
190		}
191	9939912	bool operator!=(const BoundsInfo& other) const{
192	9939912	return !(*this == other);
193		}
194		/** This is not a total order! */
195		bool operator>=(const BoundsInfo& other) const{
196		return d_atBounds >= other.d_atBounds && d_hasBounds >= other.d_hasBounds;
197		}
198	23801143	void addInChange(int sgn, const BoundsInfo& before, const BoundsInfo& after){
199	23801143	addInAtBoundChange(sgn, before.d_atBounds, after.d_atBounds);
200	23801143	addInHasBoundChange(sgn, before.d_hasBounds, after.d_hasBounds);
201	23801143	}
202	27483699	void addInAtBoundChange(int sgn, BoundCounts before, BoundCounts after){
203	27483699	d_atBounds.addInChange(sgn, before, after);
204	27483699	}
205	23801143	void addInHasBoundChange(int sgn, BoundCounts before, BoundCounts after){
206	23801143	d_hasBounds.addInChange(sgn, before, after);
207	23801143	}
208
209	56851112	inline void addInSgn(const BoundsInfo& bc, int before, int after){
210	56851112	if(!bc.d_atBounds.isZero()){ d_atBounds.addInSgn(bc.d_atBounds, before, after);}
211	56851112	if(!bc.d_hasBounds.isZero()){ d_hasBounds.addInSgn(bc.d_hasBounds, before, after);}
212	56851112	}
213		};
214
215		/** This is intended to map each row to its relevant bound information. */
216		typedef DenseMap<BoundsInfo> BoundInfoMap;
217
218		inline std::ostream& operator<<(std::ostream& os, const BoundCounts& bc){
219		os << "[bc " << bc.lowerBoundCount() << ", " << bc.upperBoundCount() << "]";
220		return os;
221		}
222
223		inline std::ostream& operator<<(std::ostream& os, const BoundsInfo& inf){
224		os << "[bi : @ " << inf.atBounds() << ", " << inf.hasBounds() << "]";
225		return os;
226		}
227	2934328	class BoundUpdateCallback {
228		public:
229	2934328	virtual ~BoundUpdateCallback() {}
230		virtual void operator()(ArithVar v, const BoundsInfo& up) = 0;
231		};
232
233		} // namespace arith
234		} // namespace theory
235		} // namespace cvc5