/*! \file term_registration_visitor.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
/** The engine */
TheoryEngine* d_engine;
- typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeToTheorySetMap;
+ typedef context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction>
+ TNodeToTheorySetMap;
/**
* Map from terms to the theories that have already had this term pre-registered.
/**
* A set of all theories in the term
*/
- theory::Theory::Set d_theories;
+ theory::TheoryIdSet d_theories;
/**
* String representation of the visited map, for debugging purposes.
*/
std::string toString() const;
-public:
-
+ public:
/** Returned set tells us which theories there are */
- typedef theory::Theory::Set return_type;
-
+ typedef theory::TheoryIdSet return_type;
+
PreRegisterVisitor(TheoryEngine* engine, context::Context* context)
- : d_engine(engine)
- , d_visited(context)
- , d_theories(0)
- {}
+ : d_engine(engine), d_visited(context), d_theories(0)
+ {
+ }
/**
- * Returns true is current has already been pre-registered with both current and parent theories.
+ * Returns true is current has already been pre-registered with both current
+ * and parent theories.
*/
bool alreadyVisited(TNode current, TNode parent);
-
+
/**
- * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
+ * Pre-registeres current with any of the current and parent theories that
+ * haven't seen the term yet.
*/
void visit(TNode current, TNode parent);
-
+
/**
* Marks the node as the starting literal.
*/
- void start(TNode node) { }
+ void start(TNode node) {}
/**
* Notifies the engine of all the theories used.
*/
- theory::Theory::Set done(TNode node) { return d_theories; }
+ theory::TheoryIdSet done(TNode node) { return d_theories; }
};
/**
* Cache from preprocessing of atoms.
*/
- typedef std::unordered_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
+ typedef std::unordered_map<TNode, theory::TheoryIdSet, TNodeHashFunction>
+ TNodeVisitedMap;
TNodeVisitedMap d_visited;
/**