diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-08 10:14:31 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-08 10:14:31 -0600 |
| commit | 564234963dd7e76c8d9b88ef941a6683694e5b53 (patch) | |
| tree | 313e46520c07d1536fffbad4b7080937cfc09aae /src/theory/theory.h | |
| parent | 805d4b7483e51a9b4d24058d493f85700a87f099 (diff) | |
Make collect model info return a Bool (#1421)
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 ){ } /** |