diff options
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 |