diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-06-30 06:06:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-06-30 06:06:30 +0000 |
commit | 29cf5a3812f1edafc3c233483c65f0cc4b125295 (patch) | |
tree | 307f9c8981e5879a4a21fe26e4e89b902f29bbee /src/theory/theory_engine.h | |
parent | c64799a735cc9fecb8e618b2c66b252d7cda549d (diff) |
only use theory registration if (1) a theory requests it, or (2) if there's more than one "real" theory (not BUILTIN or BOOL) active
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2dd3db863..852eea0c4 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -74,6 +74,13 @@ class TheoryEngine { size_t d_activeTheories; /** + * Need the registration infrastructure when theory sharing is on + * (>=2 active theories) or when the sole active theory has + * requested it. + */ + bool d_needRegistration; + + /** * The type of the simplification cache. */ typedef Cache<Node, std::pair<Node, theory::Substitutions>, NodeHashFunction> SimplifyCache; @@ -194,11 +201,22 @@ class TheoryEngine { void markActive(theory::TheoryId th) { if(!d_theoryIsActive[th]) { d_theoryIsActive[th] = true; - ++d_activeTheories; - Notice() << "Theory " << th << " has been activated." << std::endl; + if(th != theory::THEORY_BUILTIN && th != theory::THEORY_BOOL) { + if(++d_activeTheories == 1) { + // theory requests registration + d_needRegistration = hasRegisterTerm(th); + } else { + // need it for sharing + d_needRegistration = true; + } + } + Notice() << "Theory " << th << " has been activated (registration is " + << (d_needRegistration ? "on" : "off") << ")." << std::endl; } } + bool hasRegisterTerm(theory::TheoryId th) const; + public: /** The logic of the problem */ std::string d_logic; |