1 /*********************                                                        */
2 /*! \file term_registration_visitor.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Dejan Jovanovic, Morgan Deters, Tim King
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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 class PreRegisterVisitor {
41 
42   /** The engine */
43   TheoryEngine* d_engine;
44 
45   typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeToTheorySetMap;
46 
47   /**
48    * Map from terms to the theories that have already had this term pre-registered.
49    */
50   TNodeToTheorySetMap d_visited;
51 
52   /**
53    * A set of all theories in the term
54    */
55   theory::Theory::Set d_theories;
56 
57   /**
58    * String representation of the visited map, for debugging purposes.
59    */
60   std::string toString() const;
61 
62 public:
63 
64   /** Returned set tells us which theories there are */
65   typedef theory::Theory::Set return_type;
66 
PreRegisterVisitor(TheoryEngine * engine,context::Context * context)67   PreRegisterVisitor(TheoryEngine* engine, context::Context* context)
68   : d_engine(engine)
69   , d_visited(context)
70   , d_theories(0)
71   {}
72 
73   /**
74    * Returns true is current has already been pre-registered with both current and parent theories.
75    */
76   bool alreadyVisited(TNode current, TNode parent);
77 
78   /**
79    * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
80    */
81   void visit(TNode current, TNode parent);
82 
83   /**
84    * Marks the node as the starting literal.
85    */
start(TNode node)86   void start(TNode node) { }
87 
88   /**
89    * Notifies the engine of all the theories used.
90    */
done(TNode node)91   theory::Theory::Set done(TNode node) { return d_theories; }
92 };
93 
94 
95 /**
96  * The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to
97  * be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has
98  * been visited already, we need to visit it again, since we need to associate it with both atoms.
99  */
100 class SharedTermsVisitor {
101 
102   /** The shared terms database */
103   SharedTermsDatabase& d_sharedTerms;
104 
105   /**
106    * Cache from preprocessing of atoms.
107    */
108   typedef std::unordered_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
109   TNodeVisitedMap d_visited;
110 
111   /**
112    * String representation of the visited map, for debugging purposes.
113    */
114   std::string toString() const;
115 
116   /**
117    * The initial atom.
118    */
119   TNode d_atom;
120 
121 public:
122 
123   typedef void return_type;
124 
SharedTermsVisitor(SharedTermsDatabase & sharedTerms)125   SharedTermsVisitor(SharedTermsDatabase& sharedTerms)
126   : d_sharedTerms(sharedTerms) {}
127 
128   /**
129    * Returns true is current has already been pre-registered with both current and parent theories.
130    */
131   bool alreadyVisited(TNode current, TNode parent) const;
132 
133   /**
134    * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
135    */
136   void visit(TNode current, TNode parent);
137 
138   /**
139    * Marks the node as the starting literal.
140    */
141   void start(TNode node);
142 
143   /**
144    * Just clears the state.
145    */
146   void done(TNode node);
147 
148   /**
149    * Clears the internal state.
150    */
151   void clear();
152 };
153 
154 
155 }
156