Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/util/ite_utilities.h	Lines:	8	43	18.6 %
Date:	2021-05-22	Branches:	4	44	9.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Aina Niemetz, 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.
 * ****************************************************************************
 *
 * Simplifications for ITE expressions.
 *
 * This module implements preprocessing phases designed to simplify ITE
 * expressions.  Based on:
 * Kim, Somenzi, Jin.  Efficient Term-ITE Conversion for SMT.  FMCAD 2009.
 * Burch, Jerry.  Techniques for Verifying Superscalar Microprocessors.  DAC
 *'96
 */

#include "cvc5_private.h"

#ifndef CVC5__ITE_UTILITIES_H
#define CVC5__ITE_UTILITIES_H

#include <unordered_map>
#include <vector>

#include "expr/node.h"
#include "util/hash.h"
#include "util/statistics_stats.h"

namespace cvc5 {
namespace preprocessing {

class AssertionPipeline;

namespace util {

class ITECompressor;
class ITESimplifier;
class ITECareSimplifier;

/**
 * A caching visitor that computes whether a node contains a term ite.
 */
class ContainsTermITEVisitor
{
 public:
  ContainsTermITEVisitor();
  ~ContainsTermITEVisitor();

  /** returns true if a node contains a term ite. */
  bool containsTermITE(TNode n);

  /** Garbage collects the cache. */
  void garbageCollect();

  /** returns the size of the cache. */
  size_t cache_size() const { return d_cache.size(); }

 private:
  typedef std::unordered_map<Node, bool> NodeBoolMap;
  NodeBoolMap d_cache;
};

class ITEUtilities
{
 public:
  ITEUtilities();
  ~ITEUtilities();

  Node simpITE(TNode assertion);

  bool simpIteDidALotOfWorkHeuristic() const;

  /* returns false if an assertion is discovered to be equal to false. */
  bool compress(AssertionPipeline* assertionsToPreprocess);

  Node simplifyWithCare(TNode e);

  void clear();

  ContainsTermITEVisitor* getContainsVisitor()
  {
    return d_containsVisitor.get();
  }

  bool containsTermITE(TNode n)
  {
    return d_containsVisitor->containsTermITE(n);
  }

 private:
  std::unique_ptr<ContainsTermITEVisitor> d_containsVisitor;
  ITECompressor* d_compressor;
  ITESimplifier* d_simplifier;
  ITECareSimplifier* d_careSimp;
};

class IncomingArcCounter
{
 public:
  IncomingArcCounter(bool skipVars = false, bool skipConstants = false);
  ~IncomingArcCounter();
  void computeReachability(const std::vector<Node>& assertions);

  inline uint32_t lookupIncoming(Node n) const
  {
    NodeCountMap::const_iterator it = d_reachCount.find(n);
    if (it == d_reachCount.end())
    {
      return 0;
    }
    else
    {
      return (*it).second;
    }
  }
  void clear();

 private:
  typedef std::unordered_map<Node, uint32_t> NodeCountMap;
  NodeCountMap d_reachCount;

  bool d_skipVariables;
  bool d_skipConstants;
};

class TermITEHeightCounter
{
 public:
  TermITEHeightCounter();
  ~TermITEHeightCounter();

  /**
   * Compute and [potentially] cache the termITEHeight() of e.
   * The term ite height equals the maximum number of term ites
   * encountered on any path from e to a leaf.
   * Inductively:
   *  - termITEHeight(leaves) = 0
   *  - termITEHeight(e: term-ite(c, t, e) ) =
   *     1 + max(termITEHeight(t), termITEHeight(e)) ; Don't include c
   *  - termITEHeight(e not term ite) = max_{c in children(e))
   * (termITEHeight(c))
   */
  uint32_t termITEHeight(TNode e);

  /** Clear the cache. */
  void clear();

  /** Size of the cache. */
  size_t cache_size() const;

 private:
  typedef std::unordered_map<Node, uint32_t> NodeCountMap;
  NodeCountMap d_termITEHeight;
}; /* class TermITEHeightCounter */

/**
 * A routine designed to undo the potentially large blow up
 * due to expansion caused by the ite simplifier.
 */
class ITECompressor
{
 public:
  ITECompressor(ContainsTermITEVisitor* contains);
  ~ITECompressor();

  /* returns false if an assertion is discovered to be equal to false. */
  bool compress(AssertionPipeline* assertionsToPreprocess);

  /* garbage Collects the compressor. */
  void garbageCollect();

 private:
  Node d_true;  /* Copy of true. */
  Node d_false; /* Copy of false. */
  ContainsTermITEVisitor* d_contains;
  AssertionPipeline* d_assertions;
  IncomingArcCounter d_incoming;

  typedef std::unordered_map<Node, Node> NodeMap;
  NodeMap d_compressed;

  void reset();

  Node push_back_boolean(Node original, Node compressed);
  bool multipleParents(TNode c);
  Node compressBooleanITEs(Node toCompress);
  Node compressTerm(Node toCompress);
  Node compressBoolean(Node toCompress);

  class Statistics
  {
   public:
    IntStat d_compressCalls;
    IntStat d_skolemsAdded;
    Statistics();
  };
  Statistics d_statistics;
}; /* class ITECompressor */

class ITESimplifier
{
 public:
  ITESimplifier(ContainsTermITEVisitor* d_containsVisitor);
  ~ITESimplifier();

  Node simpITE(TNode assertion);

  bool doneALotOfWorkHeuristic() const;
  void clearSimpITECaches();

 private:
  Node d_true;
  Node d_false;

  ContainsTermITEVisitor* d_containsVisitor;
  inline bool containsTermITE(TNode n)
  {
    return d_containsVisitor->containsTermITE(n);
  }
  TermITEHeightCounter d_termITEHeight;
  inline uint32_t termITEHeight(TNode e)
  {
    return d_termITEHeight.termITEHeight(e);
  }

  // ConstantIte is a small inductive sublanguage:
  //     constant
  // or  termITE(cnd, ConstantIte, ConstantIte)
  typedef std::vector<Node> NodeVec;
  typedef std::unordered_map<Node, NodeVec*> ConstantLeavesMap;
  ConstantLeavesMap d_constantLeaves;

  // d_constantLeaves satisfies the following invariants:
  // not containsTermITE(x) then !isKey(x)
  // containsTermITE(x):
  // - not isKey(x) then this value is uncomputed
  // - d_constantLeaves[x] == NULL, then this contains a non-constant leaf
  // - d_constantLeaves[x] != NULL, then this contains a sorted list of constant
  // leaf
  bool isConstantIte(TNode e);

  /** If its not a constant and containsTermITE(ite),
   * returns a sorted NodeVec of the leaves. */
  NodeVec* computeConstantLeaves(TNode ite);

  // Lists all of the vectors in d_constantLeaves for fast deletion.
  std::vector<NodeVec*> d_allocatedConstantLeaves;

  /* transforms */
  Node transformAtom(TNode atom);
  Node attemptConstantRemoval(TNode atom);
  Node attemptLiftEquality(TNode atom);
  Node attemptEagerRemoval(TNode atom);

  // Given ConstantIte trees lcite and rcite,
  // return a boolean expression equivalent to (= lcite rcite)
  Node intersectConstantIte(TNode lcite, TNode rcite);

  // Given ConstantIte tree cite and a constant c,
  // return a boolean expression equivalent to (= lcite c)
  Node constantIteEqualsConstant(TNode cite, TNode c);
  uint32_t d_citeEqConstApplications;

  typedef std::pair<Node, Node> NodePair;
  using NodePairHashFunction =
      PairHashFunction<Node, Node, std::hash<Node>, std::hash<Node>>;
  typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap;
  NodePairMap d_constantIteEqualsConstantCache;
  NodePairMap d_replaceOverCache;
  NodePairMap d_replaceOverTermIteCache;
  Node replaceOver(Node n, Node replaceWith, Node simpVar);
  Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar);

  std::unordered_map<Node, bool> d_leavesConstCache;
  bool leavesAreConst(TNode e, theory::TheoryId tid);
  bool leavesAreConst(TNode e);

