summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-07-06 13:33:55 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-07-06 13:33:55 -0500
commit673bb476c2a1b51abbc95acb0afaf4e3b8a9feb7 (patch)
treeff5b597fe15afaeb83eae9e32d732f6bf27bff67 /src/theory/theory_engine.cpp
parentcbc5adb5d4f131ea6bf9a40b0c27fecf67353b4d (diff)
Add comment field for model, resolves hack for printing sep logic models.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f6894e07b..913a6800b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -796,6 +796,15 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
}
}
+void TheoryEngine::collectModelComments( theory::TheoryModel* m ){
+ for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
+ if(d_logicInfo.isTheoryEnabled(theoryId)) {
+ Trace("model-builder-debug") << " CollectModelComments on theory: " << theoryId << endl;
+ d_theoryTable[theoryId]->collectModelComments( m );
+ }
+ }
+}
+
/* get model */
TheoryModel* TheoryEngine::getModel() {
return d_curr_model;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback