diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-18 14:44:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-18 14:44:53 -0500 |
| commit | 712f798dbcab7536c21f2e7bc5e971370d898743 (patch) | |
| tree | 4ccc3462396270f3c10fff27db0e20243492ceda /src/theory/theory_state.h | |
| parent | 41edd09dda3d18c98b6cafcf3a3c98d4155fbe19 (diff) | |
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).
Diffstat (limited to 'src/theory/theory_state.h')
0 files changed, 0 insertions, 0 deletions