summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-07-20 13:28:01 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-07-20 13:28:01 -0500
commitf827fb06c949d421fb32f6629c2c353ca7bd026e (patch)
tree04b3563aa2467784517193dd22ef95f2ce1e612a /src/theory/theory_engine.h
parentdaf2eca9a4bb32680cbf35945bb09cfd13be76a7 (diff)
Infrastructure for storing and printing heap models for separation logic. Ensure value of sep.nil is correct in models. Print instantiations as sexprs.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r--src/theory/theory_engine.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index aae6fce17..eed58864a 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -711,7 +711,8 @@ public:
* collect model info
*/
void collectModelInfo( theory::TheoryModel* m, bool fullModel );
- void collectModelComments( theory::TheoryModel* m );
+ /** post process model */
+ void postProcessModel( theory::TheoryModel* m );
/**
* Get the current model
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback