Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/substitutions.h	Lines:	11	15	73.3 %
Date:	2021-08-17	Branches:	2	16	12.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Dejan Jovanovic, 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.
 * ****************************************************************************
 *
 * A substitution mapping for theory simplification.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__SUBSTITUTIONS_H
#define CVC5__THEORY__SUBSTITUTIONS_H

//#include <algorithm>
#include <utility>
#include <vector>
#include <unordered_map>

#include "expr/node.h"
#include "context/context.h"
#include "context/cdo.h"
#include "context/cdhashmap.h"
#include "util/hash.h"

namespace cvc5 {
namespace theory {

/**
 * The type for the Substitutions mapping output by
 * Theory::simplify(), TheoryEngine::simplify(), and
 * Valuation::simplify().  This is in its own header to
 * avoid circular dependences between those three.
 *
 * This map is context-dependent.
 */
class SubstitutionMap
{
 public:
  typedef context::CDHashMap<Node, Node> NodeMap;

  typedef NodeMap::iterator iterator;
  typedef NodeMap::const_iterator const_iterator;

 private:
  typedef std::unordered_map<Node, Node> NodeCache;
  /** A dummy context used by this class if none is provided */
  context::Context d_context;

  /** The variables, in order of addition */
  NodeMap d_substitutions;

  /** Cache of the already performed substitutions */
  NodeCache d_substitutionCache;

  /** Has the cache been invalidated? */
  bool d_cacheInvalidated;

  /** Internal method that performs substitution */
  Node internalSubstitute(TNode t, NodeCache& cache);

  /** Helper class to invalidate cache on user pop */
  class CacheInvalidator : public context::ContextNotifyObj
  {
    bool& d_cacheInvalidated;

   protected:
    void contextNotifyPop() override { d_cacheInvalidated = true; }

   public:
    CacheInvalidator(context::Context* context, bool& cacheInvalidated)
        : context::ContextNotifyObj(context),
          d_cacheInvalidated(cacheInvalidated)
    {
    }

  }; /* class SubstitutionMap::CacheInvalidator */

  /**
   * This object is notified on user pop and marks the SubstitutionMap's
   * cache as invalidated.
   */
  CacheInvalidator d_cacheInvalidator;

 public:
  SubstitutionMap(context::Context* context = nullptr);

  /**
   * Adds a substitution from x to t.
   */
  void addSubstitution(TNode x, TNode t, bool invalidateCache = true);

  /**
   * Merge subMap into current set of substitutions
   */
  void addSubstitutions(SubstitutionMap& subMap, bool invalidateCache = true);

  /**
   * Returns true iff x is in the substitution map
   */
  bool hasSubstitution(TNode x) const
  {
    return d_substitutions.find(x) != d_substitutions.end();
  }

  /**
   * Returns the substitution mapping that was given for x via
   * addSubstitution().  Note that the returned value might itself
   * be in the map; for the actual substitution that would be
   * performed for x, use .apply(x).  This getSubstitution() function
   * is mainly intended for constructing assertions about what has
   * already been put in the map.
   */
  TNode getSubstitution(TNode x) const
  {
    AssertArgument(
        hasSubstitution(x), x, "element not in this substitution map");
    return (*d_substitutions.find(x)).second;
  }

  /**
   * Apply the substitutions to the node.
   */
  Node apply(TNode t, bool doRewrite = false);

  /**
   * Apply the substitutions to the node.
   */
  Node apply(TNode t, bool doRewrite = false) const
  {
    return const_cast<SubstitutionMap*>(this)->apply(t, doRewrite);
  }

  iterator begin() { return d_substitutions.begin(); }

  iterator end() { return d_substitutions.end(); }

  const_iterator begin() const { return d_substitutions.begin(); }

  const_iterator end() const { return d_substitutions.end(); }

  bool empty() const { return d_substitutions.empty(); }

  /**
   * Print to the output stream
   */
  void print(std::ostream& out) const;
  void debugPrint() const;

}; /* class SubstitutionMap */

inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subst) {
  subst.print(out);
  return out;
}

}  // namespace theory

std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i);

}  // namespace cvc5

