Standardize collectModelInfo and theory-specific collectRelevantTerms (#4909)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 18 Aug 2020 19:44:53 +0000 (14:44 -0500)
committerGitHub <noreply@github.com>
Tue, 18 Aug 2020 19:44:53 +0000 (14:44 -0500)
commit712f798dbcab7536c21f2e7bc5e971370d898743
tree4ccc3462396270f3c10fff27db0e20243492ceda
parent41edd09dda3d18c98b6cafcf3a3c98d4155fbe19
Standardize collectModelInfo and theory-specific collectRelevantTerms (#4909)

This is work towards a configurable approach to equality engine management. This PR does not change any behavior, it only reorganizes the code.

This PR introduces the standard template for collectModelInfo, which isolates the usage of equality engine in relation to the model. In the future, theories will be encouraged to use the standard template for collectModelInfo and override collectRelevantTerms/collectModelValues only. This is to allow custom theory-independent modifications to building models (e.g. don't assert equality engine to model if we are using a centralized approach).

This PR standardizes TheoryArrays and TheoryDatatypes custom implementation of collectRelevantTerms as work towards using the standard template for collectModelInfo. Notice this required separating two portions of a loop in TheoryArrays::collectModelInfo which was doing two different things (collecting arrays and relevant terms).
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/theory_datatypes.h
src/theory/theory.cpp
src/theory/theory.h