diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
commit | c94347913fa464b1ec6a3da2ab21e319c0c42e02 (patch) | |
tree | 6c8252385365e5dacc86ce8c364c3d06332d39a7 /src/theory/theory.h | |
parent | 7adcbaf2eac82be6ca8cf1569bab80c961710950 (diff) |
Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model gen also.
I also expect this commit to fix bug #273.
No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 26 |
1 files changed, 20 insertions, 6 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 931b1155e..17c9ef14a 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -103,6 +103,11 @@ private: context::Context* d_context; /** + * The user context for the Theory. + */ + context::UserContext* d_userContext; + + /** * The assertFact() queue. * * These can not be TNodes as some atoms (such as equalities) are sent @@ -133,13 +138,15 @@ protected: /** * Construct a Theory. */ - Theory(TheoryId id, context::Context* ctxt, OutputChannel& out, Valuation valuation) throw() : + Theory(TheoryId id, context::Context* context, context::UserContext* userContext, + OutputChannel& out, Valuation valuation) throw() : d_id(id), - d_context(ctxt), - d_facts(ctxt), - d_factsHead(ctxt, 0), - d_sharedTermsIndex(ctxt, 0), - d_sharedTerms(ctxt), + d_context(context), + d_userContext(userContext), + d_facts(context), + d_factsHead(context, 0), + d_sharedTermsIndex(context, 0), + d_sharedTerms(context), d_out(&out), d_valuation(valuation) { @@ -328,6 +335,13 @@ public: } /** + * Get the context associated to this Theory. + */ + context::UserContext* getUserContext() const { + return d_userContext; + } + + /** * Set the output channel associated to this theory. */ void setOutputChannel(OutputChannel& out) { |