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.cpp9
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7cf356d2c..d4e1c89c5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -561,10 +561,11 @@ bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
}
void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){
- //consult each theory to get all relevant information concerning the model
- for( int i=0; i<theory::THEORY_LAST; i++ ){
- if( d_theoryTable[i] ){
- d_theoryTable[i]->collectModelInfo( m );
+ // Consult each active theory to get all relevant information
+ // concerning the model.
+ for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
+ if(d_logicInfo.isTheoryEnabled(theoryId)) {
+ d_theoryTable[theoryId]->collectModelInfo(m);
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback