Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/equality_engine_types.h	Lines:	61	81	75.3 %
Date:	2021-05-22	Branches:	11	34	32.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Dejan Jovanovic, Andrew Reynolds, Haniel Barbosa
 *
 * 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"

#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H
#define CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H

#include <string>
#include <iostream>
#include <sstream>

#include "util/hash.h"

namespace cvc5 {
namespace theory {
namespace eq {

/** Default type for the size of the sizes (size_t replacement) */
typedef uint32_t DefaultSizeType;

/** Id of the node */
typedef DefaultSizeType EqualityNodeId;

/** Id of the use list */
typedef DefaultSizeType UseListNodeId;

/** The trigger ids */
typedef DefaultSizeType TriggerId;

/** The equality edge ids */
typedef DefaultSizeType EqualityEdgeId;

/** The null node */
static const EqualityNodeId null_id = (EqualityNodeId)(-1);

/** The null use list node */
static const EqualityNodeId null_uselist_id = (EqualityNodeId)(-1);

/** The null trigger */
static const TriggerId null_trigger = (TriggerId)(-1);

/** The null edge id */
static const EqualityEdgeId null_edge = (EqualityEdgeId)(-1);

/**
 * A reason for a merge. Either an equality x = y, a merge of two
 * function applications f(x1, x2), f(y1, y2) due to congruence,
 * or a merge of an equality to false due to both sides being
 * (different) constants.
 */
enum MergeReasonType
{
  /** Terms were merged due to congruence */
  MERGED_THROUGH_CONGRUENCE,
  /** Terms were merged due to an assumption */
  MERGED_THROUGH_EQUALITY,
  /** Terms were merged due to reflexivity */
  MERGED_THROUGH_REFLEXIVITY,
  /** Terms were merged due to theory reasoning */
  MERGED_THROUGH_CONSTANTS,
  /** Terms were merged due to transitivity */
  MERGED_THROUGH_TRANS,
};

inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
  switch (reason) {
  case MERGED_THROUGH_CONGRUENCE:
    out << "congruence";
    break;
  case MERGED_THROUGH_EQUALITY:
    out << "pure equality";
    break;
  case MERGED_THROUGH_REFLEXIVITY:
    out << "reflexivity";
    break;
  case MERGED_THROUGH_CONSTANTS: out << "theory constants"; break;
  case MERGED_THROUGH_TRANS:
    out << "transitivity";
    break;
  default:
    out << "[theory]";
    break;
  }
  return out;
}

/**
 * A candidate for merging two equivalence classes, with the necessary
 * additional information.
 */
struct MergeCandidate {
  EqualityNodeId d_t1Id, d_t2Id;
  unsigned d_type;
  TNode d_reason;
  MergeCandidate(EqualityNodeId x,
                 EqualityNodeId y,
                 unsigned type,
                 TNode reason)
      : d_t1Id(x), d_t2Id(y), d_type(type), d_reason(reason)
  {}
};

/**
 * Just an index into the reasons array, and the number of merges to consume.
 */
struct DisequalityReasonRef {
  DefaultSizeType d_mergesStart;
  DefaultSizeType d_mergesEnd;
  DisequalityReasonRef(DefaultSizeType mergesStart = 0,
                       DefaultSizeType mergesEnd = 0)
      : d_mergesStart(mergesStart), d_mergesEnd(mergesEnd)
  {
  }
};

/**
 * We maintain uselist where a node appears in, and this is the node
 * of such a list.
 */
class UseListNode {

private:

  /** The id of the application node where this representative is at */
  EqualityNodeId d_applicationId;

  /** The next one in the class */
  UseListNodeId d_nextUseListNodeId;

public:

  /**
   * Creates a new node, which is in a list of it's own.
   */
  UseListNode(EqualityNodeId nodeId = null_id, UseListNodeId nextId = null_uselist_id)
  : d_applicationId(nodeId), d_nextUseListNodeId(nextId) {}

  /**
   * Returns the next node in the circular list.
   */
  UseListNodeId getNext() const {
    return d_nextUseListNodeId;
  }

