Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/term_registration_visitor.h	Lines:	9	9	100.0 %
Date:	2021-08-03	Branches:	1	2	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Dejan Jovanovic, Andrew Reynolds
 *
 * 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 lengthier description here ]]
 * \todo document this file
 */

#include "cvc5_private.h"

#pragma once

#include "context/context.h"
#include "theory/shared_terms_database.h"

#include <unordered_map>

namespace cvc5 {

class TheoryEngine;

/**
 * Visitor that calls the appropriate theory to pre-register the term. The visitor also keeps track
 * of the sets of theories that are involved in the terms, so that it can say if there are multiple
 * theories involved.
 *
 * A sub-term has been visited if the theories of both the parent and the term itself have already
 * visited this term.
 *
 * Computation of the set of theories in the original term are computed in the alreadyVisited method
 * so as no to skip any theories.
 */
class PreRegisterVisitor {

  /** The engine */
  TheoryEngine* d_engine;

  typedef context::CDHashMap<TNode, theory::TheoryIdSet> TNodeToTheorySetMap;

  /**
   * Map from terms to the theories that have already had this term pre-registered.
   */
  TNodeToTheorySetMap d_visited;

  /**
   * String representation of the visited map, for debugging purposes.
   */
  std::string toString() const;

 public:
  /** required to instantiate template for NodeVisitor */
  using return_type = void;

  PreRegisterVisitor(TheoryEngine* engine, context::Context* c)
      : d_engine(engine), d_visited(c)
  {
  }

  /**
   * Returns true is current has already been pre-registered with both current
   * and parent theories.
   */
  bool alreadyVisited(TNode current, TNode parent);

  /**
   * Pre-registeres current with any of the current and parent theories that
   * haven't seen the term yet.
   */
  void visit(TNode current, TNode parent);

  /**
   * Marks the node as the starting literal, which does nothing. This method
   * is required to instantiate template for NodeVisitor.
   */
  void start(TNode node);

  /** Called when the visitor is finished with a term, do nothing */
  void done(TNode node) {}

  /**
   * Preregister the term current occuring under term parent.  This calls
   * Theory::preRegisterTerm for the theories of current and parent, as well
   * as the theory of current's type, if it is finite.
   *
   * This method takes a set of theories visitedTheories that have already
   * preregistered current and updates this set with the theories that
   * preregister current during this call
   *
   * @param te Pointer to the theory engine containing the theories
   * @param visitedTheories The theories that have already preregistered current
   * @param current The term to preregister
   * @param parent The parent term of current
   * @param preregTheories The theories that have already preregistered current.
   * If there is no theory sharing, this coincides with visitedTheories.
   * Otherwise, visitedTheories may be a subset of preregTheories.
   */
  static void preRegister(TheoryEngine* te,
                          theory::TheoryIdSet& visitedTheories,
                          TNode current,
                          TNode parent,
                          theory::TheoryIdSet preregTheories);

 private:
  /**
   * Helper for above, called whether we wish to register a term with a theory
   * given by an identifier id.
   */
  static void preRegisterWithTheory(TheoryEngine* te,
                                    theory::TheoryIdSet& visitedTheories,
                                    theory::TheoryId id,
                                    TNode current,
                                    TNode parent,
                                    theory::TheoryIdSet preregTheories);
};


/**
 * The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to
 * be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has
 * been visited already, we need to visit it again, since we need to associate it with both atoms.
 */
class SharedTermsVisitor {
  using TNodeVisitedMap = std::unordered_map<TNode, theory::TheoryIdSet>;
  using TNodeToTheorySetMap = context::CDHashMap<TNode, theory::TheoryIdSet>;
  /**
   * String representation of the visited map, for debugging purposes.
   */
  std::string toString() const;

  /**
   * The initial atom.
   */
  TNode d_atom;

 public:
  /** required to instantiate template for NodeVisitor */
  using return_type = void;

  SharedTermsVisitor(TheoryEngine* te,
                     SharedTermsDatabase& sharedTerms,
                     context::Context* c)
      : d_engine(te), d_sharedTerms(sharedTerms), d_preregistered(c)
  {
  }

  /**
   * Returns true is current has already been pre-registered with both current and parent theories.
   */
  bool alreadyVisited(TNode current, TNode parent) const;

  /**
   * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
   */
  void visit(TNode current, TNode parent);

  /**
   * Marks the node as the starting literal, which clears the state.
   */
  void start(TNode node);

  /**
   * Just clears the state.
   */
  void done(TNode node);

  /**
   * Clears the internal state.
   */
  void clear();

