From 564234963dd7e76c8d9b88ef941a6683694e5b53 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 8 Dec 2017 10:14:31 -0600 Subject: Make collect model info return a Bool (#1421) --- src/theory/theory.h | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/theory/theory.h') 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 ){ } /** -- cgit v1.2.3