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

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_registration_visitor.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Andrew Reynolds, Morgan Deters
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** [[ Add lengthier description here ]]
13
 ** \todo document this file
14
 **/
15
16
#include "cvc4_private.h"
17
18
#pragma once
19
20
#include "context/context.h"
21
#include "theory/shared_terms_database.h"
22
23
#include <unordered_map>
24
25
namespace CVC4 {
26
27
class TheoryEngine;
28
29
/**
30
 * Visitor that calls the appropriate theory to pre-register the term. The visitor also keeps track
31
 * of the sets of theories that are involved in the terms, so that it can say if there are multiple
32
 * theories involved.
33
 *
34
 * A sub-term has been visited if the theories of both the parent and the term itself have already
35
 * visited this term.
36
 *
37
 * Computation of the set of theories in the original term are computed in the alreadyVisited method
38
 * so as no to skip any theories.
39
 */
40
8992
class PreRegisterVisitor {
41
42
  /** The engine */
43
  TheoryEngine* d_engine;
44
45
  typedef context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction>
46
      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
8995
  PreRegisterVisitor(TheoryEngine* engine, context::Context* c)
63
8995
      : d_engine(engine), d_visited(c)
64
  {
65
8995
  }
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
124736
  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
8992
class SharedTermsVisitor {
131
  using TNodeVisitedMap =
132
      std::unordered_map<TNode, theory::TheoryIdSet, TNodeHashFunction>;
133
  using TNodeToTheorySetMap =
134
      context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction>;
135
  /**
136
   * String representation of the visited map, for debugging purposes.
137
   */
138
  std::string toString() const;
139
140
  /**
141
   * The initial atom.
142
   */
143
  TNode d_atom;
144
145
 public:
146
  /** required to instantiate template for NodeVisitor */
147
  using return_type = void;
148
149
8995
  SharedTermsVisitor(TheoryEngine* te,
150
                     SharedTermsDatabase& sharedTerms,
151
                     context::Context* c)
152
8995
      : d_engine(te), d_sharedTerms(sharedTerms), d_preregistered(c)
153
  {
154
8995
  }
155
156
  /**
157
   * Returns true is current has already been pre-registered with both current and parent theories.
158
   */
159
  bool alreadyVisited(TNode current, TNode parent) const;
160
161
  /**
162
   * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
163
   */
164
  void visit(TNode current, TNode parent);
165
166
  /**
167
   * Marks the node as the starting literal, which clears the state.
168
   */
169
  void start(TNode node);
170
171
  /**
172
   * Just clears the state.
173
   */
174
  void done(TNode node);
175
176
  /**
177
   * Clears the internal state.
178
   */
179
  void clear();
180
181
 private:
182
  /** The engine */
183
  TheoryEngine* d_engine;
184
  /** The shared terms database */
185
  SharedTermsDatabase& d_sharedTerms;
186
  /** Cache of nodes we have visited in this traversal */
187
  TNodeVisitedMap d_visited;
188
  /** (Global) cache of nodes we have preregistered in this SAT context */
189
  TNodeToTheorySetMap d_preregistered;
190
};
191
192
193
}