diff options
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 |