diff options
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 45 |
1 files changed, 37 insertions, 8 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index bcb2d011b..6da47fbd8 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -136,6 +136,11 @@ private: Theory(); /** + * A unique integer identifying the theory + */ + int d_id; + + /** * The context for the Theory. */ context::Context* d_context; @@ -175,7 +180,8 @@ protected: /** * Construct a Theory. */ - Theory(context::Context* ctxt, OutputChannel& out) throw() : + Theory(int id, context::Context* ctxt, OutputChannel& out) throw() : + d_id(id), d_context(ctxt), d_facts(), d_factsResetter(*this), @@ -196,13 +202,6 @@ protected: } /** - * Get the context associated to this Theory. - */ - context::Context* getContext() const { - return d_context; - } - - /** * The output channel for the Theory. */ OutputChannel* d_out; @@ -269,6 +268,20 @@ public: static bool fullEffort(Effort e) { return e >= FULL_EFFORT; } /** + * Get the id for this Theory. + */ + int getId() const { + return d_id; + } + + /** + * Get the context associated to this Theory. + */ + context::Context* getContext() const { + return d_context; + } + + /** * Set the output channel associated to this theory. */ void setOutputChannel(OutputChannel& out) { @@ -340,6 +353,22 @@ public: } /** + * This method is called to notify a theory that the node n should be considered a "shared term" by this theory + */ + virtual void addSharedTerm(TNode n) { } + + /** + * This method is called by the shared term manager when a shared term t + * which this theory cares about (either because it received a previous + * addSharedTerm call with t or because it received a previous notifyEq call + * with t as the second argument) becomes equal to another shared term u. + * This call also serves as notice to the theory that the shared term manager + * now considers u the representative for this equivalence class of shared + * terms, so future notifications for this class will be based on u not t. + */ + virtual void notifyEq(TNode t, TNode u) { } + + /** * Check the current assignment's consistency. * * An implementation of check() is required to either: |