1 /********************* */
2 /*! \file term_registration_visitor.h
4 ** Original author: Dejan Jovanovic
5 ** Major contributors: none
6 ** Minor contributors (to current version): Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** [[ Add lengthier description here ]]
13 ** \todo document this file
16 #include "cvc4_private.h"
20 #include "context/context.h"
21 #include "theory/shared_terms_database.h"
23 #include <ext/hash_map>
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
34 * A sub-term has been visited if the theories of both the parent and the term itself have already
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.
40 class PreRegisterVisitor
{
43 TheoryEngine
* d_engine
;
45 typedef context::CDHashMap
<TNode
, theory::Theory::Set
, TNodeHashFunction
> TNodeToTheorySetMap
;
48 * Map from terms to the theories that have already had this term pre-registered.
50 TNodeToTheorySetMap d_visited
;
53 * A set of all theories in the term
55 theory::Theory::Set d_theories
;
58 * String representation of the visited map, for debugging purposes.
60 std::string
toString() const;
64 /** Returned set tells us which theories there are */
65 typedef theory::Theory::Set return_type
;
67 PreRegisterVisitor(TheoryEngine
* engine
, context::Context
* context
)
74 * Returns true is current has already been pre-registered with both current and parent theories.
76 bool alreadyVisited(TNode current
, TNode parent
);
79 * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
81 void visit(TNode current
, TNode parent
);
84 * Marks the node as the starting literal.
86 void start(TNode node
) { }
89 * Notifies the engine of all the theories used.
91 theory::Theory::Set
done(TNode node
) { return d_theories
; }
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.
100 class SharedTermsVisitor
{
102 /** The shared terms database */
103 SharedTermsDatabase
& d_sharedTerms
;
106 * Cache from preprocessing of atoms.
108 typedef std::hash_map
<TNode
, theory::Theory::Set
, TNodeHashFunction
> TNodeVisitedMap
;
109 TNodeVisitedMap d_visited
;
112 * String representation of the visited map, for debugging purposes.
114 std::string
toString() const;
123 typedef void return_type
;
125 SharedTermsVisitor(SharedTermsDatabase
& sharedTerms
)
126 : d_sharedTerms(sharedTerms
) {}
129 * Returns true is current has already been pre-registered with both current and parent theories.
131 bool alreadyVisited(TNode current
, TNode parent
) const;
134 * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
136 void visit(TNode current
, TNode parent
);
139 * Marks the node as the starting literal.
141 void start(TNode node
);
144 * Just clears the state.
146 void done(TNode node
);
149 * Clears the internal state.