  NodePairMap d_simpConstCache;
  Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
  std::unordered_map<TypeNode, Node> d_simpVars;
  Node getSimpVar(TypeNode t);

  typedef std::unordered_map<Node, Node> NodeMap;
  NodeMap d_simpContextCache;
  Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);

  NodeMap d_simpITECache;
  Node simpITEAtom(TNode atom);

 private:
  class Statistics
  {
   public:
    IntStat d_maxNonConstantsFolded;
    IntStat d_unexpected;
    IntStat d_unsimplified;
    IntStat d_exactMatchFold;
    IntStat d_binaryPredFold;
    IntStat d_specialEqualityFolds;
    IntStat d_simpITEVisits;

    HistogramStat<uint32_t> d_inSmaller;

    Statistics();
  };

  Statistics d_statistics;
};

class ITECareSimplifier
{
 public:
  ITECareSimplifier();
  ~ITECareSimplifier();

  Node simplifyWithCare(TNode e);

  void clear();

 private:
  /**
   * This should always equal the number of care sets allocated by
   * this object - the number of these that have been deleted. This is
   * initially 0 and should always be 0 at the *start* of
   * ~ITECareSimplifier().
   */
  unsigned d_careSetsOutstanding;

  Node d_true;
  Node d_false;

  typedef std::unordered_map<TNode, Node> TNodeMap;

  class CareSetPtr;
  class CareSetPtrVal
  {
   public:
    bool safeToGarbageCollect() const { return d_refCount == 0; }

   private:
    friend class ITECareSimplifier::CareSetPtr;
    ITECareSimplifier& d_iteSimplifier;
    unsigned d_refCount;
    std::set<Node> d_careSet;
    CareSetPtrVal(ITECareSimplifier& simp)
        : d_iteSimplifier(simp), d_refCount(1)
    {
    }
  }; /* class ITECareSimplifier::CareSetPtrVal */

  std::vector<CareSetPtrVal*> d_usedSets;
  void careSetPtrGC(CareSetPtrVal* val) { d_usedSets.push_back(val); }

  class CareSetPtr
  {
    CareSetPtrVal* d_val;
    CareSetPtr(CareSetPtrVal* val) : d_val(val) {}

   public:
    CareSetPtr() : d_val(NULL) {}
    CareSetPtr(const CareSetPtr& cs)
    {
      d_val = cs.d_val;
      if (d_val != NULL)
      {
        ++(d_val->d_refCount);
      }
    }
    ~CareSetPtr()
    {
      if (d_val != NULL && (--(d_val->d_refCount) == 0))
      {
        d_val->d_iteSimplifier.careSetPtrGC(d_val);
      }
    }
    CareSetPtr& operator=(const CareSetPtr& cs)
    {
      if (d_val != cs.d_val)
      {
        if (d_val != NULL && (--(d_val->d_refCount) == 0))
        {
          d_val->d_iteSimplifier.careSetPtrGC(d_val);
        }
        d_val = cs.d_val;
        if (d_val != NULL)
        {
          ++(d_val->d_refCount);
        }
      }
      return *this;
    }
    std::set<Node>& getCareSet() { return d_val->d_careSet; }

    static CareSetPtr mkNew(ITECareSimplifier& simp);
    static CareSetPtr recycle(CareSetPtrVal* val)
    {
      Assert(val != NULL && val->d_refCount == 0);
      val->d_refCount = 1;
      return CareSetPtr(val);
    }
  }; /* class ITECareSimplifier::CareSetPtr */

  CareSetPtr getNewSet();

  typedef std::map<TNode, CareSetPtr> CareMap;
  void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet);
  Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache);
};

}  // namespace util
}  // namespace preprocessing
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Aina Niemetz, 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		* Simplifications for ITE expressions.
14		*
15		* This module implements preprocessing phases designed to simplify ITE
16		* expressions. Based on:
17		* Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009.
18		* Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC
19		*'96
20		*/
21
22		#include "cvc5_private.h"
23
24		#ifndef CVC5__ITE_UTILITIES_H
25		#define CVC5__ITE_UTILITIES_H
26
27		#include <unordered_map>
28		#include <vector>
29
30		#include "expr/node.h"
31		#include "util/hash.h"
32		#include "util/statistics_stats.h"
33
34		namespace cvc5 {
35		namespace preprocessing {
36
37		class AssertionPipeline;
38
39		namespace util {
40
41		class ITECompressor;
42		class ITESimplifier;
43		class ITECareSimplifier;
44
45		/**
46		* A caching visitor that computes whether a node contains a term ite.
47		*/
48		class ContainsTermITEVisitor
49		{
50		public:
51		ContainsTermITEVisitor();
52		~ContainsTermITEVisitor();
53
54		/** returns true if a node contains a term ite. */
55		bool containsTermITE(TNode n);
56
57		/** Garbage collects the cache. */
58		void garbageCollect();
59
60		/** returns the size of the cache. */
61		size_t cache_size() const { return d_cache.size(); }
62
63		private:
64		typedef std::unordered_map<Node, bool> NodeBoolMap;
65		NodeBoolMap d_cache;
66		};
67
68		class ITEUtilities
69		{
70		public:
71		ITEUtilities();
72		~ITEUtilities();
73
74		Node simpITE(TNode assertion);
75
76		bool simpIteDidALotOfWorkHeuristic() const;
77
78		/* returns false if an assertion is discovered to be equal to false. */
79		bool compress(AssertionPipeline* assertionsToPreprocess);
80
81		Node simplifyWithCare(TNode e);
82
83		void clear();
84
85		ContainsTermITEVisitor* getContainsVisitor()
86		{
87		return d_containsVisitor.get();
88		}
89
90	4	bool containsTermITE(TNode n)
91		{
92	4	return d_containsVisitor->containsTermITE(n);
93		}
94
95		private:
96		std::unique_ptr<ContainsTermITEVisitor> d_containsVisitor;
97		ITECompressor* d_compressor;
98		ITESimplifier* d_simplifier;
99		ITECareSimplifier* d_careSimp;
100		};
101
102		class IncomingArcCounter
103		{
104		public:
105		IncomingArcCounter(bool skipVars = false, bool skipConstants = false);
106		~IncomingArcCounter();
107		void computeReachability(const std::vector<Node>& assertions);
108
109	14218	inline uint32_t lookupIncoming(Node n) const
110		{
111	14218	NodeCountMap::const_iterator it = d_reachCount.find(n);
112	14218	if (it == d_reachCount.end())
113		{
114		return 0;
115		}
116		else
117		{
118	14218	return (*it).second;
119		}
120		}
121		void clear();
122
123		private:
124		typedef std::unordered_map<Node, uint32_t> NodeCountMap;
125		NodeCountMap d_reachCount;
126
127		bool d_skipVariables;
128		bool d_skipConstants;
129		};
130
131		class TermITEHeightCounter
132		{
133		public:
134		TermITEHeightCounter();
135		~TermITEHeightCounter();
136
137		/**
138		* Compute and [potentially] cache the termITEHeight() of e.
139		* The term ite height equals the maximum number of term ites
140		* encountered on any path from e to a leaf.
141		* Inductively:
142		* - termITEHeight(leaves) = 0
143		* - termITEHeight(e: term-ite(c, t, e) ) =
144		* 1 + max(termITEHeight(t), termITEHeight(e)) ; Don't include c
145		* - termITEHeight(e not term ite) = max_{c in children(e))
146		* (termITEHeight(c))
147		*/
148		uint32_t termITEHeight(TNode e);
149
150		/** Clear the cache. */
151		void clear();
152
153		/** Size of the cache. */
154		size_t cache_size() const;
155
156		private:
157		typedef std::unordered_map<Node, uint32_t> NodeCountMap;
158		NodeCountMap d_termITEHeight;
159		}; /* class TermITEHeightCounter */
160
161		/**
162		* A routine designed to undo the potentially large blow up
163		* due to expansion caused by the ite simplifier.
164		*/
165		class ITECompressor
166		{
167		public:
168		ITECompressor(ContainsTermITEVisitor* contains);
169		~ITECompressor();
170
171		/* returns false if an assertion is discovered to be equal to false. */
172		bool compress(AssertionPipeline* assertionsToPreprocess);
173
174		/* garbage Collects the compressor. */
175		void garbageCollect();
176
177		private:
178		Node d_true; /* Copy of true. */
179		Node d_false; /* Copy of false. */
180		ContainsTermITEVisitor* d_contains;
181		AssertionPipeline* d_assertions;
182		IncomingArcCounter d_incoming;
183
184		typedef std::unordered_map<Node, Node> NodeMap;
185		NodeMap d_compressed;
186
187		void reset();
188
189		Node push_back_boolean(Node original, Node compressed);
190		bool multipleParents(TNode c);
191		Node compressBooleanITEs(Node toCompress);
192		Node compressTerm(Node toCompress);
193		Node compressBoolean(Node toCompress);
194
195		class Statistics
196		{
197		public:
198		IntStat d_compressCalls;
199		IntStat d_skolemsAdded;
200		Statistics();
201		};
202		Statistics d_statistics;
203		}; /* class ITECompressor */
204
205		class ITESimplifier
206		{
207		public:
208		ITESimplifier(ContainsTermITEVisitor* d_containsVisitor);
209		~ITESimplifier();
210
211		Node simpITE(TNode assertion);
212
213		bool doneALotOfWorkHeuristic() const;
214		void clearSimpITECaches();
215
216		private:
217		Node d_true;
218		Node d_false;
219
220		ContainsTermITEVisitor* d_containsVisitor;
221	4086	inline bool containsTermITE(TNode n)
222		{
223	4086	return d_containsVisitor->containsTermITE(n);
224		}
225		TermITEHeightCounter d_termITEHeight;
226		inline uint32_t termITEHeight(TNode e)
227		{
228		return d_termITEHeight.termITEHeight(e);
229		}
230
231		// ConstantIte is a small inductive sublanguage:
232		// constant
233		// or termITE(cnd, ConstantIte, ConstantIte)
234		typedef std::vector<Node> NodeVec;
235		typedef std::unordered_map<Node, NodeVec*> ConstantLeavesMap;
236		ConstantLeavesMap d_constantLeaves;
237
238		// d_constantLeaves satisfies the following invariants:
239		// not containsTermITE(x) then !isKey(x)
240		// containsTermITE(x):
241		// - not isKey(x) then this value is uncomputed
242		// - d_constantLeaves[x] == NULL, then this contains a non-constant leaf
243		// - d_constantLeaves[x] != NULL, then this contains a sorted list of constant
244		// leaf
245		bool isConstantIte(TNode e);
246
247		/** If its not a constant and containsTermITE(ite),
248		* returns a sorted NodeVec of the leaves. */
249		NodeVec* computeConstantLeaves(TNode ite);
250
251		// Lists all of the vectors in d_constantLeaves for fast deletion.
252		std::vector<NodeVec*> d_allocatedConstantLeaves;
253
254		/* transforms */
255		Node transformAtom(TNode atom);
256		Node attemptConstantRemoval(TNode atom);
257		Node attemptLiftEquality(TNode atom);
258		Node attemptEagerRemoval(TNode atom);
259
260		// Given ConstantIte trees lcite and rcite,
261		// return a boolean expression equivalent to (= lcite rcite)
262		Node intersectConstantIte(TNode lcite, TNode rcite);
263
264		// Given ConstantIte tree cite and a constant c,
265		// return a boolean expression equivalent to (= lcite c)
266		Node constantIteEqualsConstant(TNode cite, TNode c);
267		uint32_t d_citeEqConstApplications;
268
269		typedef std::pair<Node, Node> NodePair;
270		using NodePairHashFunction =
271		PairHashFunction<Node, Node, std::hash<Node>, std::hash<Node>>;
272		typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap;
273		NodePairMap d_constantIteEqualsConstantCache;
274		NodePairMap d_replaceOverCache;
275		NodePairMap d_replaceOverTermIteCache;
276		Node replaceOver(Node n, Node replaceWith, Node simpVar);
277		Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar);
278
279		std::unordered_map<Node, bool> d_leavesConstCache;
280		bool leavesAreConst(TNode e, theory::TheoryId tid);
281		bool leavesAreConst(TNode e);
282
283		NodePairMap d_simpConstCache;
284		Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
285		std::unordered_map<TypeNode, Node> d_simpVars;
286		Node getSimpVar(TypeNode t);
287
288		typedef std::unordered_map<Node, Node> NodeMap;
289		NodeMap d_simpContextCache;
290		Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
291
292		NodeMap d_simpITECache;
293		Node simpITEAtom(TNode atom);
294
295		private:
296		class Statistics
297		{
298		public:
299		IntStat d_maxNonConstantsFolded;
300		IntStat d_unexpected;
301		IntStat d_unsimplified;
302		IntStat d_exactMatchFold;
303		IntStat d_binaryPredFold;
304		IntStat d_specialEqualityFolds;
305		IntStat d_simpITEVisits;
306
307		HistogramStat<uint32_t> d_inSmaller;
308
309		Statistics();
310		};
311
312		Statistics d_statistics;
313		};
314
315		class ITECareSimplifier
316		{
317		public:
318		ITECareSimplifier();
319		~ITECareSimplifier();
320
321		Node simplifyWithCare(TNode e);
322
323		void clear();
324
325		private:
326		/**
327		* This should always equal the number of care sets allocated by
328		* this object - the number of these that have been deleted. This is
329		* initially 0 and should always be 0 at the start of
330		* ~ITECareSimplifier().
331		*/
332		unsigned d_careSetsOutstanding;
333
334		Node d_true;
335		Node d_false;
336
337		typedef std::unordered_map<TNode, Node> TNodeMap;
338
339		class CareSetPtr;
340		class CareSetPtrVal
341		{
342		public:
343		bool safeToGarbageCollect() const { return d_refCount == 0; }
344
345		private:
346		friend class ITECareSimplifier::CareSetPtr;
347		ITECareSimplifier& d_iteSimplifier;
348		unsigned d_refCount;
349		std::set<Node> d_careSet;
350		CareSetPtrVal(ITECareSimplifier& simp)
351		: d_iteSimplifier(simp), d_refCount(1)
352		{
353		}
354		}; /* class ITECareSimplifier::CareSetPtrVal */
355
356		std::vector<CareSetPtrVal*> d_usedSets;
357		void careSetPtrGC(CareSetPtrVal* val) { d_usedSets.push_back(val); }
358
359		class CareSetPtr
360		{
361		CareSetPtrVal* d_val;
362		CareSetPtr(CareSetPtrVal* val) : d_val(val) {}
363
364		public:
365		CareSetPtr() : d_val(NULL) {}
366		CareSetPtr(const CareSetPtr& cs)
367		{
368		d_val = cs.d_val;
369		if (d_val != NULL)
370		{
371		++(d_val->d_refCount);
372		}
373		}
374		~CareSetPtr()
375		{
376		if (d_val != NULL && (--(d_val->d_refCount) == 0))
377		{
378		d_val->d_iteSimplifier.careSetPtrGC(d_val);
379		}
380		}
381		CareSetPtr& operator=(const CareSetPtr& cs)
382		{
383		if (d_val != cs.d_val)
384		{
385		if (d_val != NULL && (--(d_val->d_refCount) == 0))
386		{
387		d_val->d_iteSimplifier.careSetPtrGC(d_val);
388		}
389		d_val = cs.d_val;
390		if (d_val != NULL)
391		{
392		++(d_val->d_refCount);
393		}
394		}
395		return *this;
396		}
397		std::set<Node>& getCareSet() { return d_val->d_careSet; }
398
399		static CareSetPtr mkNew(ITECareSimplifier& simp);
400		static CareSetPtr recycle(CareSetPtrVal* val)
401		{
402		Assert(val != NULL && val->d_refCount == 0);
403		val->d_refCount = 1;
404		return CareSetPtr(val);
405		}
406		}; /* class ITECareSimplifier::CareSetPtr */
407
408		CareSetPtr getNewSet();
409
410		typedef std::map<TNode, CareSetPtr> CareMap;
411		void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet);
412		Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache);
413		};
414
415		} // namespace util
416		} // namespace preprocessing
417		} // namespace cvc5
418
419		#endif