diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 06:53:33 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 06:53:33 +0000 |
commit | 72f552ead344b13d90832222157b970ae3dec8ff (patch) | |
tree | b02854356d5c5f98b3873f858f38b6762135bdc1 /src/theory/term_registration_visitor.h | |
parent | 62a50760346e130345b24e8a14ad0dac0dca5d38 (diff) |
additional stuff for sharing,
Diffstat (limited to 'src/theory/term_registration_visitor.h')
-rw-r--r-- | src/theory/term_registration_visitor.h | 146 |
1 files changed, 146 insertions, 0 deletions
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h new file mode 100644 index 000000000..29269bb52 --- /dev/null +++ b/src/theory/term_registration_visitor.h @@ -0,0 +1,146 @@ +/********************* */ +/*! \file node_visitor.h + ** \verbatim + ** Original author: dejan + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + **/ + +#pragma once + +#include "context/context.h" +#include "theory/shared_terms_database.h" + +#include <ext/hash_map> + +namespace CVC4 { + +class TheoryEngine; + +/** + * Visitor that calls the apropriate theory to preregister the term. + */ +class PreRegisterVisitor { + + /** The engine */ + TheoryEngine* d_engine; + + /** + * Map from nodes to the theories that have already seen them. + */ + typedef context::CDMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; + TNodeVisitedMap d_visited; + + /** + * All the theories of the visitation. + */ + theory::Theory::Set d_theories; + + /** + * String representation of the visited map, for debugging purposes. + */ + std::string toString() const; + + /** + * Is there more than one theory involved. + */ + bool d_multipleTheories; + +public: + + /** Return type tells us if there are more than one theory or not */ + typedef bool return_type; + + PreRegisterVisitor(TheoryEngine* engine, context::Context* context) + : d_engine(engine), d_visited(context), d_theories(0) {} + + /** + * Returns true is current has already been pre-registered with both current and parent theories. + */ + bool alreadyVisited(TNode current, TNode parent) const; + + /** + * 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); + + /** + * Notifies the engine of all the theories used. + */ + bool done(TNode node); + +}; + + +/** + * The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to + * be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has + * been visited already, we need to visit it again, since we need to associate it with both atoms. + */ +class SharedTermsVisitor { + + /** The shared terms database */ + SharedTermsDatabase& d_sharedTerms; + + /** + * Cache from proprocessing of atoms. + */ + typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; + TNodeVisitedMap d_visited; + + /** + * String representation of the visited map, for debugging purposes. + */ + std::string toString() const; + + /** + * The initial atom. + */ + TNode d_atom; + +public: + + typedef void return_type; + + SharedTermsVisitor(SharedTermsDatabase& sharedTerms) + : d_sharedTerms(sharedTerms) {} + + /** + * Returns true is current has already been pre-registered with both current and parent theories. + */ + bool alreadyVisited(TNode current, TNode parent) const; + + /** + * 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); + + /** + * Just clears the state. + */ + void done(TNode node); + + /** + * Clears the internal state. + */ + void clear(); +}; + + +} |