Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/context/cdhashset.h	Lines:	35	42	83.3 %
Date:	2021-08-01	Branches:	4	44	9.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Tim King, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * Context-dependent set class.
 */

#include "cvc5_private.h"

#ifndef CVC5__CONTEXT__CDHASHSET_H
#define CVC5__CONTEXT__CDHASHSET_H

#include "base/check.h"
#include "context/cdinsert_hashmap.h"
#include "context/context.h"

namespace cvc5 {
namespace context {

template <class V, class HashFcn = std::hash<V>>
class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn>
{
  typedef CDInsertHashMap<V, bool, HashFcn> super;

  // no copy or assignment
  CDHashSet(const CDHashSet&) = delete;
  CDHashSet& operator=(const CDHashSet&) = delete;

public:

  // ensure these are publicly accessible
  static void* operator new(size_t size, bool b) {
    return ContextObj::operator new(size, b);
  }

  static void operator delete(void* pMem, bool b) {
    return ContextObj::operator delete(pMem, b);
  }

  void deleteSelf() {
    this->ContextObj::deleteSelf();
  }

  static void operator delete(void* pMem) {
    AlwaysAssert(false) << "It is not allowed to delete a ContextObj this way!";
  }

  CDHashSet(Context* context) :
    super(context) {
  }

  size_t size() const {
    return super::size();
  }

  bool empty() const {
    return super::empty();
  }

  bool insert(const V& v) {
    return super::insert_safe(v, true);
  }

  bool contains(const V& v) const {
    return super::contains(v);
  }

  class const_iterator {
    typename super::const_iterator d_it;

  public:

    const_iterator(const typename super::const_iterator& it) : d_it(it) {}
    const_iterator(const const_iterator& it) : d_it(it.d_it) {}

    // Default constructor
    const_iterator() {}

    // (Dis)equality
    bool operator==(const const_iterator& i) const {
      return d_it == i.d_it;
    }
    bool operator!=(const const_iterator& i) const {
      return d_it != i.d_it;
    }

    // Dereference operators.
    V operator*() const {
      return (*d_it).first;
    }

    // Prefix increment
    const_iterator& operator++() {
      ++d_it;
      return *this;
    }

    // Postfix increment: requires a Proxy object to hold the
    // intermediate value for dereferencing
    class Proxy {
      const V& d_val;

    public:

      Proxy(const V& v) : d_val(v) {}

      V operator*() const {
        return d_val;
      }
      V* operator->() const { return &d_val; }
    };/* class CDSet<>::iterator::Proxy */

    // Actual postfix increment: returns Proxy with the old value.
    // Now, an expression like *i++ will return the current *i, and
    // then advance the orderedIterator.  However, don't try to use
    // Proxy for anything else.
    const Proxy operator++(int) {
      Proxy e(*(*this));
      ++(*this);
      return e;
    }
  };/* class CDSet<>::iterator */

  const_iterator begin() const {
    return const_iterator(super::begin());
  }

  const_iterator end() const {
    return const_iterator(super::end());
  }

  const_iterator find(const V& v) const {
    return const_iterator(super::find(v));
  }

  typedef typename super::key_iterator key_iterator;
  key_iterator key_begin() const {
    return super::key_begin();
  }
  key_iterator key_end() const {
    return super::key_end();
  }

  void insertAtContextLevelZero(const V& v) {
    return super::insertAtContextLevelZero(v, true);
  }

}; /* class CDHashSet */

}  // namespace context
}  // namespace cvc5

#endif /* CVC5__CONTEXT__CDHASHSET_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Tim King, Mathias Preiner
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		* Context-dependent set class.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__CONTEXT__CDHASHSET_H
19		#define CVC5__CONTEXT__CDHASHSET_H
20
21		#include "base/check.h"
22		#include "context/cdinsert_hashmap.h"
23		#include "context/context.h"
24
25		namespace cvc5 {
26		namespace context {
27
28		template <class V, class HashFcn = std::hash<V>>
29	784113	class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn>
30		{
31		typedef CDInsertHashMap<V, bool, HashFcn> super;
32
33		// no copy or assignment
34		CDHashSet(const CDHashSet&) = delete;
35		CDHashSet& operator=(const CDHashSet&) = delete;
36
37		public:
38
39		// ensure these are publicly accessible
40	6453	static void* operator new(size_t size, bool b) {
41	6453	return ContextObj::operator new(size, b);
42		}
43
44		static void operator delete(void* pMem, bool b) {
45		return ContextObj::operator delete(pMem, b);
46		}
47
48	6453	void deleteSelf() {
49	6453	this->ContextObj::deleteSelf();
50	6453	}
51
52		static void operator delete(void* pMem) {
53		AlwaysAssert(false) << "It is not allowed to delete a ContextObj this way!";
54		}
55
56	684419	CDHashSet(Context* context) :
57	684419	super(context) {
58	684419	}
59
60	7540	size_t size() const {
61	7540	return super::size();
62		}
63
64		bool empty() const {
65		return super::empty();
66		}
67
68	7331343	bool insert(const V& v) {
69	7331343	return super::insert_safe(v, true);
70		}
71
72	159596876	bool contains(const V& v) const {
73	159596876	return super::contains(v);
74		}
75
76		class const_iterator {
77		typename super::const_iterator d_it;
78
79		public:
80
81	44142556	const_iterator(const typename super::const_iterator& it) : d_it(it) {}
82		const_iterator(const const_iterator& it) : d_it(it.d_it) {}
83
84		// Default constructor
85		const_iterator() {}
86
87		// (Dis)equality
88	5620427	bool operator==(const const_iterator& i) const {
89	5620427	return d_it == i.d_it;
90		}
91	16450936	bool operator!=(const const_iterator& i) const {
92	16450936	return d_it != i.d_it;
93		}
94
95		// Dereference operators.
96	162	V operator*() const {
97	162	return (*d_it).first;
98		}
99
100		// Prefix increment
101	162	const_iterator& operator++() {
102	162	++d_it;
103	162	return *this;
104		}
105
106		// Postfix increment: requires a Proxy object to hold the
107		// intermediate value for dereferencing
108		class Proxy {
109		const V& d_val;
110
111		public:
112
113		Proxy(const V& v) : d_val(v) {}
114
115		V operator*() const {
116		return d_val;
117		}
118		V* operator->() const { return &d_val; }
119		};/* class CDSet<>::iterator::Proxy */
120
121		// Actual postfix increment: returns Proxy with the old value.
122		// Now, an expression like i++ will return the current i, and
123		// then advance the orderedIterator. However, don't try to use
124		// Proxy for anything else.
125		const Proxy operator++(int) {
126		Proxy e((this));
127		++(*this);
128		return e;
129		}
130		};/* class CDSet<>::iterator */
131
132	80	const_iterator begin() const {
133	80	return const_iterator(super::begin());
134		}
135
136	22071355	const_iterator end() const {
137	22071355	return const_iterator(super::end());
138		}
139
140	22071121	const_iterator find(const V& v) const {
141	22071121	return const_iterator(super::find(v));
142		}
143
144		typedef typename super::key_iterator key_iterator;
145	583	key_iterator key_begin() const {
146	583	return super::key_begin();
147		}
148	583	key_iterator key_end() const {
149	583	return super::key_end();
150		}
151
152		void insertAtContextLevelZero(const V& v) {
153		return super::insertAtContextLevelZero(v, true);
154		}
155
156		}; /* class CDHashSet */
157
158		} // namespace context
159		} // namespace cvc5
160
161		#endif /* CVC5__CONTEXT__CDHASHSET_H */