  /**
   * Returns the id of the function application.
   */
  EqualityNodeId getApplicationId() const {
    return d_applicationId;
  }
};

/**
 * Main class for representing nodes in the equivalence class. The
 * nodes are a circular list, with the representative carrying the
 * size. Each individual node carries with itself the uselist of
 * function applications it appears in and the list of asserted
 * disequalities it belongs to. In order to get these lists one must
 * traverse the entire class and pick up all the individual lists.
 */
class EqualityNode {

private:

  /** The size of this equivalence class (if it's a representative) */
  DefaultSizeType d_size;

  /** The id (in the eq-manager) of the representative equality node */
  EqualityNodeId d_findId;

  /** The next equality node in this class */
  EqualityNodeId d_nextId;

  /** The use list of this node */
  UseListNodeId d_useList;

public:

  /**
   * Creates a new node, which is in a list of it's own.
   */
  EqualityNode(EqualityNodeId nodeId = null_id)
  : d_size(1)
  , d_findId(nodeId)
  , d_nextId(nodeId)
  , d_useList(null_uselist_id)
  {}

  /**
   * Returns the requested uselist.
   */
  UseListNodeId getUseList() const {
    return d_useList;
  }

  /**
   * Returns the next node in the class circular list.
   */
  EqualityNodeId getNext() const {
    return d_nextId;
  }

  /**
   * Returns the size of this equivalence class (only valid if this is the representative).
   */
  DefaultSizeType getSize() const {
    return d_size;
  }

  /**
   * Merges the two lists. If add size is true the size of this node is increased by the size of
   * the other node, otherwise the size is decreased by the size of the other node.
   */
  template<bool addSize>
  void merge(EqualityNode& other) {
    EqualityNodeId tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp;
    if (addSize) {
      d_size += other.d_size;
    } else {
      d_size -= other.d_size;
    }
  }

  /**
   * Returns the class representative.
   */
  EqualityNodeId getFind() const { return d_findId; }

  /**
   * Set the class representative.
   */
  void setFind(EqualityNodeId findId) { d_findId = findId; }

  /**
   * Note that this node is used in a function application funId, or
   * a negatively asserted equality (dis-equality) with funId.
   */
  template<typename memory_class>
  void usedIn(EqualityNodeId funId, memory_class& memory) {
    UseListNodeId newUseId = memory.size();
    memory.push_back(UseListNode(funId, d_useList));
    d_useList = newUseId;
  }

  /**
   * For backtracking: remove the first element from the uselist and pop the memory.
   */
  template<typename memory_class>
  void removeTopFromUseList(memory_class& memory) {
    Assert((int)d_useList == (int)memory.size() - 1);
    d_useList = memory.back().getNext();
    memory.pop_back();
  }
};

/** A pair of ids */
typedef std::pair<EqualityNodeId, EqualityNodeId> EqualityPair;
using EqualityPairHashFunction =
    PairHashFunction<EqualityNodeId, EqualityNodeId>;

enum FunctionApplicationType {
  /** This application is an equality a = b */
  APP_EQUALITY,
  /** This is a part of an uninterpreted application f(t1, ...., tn) */
  APP_UNINTERPRETED,
  /** This is a part of an interpreted application f(t1, ..., tn) */
  APP_INTERPRETED
};

/**
 * Represents the function APPLY a b. If isEquality is true then it
 * represents the predicate (a = b). Note that since one can not
 * construct the equality over function terms, the equality and hash
 * function below are still well defined.
 */
struct FunctionApplication {
  /** Type of application */
  FunctionApplicationType d_type;
  /** The actual application elements */
  EqualityNodeId d_a, d_b;

  /** Construct an application */
  FunctionApplication(FunctionApplicationType type = APP_EQUALITY,
                      EqualityNodeId a = null_id,
                      EqualityNodeId b = null_id)
      : d_type(type), d_a(a), d_b(b)
  {
  }

  /** Equality of two applications */
  bool operator == (const FunctionApplication& other) const {
    return d_type == other.d_type && d_a == other.d_a && d_b == other.d_b;
  }

  /** Is this a null application */
  bool isNull() const { return d_a == null_id || d_b == null_id; }

  /** Is this an equality */
  bool isEquality() const { return d_type == APP_EQUALITY; }

