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
17 #include "context/context.h"
18 #include "theory/shared_terms_database.h"
20 #include <ext/hash_map>
27 * Visitor that calls the apropriate theory to preregister the term.
29 class PreRegisterVisitor
{
32 TheoryEngine
* d_engine
;
35 * Map from nodes to the theories that have already seen them.
37 typedef context::CDMap
<TNode
, theory::Theory::Set
, TNodeHashFunction
> TNodeVisitedMap
;
38 TNodeVisitedMap d_visited
;
41 * All the theories of the visitation.
43 theory::Theory::Set d_theories
;
46 * String representation of the visited map, for debugging purposes.
48 std::string
toString() const;
51 * Is there more than one theory involved.
53 bool d_multipleTheories
;
57 /** Return type tells us if there are more than one theory or not */
58 typedef bool return_type
;
60 PreRegisterVisitor(TheoryEngine
* engine
, context::Context
* context
)
61 : d_engine(engine
), d_visited(context
), d_theories(0) {}
64 * Returns true is current has already been pre-registered with both current and parent theories.
66 bool alreadyVisited(TNode current
, TNode parent
) const;
69 * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
71 void visit(TNode current
, TNode parent
);
74 * Marks the node as the starting literal.
76 void start(TNode node
);
79 * Notifies the engine of all the theories used.
81 bool done(TNode node
);
87 * The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to
88 * be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has
89 * been visited already, we need to visit it again, since we need to associate it with both atoms.
91 class SharedTermsVisitor
{
93 /** The shared terms database */
94 SharedTermsDatabase
& d_sharedTerms
;
97 * Cache from proprocessing of atoms.
99 typedef std::hash_map
<TNode
, theory::Theory::Set
, TNodeHashFunction
> TNodeVisitedMap
;
100 TNodeVisitedMap d_visited
;
103 * String representation of the visited map, for debugging purposes.
105 std::string
toString() const;
114 typedef void return_type
;
116 SharedTermsVisitor(SharedTermsDatabase
& sharedTerms
)
117 : d_sharedTerms(sharedTerms
) {}
120 * Returns true is current has already been pre-registered with both current and parent theories.
122 bool alreadyVisited(TNode current
, TNode parent
) const;
125 * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
127 void visit(TNode current
, TNode parent
);
130 * Marks the node as the starting literal.
132 void start(TNode node
);
135 * Just clears the state.
137 void done(TNode node
);
140 * Clears the internal state.