Refactor inference manager in strings to be amenable to proofs (#4363)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 20 Apr 2020 20:16:18 +0000 (15:16 -0500)
committerGitHub <noreply@github.com>
Mon, 20 Apr 2020 20:16:18 +0000 (15:16 -0500)
commit6255c0356bd78140a9cf075491c1d4608ac27704
treea8b34f58a7dce1cd68d29ab6979fec0ec936cf82
parenta76b222149e828ed0fe7fb6e91684552dc7b64ec
Refactor inference manager in strings to be amenable to proofs (#4363)

This is a key refactoring towards proofs for strings.

This ensures that InferInfo is maintained until just before facts, lemmas and conflicts are processed. This allows us both to:
(1) track more accurate stats and debug information,
(2) have enough information to ensure that proofs can be constructed at the moment facts, lemmas, and conflicts are processed.

Changes in this PR:

PendingInfer and InferInfo were merged, CoreInferInfo is now the previous equivalent of InferInfo, extended with core-solver-specific information, which is only used by CoreSolver.
sendInference( const InferInfo& info, ... ) is now the central method for sending inferences which is called by the other variants, not the other way around.
sendLemma is inlined into sendInference(...) for clarity.
doPendingLemmas and doPendingFacts are extended to process the side effects of the inference infos.
There is actually a further issue with pending inferences related to eagerly processing the side effect of CoreInferInfo before we know the lemma is sent. I believe this issue does not occur in practice based on our strategy. Further refactoring could tighten this, e.g. virtual void InferInfo::processSideEffect. I will do this in another PR.

Further refactoring can address whether asLemma should be a field of InferInfo (it probably should), and whether we should explicitly check for AND in conclusions instead of making it the responsibility of the user of this class.
src/theory/strings/core_solver.cpp
src/theory/strings/core_solver.h
src/theory/strings/infer_info.cpp
src/theory/strings/infer_info.h
src/theory/strings/inference_manager.cpp
src/theory/strings/inference_manager.h