  /** Is this an interpreted application (equality is special, i.e. not interpreted) */
  bool isInterpreted() const { return d_type == APP_INTERPRETED; }
};

struct FunctionApplicationHashFunction {
  size_t operator () (const FunctionApplication& app) const {
    size_t hash = 0;
    hash = 0x9e3779b9 + app.d_a;
    hash ^= 0x9e3779b9 + app.d_b + (hash << 6) + (hash >> 2);
    return hash;
  }
};

/**
 * At time of addition a function application can already normalize to something, so
 * we keep both the original, and the normalized version.
 */
struct FunctionApplicationPair {
  FunctionApplication d_original;
  FunctionApplication d_normalized;
  FunctionApplicationPair() {}
  FunctionApplicationPair(const FunctionApplication& original,
                          const FunctionApplication& normalized)
      : d_original(original), d_normalized(normalized)
  {
  }
  bool isNull() const { return d_original.isNull(); }
};

/**
 * Information about the added triggers.
 */
struct TriggerInfo {
  /** The trigger itself */
  Node d_trigger;
  /** Polarity of the trigger */
  bool d_polarity;
  TriggerInfo() : d_polarity(false) {}
  TriggerInfo(Node trigger, bool polarity)
      : d_trigger(trigger), d_polarity(polarity)
  {
  }
};

} // namespace eq
} // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Dejan Jovanovic, Andrew Reynolds, Haniel Barbosa
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
21		#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H
22		#define CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H
23
24		#include <string>
25		#include <iostream>
26		#include <sstream>
27
28		#include "util/hash.h"
29
30		namespace cvc5 {
31		namespace theory {
32		namespace eq {
33
34		/** Default type for the size of the sizes (size_t replacement) */
35		typedef uint32_t DefaultSizeType;
36
37		/** Id of the node */
38		typedef DefaultSizeType EqualityNodeId;
39
40		/** Id of the use list */
41		typedef DefaultSizeType UseListNodeId;
42
43		/** The trigger ids */
44		typedef DefaultSizeType TriggerId;
45
46		/** The equality edge ids */
47		typedef DefaultSizeType EqualityEdgeId;
48
49		/** The null node */
50		static const EqualityNodeId null_id = (EqualityNodeId)(-1);
51
52		/** The null use list node */
53		static const EqualityNodeId null_uselist_id = (EqualityNodeId)(-1);
54
55		/** The null trigger */
56		static const TriggerId null_trigger = (TriggerId)(-1);
57
58		/** The null edge id */
59		static const EqualityEdgeId null_edge = (EqualityEdgeId)(-1);
60
61		/**
62		* A reason for a merge. Either an equality x = y, a merge of two
63		* function applications f(x1, x2), f(y1, y2) due to congruence,
64		* or a merge of an equality to false due to both sides being
65		* (different) constants.
66		*/
67		enum MergeReasonType
68		{
69		/** Terms were merged due to congruence */
70		MERGED_THROUGH_CONGRUENCE,
71		/** Terms were merged due to an assumption */
72		MERGED_THROUGH_EQUALITY,
73		/** Terms were merged due to reflexivity */
74		MERGED_THROUGH_REFLEXIVITY,
75		/** Terms were merged due to theory reasoning */
76		MERGED_THROUGH_CONSTANTS,
77		/** Terms were merged due to transitivity */
78		MERGED_THROUGH_TRANS,
79		};
80
81		inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
82		switch (reason) {
83		case MERGED_THROUGH_CONGRUENCE:
84		out << "congruence";
85		break;
86		case MERGED_THROUGH_EQUALITY:
87		out << "pure equality";
88		break;
89		case MERGED_THROUGH_REFLEXIVITY:
90		out << "reflexivity";
91		break;
92		case MERGED_THROUGH_CONSTANTS: out << "theory constants"; break;
93		case MERGED_THROUGH_TRANS:
94		out << "transitivity";
95		break;
96		default:
97		out << "[theory]";
98		break;
99		}
100		return out;
101		}
102
103		/**
104		* A candidate for merging two equivalence classes, with the necessary
105		* additional information.
106		*/
107	146208486	struct MergeCandidate {
108		EqualityNodeId d_t1Id, d_t2Id;
109		unsigned d_type;
110		TNode d_reason;
111	30656006	MergeCandidate(EqualityNodeId x,
112		EqualityNodeId y,
113		unsigned type,
114		TNode reason)
115	30656006	: d_t1Id(x), d_t2Id(y), d_type(type), d_reason(reason)
116	30656006	{}
117		};
118
119		/**
120		* Just an index into the reasons array, and the number of merges to consume.
121		*/
122		struct DisequalityReasonRef {
123		DefaultSizeType d_mergesStart;
124		DefaultSizeType d_mergesEnd;
125	16738509	DisequalityReasonRef(DefaultSizeType mergesStart = 0,
126		DefaultSizeType mergesEnd = 0)
127	16738509	: d_mergesStart(mergesStart), d_mergesEnd(mergesEnd)
128		{
129	16738509	}
130		};
131
132		/**
133		* We maintain uselist where a node appears in, and this is the node
134		* of such a list.
135		*/
136		class UseListNode {
137
138		private:
139
140		/** The id of the application node where this representative is at */
141		EqualityNodeId d_applicationId;
142
143		/** The next one in the class */
144		UseListNodeId d_nextUseListNodeId;
145
146		public:
147
148		/**
149		* Creates a new node, which is in a list of it's own.
150		*/
151	5934382	UseListNode(EqualityNodeId nodeId = null_id, UseListNodeId nextId = null_uselist_id)
152	5934382	: d_applicationId(nodeId), d_nextUseListNodeId(nextId) {}
153
154		/**
155		* Returns the next node in the circular list.
156		*/
157	55777414	UseListNodeId getNext() const {
158	55777414	return d_nextUseListNodeId;
159		}
160
161		/**
162		* Returns the id of the function application.
163		*/
164	99693692	EqualityNodeId getApplicationId() const {
165	99693692	return d_applicationId;
166		}
167		};
168
169		/**
170		* Main class for representing nodes in the equivalence class. The
171		* nodes are a circular list, with the representative carrying the
172		* size. Each individual node carries with itself the uselist of
173		* function applications it appears in and the list of asserted
174		* disequalities it belongs to. In order to get these lists one must
175		* traverse the entire class and pick up all the individual lists.
176		*/
177		class EqualityNode {
178
179		private:
180
181		/** The size of this equivalence class (if it's a representative) */
182		DefaultSizeType d_size;
183
184		/** The id (in the eq-manager) of the representative equality node */
185		EqualityNodeId d_findId;
186
187		/** The next equality node in this class */
188		EqualityNodeId d_nextId;
189
190		/** The use list of this node */
191		UseListNodeId d_useList;
192
193		public:
194
195		/**
196		* Creates a new node, which is in a list of it's own.
197		*/
198	7155562	EqualityNode(EqualityNodeId nodeId = null_id)
199	7155562	: d_size(1)
200		, d_findId(nodeId)
201		, d_nextId(nodeId)
202	7155562	, d_useList(null_uselist_id)
203	7155562	{}
204
205		/**
206		* Returns the requested uselist.
207		*/
208	34490542	UseListNodeId getUseList() const {
209	34490542	return d_useList;
210		}
211
212		/**
213		* Returns the next node in the class circular list.
214		*/
215	108165944	EqualityNodeId getNext() const {
216	108165944	return d_nextId;
217		}
218
219		/**
220		* Returns the size of this equivalence class (only valid if this is the representative).
221		*/
222	13181022	DefaultSizeType getSize() const {
223	13181022	return d_size;
224		}
225
226		/**
227		* Merges the two lists. If add size is true the size of this node is increased by the size of
228		* the other node, otherwise the size is decreased by the size of the other node.
229		*/
230		template<bool addSize>
231	44093467	void merge(EqualityNode& other) {
232	44093467	EqualityNodeId tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp;
233		if (addSize) {
234	22047360	d_size += other.d_size;
235		} else {
236	22046107	d_size -= other.d_size;
237		}
238	44093467	}
239
240		/**
241		* Returns the class representative.
242		*/
243	838227062	EqualityNodeId getFind() const { return d_findId; }
244
245		/**
246		* Set the class representative.
247		*/
248	57490135	void setFind(EqualityNodeId findId) { d_findId = findId; }
249
250		/**
251		* Note that this node is used in a function application funId, or
252		* a negatively asserted equality (dis-equality) with funId.
253		*/
254		template<typename memory_class>
255	5934382	void usedIn(EqualityNodeId funId, memory_class& memory) {
256	5934382	UseListNodeId newUseId = memory.size();
257	5934382	memory.push_back(UseListNode(funId, d_useList));
258	5934382	d_useList = newUseId;
259	5934382	}
260
261		/**
262		* For backtracking: remove the first element from the uselist and pop the memory.
263		*/
264		template<typename memory_class>
265	5930568	void removeTopFromUseList(memory_class& memory) {
266	5930568	Assert((int)d_useList == (int)memory.size() - 1);
267	5930568	d_useList = memory.back().getNext();
268	5930568	memory.pop_back();
269	5930568	}
270		};
271
272		/** A pair of ids */
273		typedef std::pair<EqualityNodeId, EqualityNodeId> EqualityPair;
274		using EqualityPairHashFunction =
275		PairHashFunction<EqualityNodeId, EqualityNodeId>;
276
277		enum FunctionApplicationType {
278		/** This application is an equality a = b */
279		APP_EQUALITY,
280		/** This is a part of an uninterpreted application f(t1, ...., tn) */
281		APP_UNINTERPRETED,
282		/** This is a part of an interpreted application f(t1, ..., tn) */
283		APP_INTERPRETED
284		};
285
286		/**
287		* Represents the function APPLY a b. If isEquality is true then it
288		* represents the predicate (a = b). Note that since one can not
289		* construct the equality over function terms, the equality and hash
290		* function below are still well defined.
291		*/
292		struct FunctionApplication {
293		/** Type of application */
294		FunctionApplicationType d_type;
295		/** The actual application elements */
296		EqualityNodeId d_a, d_b;
297
298		/** Construct an application */
299	61524571	FunctionApplication(FunctionApplicationType type = APP_EQUALITY,
300		EqualityNodeId a = null_id,
301		EqualityNodeId b = null_id)
302	61524571	: d_type(type), d_a(a), d_b(b)
303		{
304	61524571	}
305
306		/** Equality of two applications */
307	44067039	bool operator == (const FunctionApplication& other) const {
308	44067039	return d_type == other.d_type && d_a == other.d_a && d_b == other.d_b;
309		}
310
311		/** Is this a null application */
312	6875980	bool isNull() const { return d_a == null_id \|\| d_b == null_id; }
313
314		/** Is this an equality */
315	28848307	bool isEquality() const { return d_type == APP_EQUALITY; }
316
317		/** Is this an interpreted application (equality is special, i.e. not interpreted) */
318	34375661	bool isInterpreted() const { return d_type == APP_INTERPRETED; }
319		};
320
321		struct FunctionApplicationHashFunction {
322	90996453	size_t operator () (const FunctionApplication& app) const {
323	90996453	size_t hash = 0;
324	90996453	hash = 0x9e3779b9 + app.d_a;
325	90996453	hash ^= 0x9e3779b9 + app.d_b + (hash << 6) + (hash >> 2);
326	90996453	return hash;
327		}
328		};
329
330		/**
331		* At time of addition a function application can already normalize to something, so
332		* we keep both the original, and the normalized version.
333		*/
334		struct FunctionApplicationPair {
335		FunctionApplication d_original;
336		FunctionApplication d_normalized;
337	7155562	FunctionApplicationPair() {}
338	2967191	FunctionApplicationPair(const FunctionApplication& original,
339		const FunctionApplication& normalized)
340	2967191	: d_original(original), d_normalized(normalized)
341		{
342	2967191	}
343		bool isNull() const { return d_original.isNull(); }
344		};
345
346		/**
347		* Information about the added triggers.
348		*/
349	16282562	struct TriggerInfo {
350		/** The trigger itself */
351		Node d_trigger;
352		/** Polarity of the trigger */
353		bool d_polarity;
354		TriggerInfo() : d_polarity(false) {}
355	3458436	TriggerInfo(Node trigger, bool polarity)
356	3458436	: d_trigger(trigger), d_polarity(polarity)
357		{
358	3458436	}
359		};
360
361		} // namespace eq
362		} // namespace theory
363		} // namespace cvc5
364
365		#endif /* CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H */