diff options
Diffstat (limited to 'src/theory/theory.h')
| -rw-r--r-- | src/theory/theory.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 0f820ac8e..204c514a9 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -512,9 +512,11 @@ public: * Get all relevant information in this theory regarding the current * model. This should be called after a call to check( FULL_EFFORT ) * for all theories with no conflicts and no lemmas added. + * + * This method returns true if and only if the equality engine of m is + * consistent as a result of this call. */ - virtual void collectModelInfo( TheoryModel* m ){ } - + virtual bool collectModelInfo(TheoryModel* m) { return true; } /** if theories want to do something with model after building, do it here */ virtual void postProcessModel( TheoryModel* m ){ } /** |