 private:
  /** The engine */
  TheoryEngine* d_engine;
  /** The shared terms database */
  SharedTermsDatabase& d_sharedTerms;
  /** Cache of nodes we have visited in this traversal */
  TNodeVisitedMap d_visited;
  /** (Global) cache of nodes we have preregistered in this SAT context */
  TNodeToTheorySetMap d_preregistered;
};

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Dejan Jovanovic, Andrew Reynolds
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 lengthier description here ]]
14		* \todo document this file
15		*/
16
17		#include "cvc5_private.h"
18
19		#pragma once
20
21		#include "context/context.h"
22		#include "theory/shared_terms_database.h"
23
24		#include <unordered_map>
25
26		namespace cvc5 {
27
28		class TheoryEngine;
29
30		/**
31		* Visitor that calls the appropriate theory to pre-register the term. The visitor also keeps track
32		* of the sets of theories that are involved in the terms, so that it can say if there are multiple
33		* theories involved.
34		*
35		* A sub-term has been visited if the theories of both the parent and the term itself have already
36		* visited this term.
37		*
38		* Computation of the set of theories in the original term are computed in the alreadyVisited method
39		* so as no to skip any theories.
40		*/
41	9841	class PreRegisterVisitor {
42
43		/** The engine */
44		TheoryEngine* d_engine;
45
46		typedef context::CDHashMap<TNode, theory::TheoryIdSet> TNodeToTheorySetMap;
47
48		/**
49		* Map from terms to the theories that have already had this term pre-registered.
50		*/
51		TNodeToTheorySetMap d_visited;
52
53		/**
54		* String representation of the visited map, for debugging purposes.
55		*/
56		std::string toString() const;
57
58		public:
59		/** required to instantiate template for NodeVisitor */
60		using return_type = void;
61
62	9841	PreRegisterVisitor(TheoryEngine* engine, context::Context* c)
63	9841	: d_engine(engine), d_visited(c)
64		{
65	9841	}
66
67		/**
68		* Returns true is current has already been pre-registered with both current
69		* and parent theories.
70		*/
71		bool alreadyVisited(TNode current, TNode parent);
72
73		/**
74		* Pre-registeres current with any of the current and parent theories that
75		* haven't seen the term yet.
76		*/
77		void visit(TNode current, TNode parent);
78
79		/**
80		* Marks the node as the starting literal, which does nothing. This method
81		* is required to instantiate template for NodeVisitor.
82		*/
83		void start(TNode node);
84
85		/** Called when the visitor is finished with a term, do nothing */
86	210516	void done(TNode node) {}
87
88		/**
89		* Preregister the term current occuring under term parent. This calls
90		* Theory::preRegisterTerm for the theories of current and parent, as well
91		* as the theory of current's type, if it is finite.
92		*
93		* This method takes a set of theories visitedTheories that have already
94		* preregistered current and updates this set with the theories that
95		* preregister current during this call
96		*
97		* @param te Pointer to the theory engine containing the theories
98		* @param visitedTheories The theories that have already preregistered current
99		* @param current The term to preregister
100		* @param parent The parent term of current
101		* @param preregTheories The theories that have already preregistered current.
102		* If there is no theory sharing, this coincides with visitedTheories.
103		* Otherwise, visitedTheories may be a subset of preregTheories.
104		*/
105		static void preRegister(TheoryEngine* te,
106		theory::TheoryIdSet& visitedTheories,
107		TNode current,
108		TNode parent,
109		theory::TheoryIdSet preregTheories);
110
111		private:
112		/**
113		* Helper for above, called whether we wish to register a term with a theory
114		* given by an identifier id.
115		*/
116		static void preRegisterWithTheory(TheoryEngine* te,
117		theory::TheoryIdSet& visitedTheories,
118		theory::TheoryId id,
119		TNode current,
120		TNode parent,
121		theory::TheoryIdSet preregTheories);
122		};
123
124
125		/**
126		* The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to
127		* be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has
128		* been visited already, we need to visit it again, since we need to associate it with both atoms.
129		*/
130	9841	class SharedTermsVisitor {
131		using TNodeVisitedMap = std::unordered_map<TNode, theory::TheoryIdSet>;
132		using TNodeToTheorySetMap = context::CDHashMap<TNode, theory::TheoryIdSet>;
133		/**
134		* String representation of the visited map, for debugging purposes.
135		*/
136		std::string toString() const;
137
138		/**
139		* The initial atom.
140		*/
141		TNode d_atom;
142
143		public:
144		/** required to instantiate template for NodeVisitor */
145		using return_type = void;
146
147	9841	SharedTermsVisitor(TheoryEngine* te,
148		SharedTermsDatabase& sharedTerms,
149		context::Context* c)
150	9841	: d_engine(te), d_sharedTerms(sharedTerms), d_preregistered(c)
151		{
152	9841	}
153
154		/**
155		* Returns true is current has already been pre-registered with both current and parent theories.
156		*/
157		bool alreadyVisited(TNode current, TNode parent) const;
158
159		/**
160		* Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
161		*/
162		void visit(TNode current, TNode parent);
163
164		/**
165		* Marks the node as the starting literal, which clears the state.
166		*/
167		void start(TNode node);
168
169		/**
170		* Just clears the state.
171		*/
172		void done(TNode node);
173
174		/**
175		* Clears the internal state.
176		*/
177		void clear();
178
179		private:
180		/** The engine */
181		TheoryEngine* d_engine;
182		/** The shared terms database */
183		SharedTermsDatabase& d_sharedTerms;
184		/** Cache of nodes we have visited in this traversal */
185		TNodeVisitedMap d_visited;
186		/** (Global) cache of nodes we have preregistered in this SAT context */
187		TNodeToTheorySetMap d_preregistered;
188		};
189
190		} // namespace cvc5