Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/term_registration_visitor.h	Lines:	3	3	100.0 %
Date:	2021-11-06	Branches:	0	0	0.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 <unordered_map>

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

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 : protected EnvObj
{
  /** 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(Env& env, TheoryEngine* engine);

  /**
   * 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(Env& env,
                          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 : protected EnvObj
{
  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(Env& env,
                     TheoryEngine* te,
                     SharedTermsDatabase& sharedTerms);

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