Age | Commit message (Collapse) | Author |
|
This PR does some more cleanup of the includes.
|
|
|
|
This cleans up various interfaces of Theory now that all theories have been updated to the new standard. This includes making check non-virtual, standardizing when trigger terms are added to equality engines, and simplifications for collectModelInfo.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
This PR makes it so that the distributed model manager can be used independently of the architecture for equality engine management for theories, meaning the choice of using a separate equality engine for the model can be done in both the current distributed architecture, or the proposed central architecture (where there would be 2 equality engines, the central one and the model one). The "central model manager" on the other hand will only be combined with the central architecture. This will make it easier to test the centralized equality engine manager, since all things related to model construction can be preserved when using a central architecture.
This PR moves some of the responsibilities from the (distributed) equality engine manager to the distributed model manager, including the management of the context of the model equality engine and the allocation of its equality engine.
This PR is not intended to make any behavior changes to the current architecture.
|
|
This class is responsible for model building when using a distributed approach for equality engines.
This PR defines the class but does not yet activate it in TheoryEngine.
This includes some model-specific things from TheoryEngine which will be migrated to this class on the next PR.
|