Connect the shared solver to theory engine (#5103)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 26 Sep 2020 15:07:42 +0000 (10:07 -0500)
committerGitHub <noreply@github.com>
Sat, 26 Sep 2020 15:07:42 +0000 (10:07 -0500)
commit1fe9c2efe36b126c70097b0f83db5654e0abcabe
tree46323cb7c712618a974092bced6f66dd07be3862
parent6ad02b5e0599149e0bd1548855aec8ac890f5a87
Connect the shared solver to theory engine (#5103)

This makes SharedSolver the main communication point for TheoryEngine during solving for combination-related solving tasks. This class is a generalization of SharedTermsDatabase, and in the distributed architecture is a wrapper around shared terms database.

It has 5 callbacks in theory engine: for preregistration, preNotifyFact (which calls addSharedTerms on theories), assertSharedEquality, explain, getEqualityStatus.

This PR has no intended behavior changes.

FYI @barrettcw
src/theory/combination_engine.cpp
src/theory/combination_engine.h
src/theory/ee_manager.cpp
src/theory/ee_manager.h
src/theory/ee_manager_distributed.cpp
src/theory/ee_manager_distributed.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h