Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/bound_counts.h	Lines:	83	97	85.6 %
Date:	2021-05-22	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	34074236	BoundCounts() : d_lowerBoundCount(0), d_upperBoundCount(0) {}
37	144678374	BoundCounts(uint32_t lbs, uint32_t ubs)
38	144678374	: d_lowerBoundCount(lbs), d_upperBoundCount(ubs) {}
39
40	51356242	bool operator==(BoundCounts bc) const {
41	51356242	return d_lowerBoundCount == bc.d_lowerBoundCount
42	51356242	&& d_upperBoundCount == bc.d_upperBoundCount;
43		}
44	3903963	bool operator!=(BoundCounts bc) const {
45	3903963	return d_lowerBoundCount != bc.d_lowerBoundCount
46	3903963	\|\| 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	204423939	inline bool isZero() const{ return d_lowerBoundCount == 0 && d_upperBoundCount == 0; }
55	14784544	inline uint32_t lowerBoundCount() const{
56	14784544	return d_lowerBoundCount;
57		}
58	14674989	inline uint32_t upperBoundCount() const{
59	14674989	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	760312	inline BoundCounts& operator+=(BoundCounts bc) {
75	760312	d_upperBoundCount += bc.d_upperBoundCount;
76	760312	d_lowerBoundCount += bc.d_lowerBoundCount;
77	760312	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	978634	inline BoundCounts multiplyBySgn(int sgn) const{
94	978634	if(sgn > 0){
95	329938	return *this;
96	648696	}else if(sgn == 0){
97		return BoundCounts(0,0);
98		}else{
99	648696	return BoundCounts(d_upperBoundCount, d_lowerBoundCount);
100		}
101		}
102
103	41216946	inline void addInChange(int sgn, BoundCounts before, BoundCounts after){
104	41216946	if(before == after){
105	2935574	return;
106	38281372	}else if(sgn < 0){
107	21273790	Assert(d_upperBoundCount >= before.d_lowerBoundCount);
108	21273790	Assert(d_lowerBoundCount >= before.d_upperBoundCount);
109	21273790	d_upperBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
110	21273790	d_lowerBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
111	17007582	}else if(sgn > 0){
112	17007582	Assert(d_upperBoundCount >= before.d_upperBoundCount);
113	17007582	Assert(d_lowerBoundCount >= before.d_lowerBoundCount);
114	17007582	d_upperBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
115	17007582	d_lowerBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
116		}
117		}
118
119	99089359	inline void addInSgn(BoundCounts bc, int before, int after){
120	99089359	Assert(before != after);
121	99089359	Assert(!bc.isZero());
122
123	99089359	if(before < 0){
124	25375025	d_upperBoundCount -= bc.d_lowerBoundCount;
125	25375025	d_lowerBoundCount -= bc.d_upperBoundCount;
126	73714334	}else if(before > 0){
127	25293719	d_upperBoundCount -= bc.d_upperBoundCount;
128	25293719	d_lowerBoundCount -= bc.d_lowerBoundCount;
129		}
130	99089359	if(after < 0){
131	29490168	d_upperBoundCount += bc.d_lowerBoundCount;
132	29490168	d_lowerBoundCount += bc.d_upperBoundCount;
133	69599191	}else if(after > 0){
134	26574356	d_upperBoundCount += bc.d_upperBoundCount;
135	26574356	d_lowerBoundCount += bc.d_lowerBoundCount;
136		}
137	99089359	}
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	17037118	BoundsInfo() : d_atBounds(), d_hasBounds() {}
156	68600193	BoundsInfo(BoundCounts atBounds, BoundCounts hasBounds)
157	68600193	: d_atBounds(atBounds), d_hasBounds(hasBounds) {}
158
159	837824	BoundCounts atBounds() const { return d_atBounds; }
160	7747491	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	380156	inline BoundsInfo& operator+=(const BoundsInfo& bc) {
175	380156	d_atBounds += bc.d_atBounds;
176	380156	d_hasBounds += bc.d_hasBounds;
177	380156	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	489317	inline BoundsInfo multiplyBySgn(int sgn) const{
185	489317	return BoundsInfo(d_atBounds.multiplyBySgn(sgn), d_hasBounds.multiplyBySgn(sgn));
186		}
187
188	7880098	bool operator==(const BoundsInfo& other) const{
189	7880098	return d_atBounds == other.d_atBounds && d_hasBounds == other.d_hasBounds;
190		}
191	7880098	bool operator!=(const BoundsInfo& other) const{
192	7880098	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	19034887	void addInChange(int sgn, const BoundsInfo& before, const BoundsInfo& after){
199	19034887	addInAtBoundChange(sgn, before.d_atBounds, after.d_atBounds);
200	19034887	addInHasBoundChange(sgn, before.d_hasBounds, after.d_hasBounds);
201	19034887	}
202	22182059	void addInAtBoundChange(int sgn, BoundCounts before, BoundCounts after){
203	22182059	d_atBounds.addInChange(sgn, before, after);
204	22182059	}
205	19034887	void addInHasBoundChange(int sgn, BoundCounts before, BoundCounts after){
206	19034887	d_hasBounds.addInChange(sgn, before, after);
207	19034887	}
208
209	52667290	inline void addInSgn(const BoundsInfo& bc, int before, int after){
210	52667290	if(!bc.d_atBounds.isZero()){ d_atBounds.addInSgn(bc.d_atBounds, before, after);}
211	52667290	if(!bc.d_hasBounds.isZero()){ d_hasBounds.addInSgn(bc.d_hasBounds, before, after);}
212	52667290	}
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	2028726	class BoundUpdateCallback {
228		public:
229	2028726	virtual ~BoundUpdateCallback() {}
230		virtual void operator()(ArithVar v, const BoundsInfo& up) = 0;
231		};
232
233		} // namespace arith
234		} // namespace theory
235		} // namespace cvc5