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_engine.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_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 04f15e89f..915373074 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -80,6 +80,9 @@ class TheoryEngine { /** Our context */ context::Context* d_context; + /** Our user context */ + context::UserContext* d_userContext; + /** * A table of from theory IDs to theory pointers. Never use this table * directly, use theoryOf() instead. @@ -343,7 +346,7 @@ class TheoryEngine { public: /** Constructs a theory engine */ - TheoryEngine(context::Context* ctxt); + TheoryEngine(context::Context* context, context::UserContext* userContext); /** Destroys a theory engine */ ~TheoryEngine(); @@ -356,7 +359,7 @@ public: inline void addTheory(theory::TheoryId theoryId) { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId); - d_theoryTable[theoryId] = new TheoryClass(d_context, *d_theoryOut[theoryId], theory::Valuation(this)); + d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this)); } /** @@ -407,7 +410,8 @@ public: /** * Solve the given literal with a theory that owns it. */ - theory::Theory::SolveStatus solve(TNode literal, theory::SubstitutionMap& substitionOut); + theory::Theory::SolveStatus solve(TNode literal, + theory::SubstitutionMap& substitutionOut); /** * Preregister a Theory atom with the responsible theory (or |