1 /********************* */
2 /*! \file node_visitor.h
4 ** Original author: dejan
6 ** Minor contributors (to current version):
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
15 #include "cvc4_private.h"
19 #include "context/context.h"
20 #include "theory/shared_terms_database.h"
22 #include <ext/hash_map>
29 * Visitor that calls the appropriate theory to pre-register the term. The visitor also keeps track
30 * of the sets of theories that are involved in the terms, so that it can say if there are multiple
33 * A sub-term has been visited if the theories of both the parent and the term itself have already
36 * Computation of the set of theories in the original term are computed in the alreadyVisited method
37 * so as no to skip any theories.
39 class PreRegisterVisitor
{
42 TheoryEngine
* d_engine
;
44 typedef context::CDHashMap
<TNode
, theory::Theory::Set
, TNodeHashFunction
> TNodeToTheorySetMap
;
47 * Map from terms to the theories that have already had this term pre-registered.
49 TNodeToTheorySetMap d_visited
;
52 * A set of all theories in the term
54 theory::Theory::Set d_theories
;
57 * Is true if the term we're traversing involves multiple theories.
59 bool d_multipleTheories
;
62 * String representation of the visited map, for debugging purposes.
64 std::string
toString() const;
68 /** Return type tells us if there are more than one theory or not */
69 typedef bool return_type
;
71 PreRegisterVisitor(TheoryEngine
* engine
, context::Context
* context
)
75 , d_multipleTheories(false)
79 * Returns true is current has already been pre-registered with both current and parent theories.
81 bool alreadyVisited(TNode current
, TNode parent
);
84 * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
86 void visit(TNode current
, TNode parent
);
89 * Marks the node as the starting literal.
91 void start(TNode node
);
94 * Notifies the engine of all the theories used.
96 bool done(TNode node
);
102 * The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to
103 * be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has
104 * been visited already, we need to visit it again, since we need to associate it with both atoms.
106 class SharedTermsVisitor
{
108 /** The shared terms database */
109 SharedTermsDatabase
& d_sharedTerms
;
112 * Cache from proprocessing of atoms.
114 typedef std::hash_map
<TNode
, theory::Theory::Set
, TNodeHashFunction
> TNodeVisitedMap
;
115 TNodeVisitedMap d_visited
;
118 * String representation of the visited map, for debugging purposes.
120 std::string
toString() const;
129 typedef void return_type
;
131 SharedTermsVisitor(SharedTermsDatabase
& sharedTerms
)
132 : d_sharedTerms(sharedTerms
) {}
135 * Returns true is current has already been pre-registered with both current and parent theories.
137 bool alreadyVisited(TNode current
, TNode parent
) const;
140 * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
142 void visit(TNode current
, TNode parent
);
145 * Marks the node as the starting literal.
147 void start(TNode node
);
150 * Just clears the state.
152 void done(TNode node
);
155 * Clears the internal state.