diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-04 15:18:12 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-04 15:18:12 -0500 |
commit | a635120676d265b27fa7c49d86d16a3e6d96174e (patch) | |
tree | 978e5e4c8a688fde4a5b152937caea864bedba53 /src/theory/theory_model_builder.h | |
parent | d367c9f9b299a15fb970d62df04d3df22b7ca08d (diff) |
Minor improvements to theory model builder interface. (#2408)
Diffstat (limited to 'src/theory/theory_model_builder.h')
-rw-r--r-- | src/theory/theory_model_builder.h | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index 68e8c6b49..bff230b5c 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -68,13 +68,14 @@ class TheoryEngineModelBuilder : public ModelBuilder * are building fails to satisfy a quantified formula. */ bool buildModel(Model* m) override; - /** Debug check model. + + /** postprocess model * - * This throws an assertion failure if the model - * contains an equivalence class with two terms t1 and t2 - * such that t1^M != t2^M. + * This is called when m is a model that will be returned to the user. This + * method checks the internal consistency of the model if we are in a debug + * build. */ - void debugCheckModel(Model* m); + void postProcessModel(bool incomplete, Model* m); protected: /** pointer to theory engine */ @@ -102,6 +103,13 @@ class TheoryEngineModelBuilder : public ModelBuilder virtual void debugModel(TheoryModel* m) {} //-----------------------------------end virtual functions + /** Debug check model. + * + * This throws an assertion failure if the model contains an equivalence + * class with two terms t1 and t2 such that t1^M != t2^M. + */ + void debugCheckModel(TheoryModel* m); + /** is n assignable? * * A term n is assignable if its value |