#endif /* CVC5__THEORY__SUBSTITUTIONS_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Dejan Jovanovic, 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		* A substitution mapping for theory simplification.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__SUBSTITUTIONS_H
19		#define CVC5__THEORY__SUBSTITUTIONS_H
20
21		//#include <algorithm>
22		#include <utility>
23		#include <vector>
24		#include <unordered_map>
25
26		#include "expr/node.h"
27		#include "context/context.h"
28		#include "context/cdo.h"
29		#include "context/cdhashmap.h"
30		#include "util/hash.h"
31
32		namespace cvc5 {
33		namespace theory {
34
35		/**
36		* The type for the Substitutions mapping output by
37		* Theory::simplify(), TheoryEngine::simplify(), and
38		* Valuation::simplify(). This is in its own header to
39		* avoid circular dependences between those three.
40		*
41		* This map is context-dependent.
42		*/
43	117070	class SubstitutionMap
44		{
45		public:
46		typedef context::CDHashMap<Node, Node> NodeMap;
47
48		typedef NodeMap::iterator iterator;
49		typedef NodeMap::const_iterator const_iterator;
50
51		private:
52		typedef std::unordered_map<Node, Node> NodeCache;
53		/** A dummy context used by this class if none is provided */
54		context::Context d_context;
55
56		/** The variables, in order of addition */
57		NodeMap d_substitutions;
58
59		/** Cache of the already performed substitutions */
60		NodeCache d_substitutionCache;
61
62		/** Has the cache been invalidated? */
63		bool d_cacheInvalidated;
64
65		/** Internal method that performs substitution */
66		Node internalSubstitute(TNode t, NodeCache& cache);
67
68		/** Helper class to invalidate cache on user pop */
69	117070	class CacheInvalidator : public context::ContextNotifyObj
70		{
71		bool& d_cacheInvalidated;
72
73		protected:
74	3034075	void contextNotifyPop() override { d_cacheInvalidated = true; }
75
76		public:
77	117070	CacheInvalidator(context::Context* context, bool& cacheInvalidated)
78	117070	: context::ContextNotifyObj(context),
79	117070	d_cacheInvalidated(cacheInvalidated)
80		{
81	117070	}
82
83		}; /* class SubstitutionMap::CacheInvalidator */
84
85		/**
86		* This object is notified on user pop and marks the SubstitutionMap's
87		* cache as invalidated.
88		*/
89		CacheInvalidator d_cacheInvalidator;
90
91		public:
92		SubstitutionMap(context::Context* context = nullptr);
93
94		/**
95		* Adds a substitution from x to t.
96		*/
97		void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
98
99		/**
100		* Merge subMap into current set of substitutions
101		*/
102		void addSubstitutions(SubstitutionMap& subMap, bool invalidateCache = true);
103
104		/**
105		* Returns true iff x is in the substitution map
106		*/
107	359	bool hasSubstitution(TNode x) const
108		{
109	359	return d_substitutions.find(x) != d_substitutions.end();
110		}
111
112		/**
113		* Returns the substitution mapping that was given for x via
114		* addSubstitution(). Note that the returned value might itself
115		* be in the map; for the actual substitution that would be
116		* performed for x, use .apply(x). This getSubstitution() function
117		* is mainly intended for constructing assertions about what has
118		* already been put in the map.
119		*/
120		TNode getSubstitution(TNode x) const
121		{
122		AssertArgument(
123		hasSubstitution(x), x, "element not in this substitution map");
124		return (*d_substitutions.find(x)).second;
125		}
126
127		/**
128		* Apply the substitutions to the node.
129		*/
130		Node apply(TNode t, bool doRewrite = false);
131
132		/**
133		* Apply the substitutions to the node.
134		*/
135		Node apply(TNode t, bool doRewrite = false) const
136		{
137		return const_cast<SubstitutionMap*>(this)->apply(t, doRewrite);
138		}
139
140	40828	iterator begin() { return d_substitutions.begin(); }
141
142	99377	iterator end() { return d_substitutions.end(); }
143
144		const_iterator begin() const { return d_substitutions.begin(); }
145
146		const_iterator end() const { return d_substitutions.end(); }
147
148		bool empty() const { return d_substitutions.empty(); }
149
150		/**
151		* Print to the output stream
152		*/
153		void print(std::ostream& out) const;
154		void debugPrint() const;
155
156		}; /* class SubstitutionMap */
157
158		inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subst) {
159		subst.print(out);
160		return out;
161		}
162
163		} // namespace theory
164
165		std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i);
166
167		} // namespace cvc5
168
169		#endif /* CVC5__THEORY__SUBSTITUTIONS_H */