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 apropriate theory to preregister the term.
31 class PreRegisterVisitor
{
34 TheoryEngine
* d_engine
;
37 * Map from nodes to the theories that have already seen them.
39 typedef context::CDMap
<TNode
, theory::Theory::Set
, TNodeHashFunction
> TNodeVisitedMap
;
40 TNodeVisitedMap d_visited
;
43 * All the theories of the visitation.
45 theory::Theory::Set d_theories
;
48 * String representation of the visited map, for debugging purposes.
50 std::string
toString() const;
53 * Is there more than one theory involved.
55 bool d_multipleTheories
;
59 /** Return type tells us if there are more than one theory or not */
60 typedef bool return_type
;
62 PreRegisterVisitor(TheoryEngine
* engine
, context::Context
* context
)
63 : d_engine(engine
), d_visited(context
), d_theories(0) {}
66 * Returns true is current has already been pre-registered with both current and parent theories.
68 bool alreadyVisited(TNode current
, TNode parent
) const;
71 * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
73 void visit(TNode current
, TNode parent
);
76 * Marks the node as the starting literal.
78 void start(TNode node
);
81 * Notifies the engine of all the theories used.
83 bool done(TNode node
);
89 * The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to
90 * be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has
91 * been visited already, we need to visit it again, since we need to associate it with both atoms.
93 class SharedTermsVisitor
{
95 /** The shared terms database */
96 SharedTermsDatabase
& d_sharedTerms
;
99 * Cache from proprocessing of atoms.
101 typedef std::hash_map
<TNode
, theory::Theory::Set
, TNodeHashFunction
> TNodeVisitedMap
;
102 TNodeVisitedMap d_visited
;
105 * String representation of the visited map, for debugging purposes.
107 std::string
toString() const;
116 typedef void return_type
;
118 SharedTermsVisitor(SharedTermsDatabase
& sharedTerms
)
119 : d_sharedTerms(sharedTerms
) {}
122 * Returns true is current has already been pre-registered with both current and parent theories.
124 bool alreadyVisited(TNode current
, TNode parent
) const;
127 * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
129 void visit(TNode current
, TNode parent
);
132 * Marks the node as the starting literal.
134 void start(TNode node
);
137 * Just clears the state.
139 void done(TNode node
);
142 * Clears the internal state.