summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp14
1 files changed, 0 insertions, 14 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 32a80a418..2c27c6054 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -266,7 +266,6 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode,
}
void TheoryEngine::finishInit() {
-
//initialize the quantifiers engine, master equality engine, model, model builder
if( d_logicInfo.isQuantified() ) {
// initialize the quantifiers engine
@@ -350,7 +349,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
d_factsAsserted(context, false),
d_preRegistrationVisitor(this, context),
d_sharedTermsVisitor(d_sharedTerms),
- d_theoryAlternatives(),
d_attr_handle(),
d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
{
@@ -2374,18 +2372,6 @@ void TheoryEngine::spendResource(ResourceManager::Resource r)
d_resourceManager->spendResource(r);
}
-void TheoryEngine::enableTheoryAlternative(const std::string& name){
- Debug("TheoryEngine::enableTheoryAlternative")
- << "TheoryEngine::enableTheoryAlternative(" << name << ")" << std::endl;
-
- d_theoryAlternatives.insert(name);
-}
-
-bool TheoryEngine::useTheoryAlternative(const std::string& name) {
- return d_theoryAlternatives.find(name) != d_theoryAlternatives.end();
-}
-
-
TheoryEngine::Statistics::Statistics(theory::TheoryId theory):
conflicts(getStatsPrefix(theory) + "::conflicts", 0),
propagations(getStatsPrefix(theory) + "::propagations", 0),
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback