(proof-new) Update the strings inference manager for proofs (#5220)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 29 Oct 2020 15:00:08 +0000 (10:00 -0500)
committerGitHub <noreply@github.com>
Thu, 29 Oct 2020 15:00:08 +0000 (10:00 -0500)
commit6898ab93a3858e78b20af38e537fe48ee9140c58
treea2458fef28a0137110b4326fe7052701b56c9b8e
parent0cebb4e9b2a5caa8fafa6ebd562a25aa18de9d43
(proof-new) Update the strings inference manager for proofs (#5220)

This updates the inference manager in strings in two ways:
(1) It now inherits from InferenceManagerBuffered, meaning that the custom methods for process the current pending lemma/fact vectors are removed in favor of the standard ones.
(2) It has support for proof generation via the InferProofCons utility.

This PR standardizes three methods processFact, processLemma, and processConflict which take InferInfo and processes any string-specific behavior pertaining to processing facts, lemmas and conflicts with the inference manager. These methods are intended to preserve the previous behavior of this class.
src/theory/strings/core_solver.cpp
src/theory/strings/infer_info.cpp
src/theory/strings/infer_info.h
src/theory/strings/inference_manager.cpp
src/theory/strings/inference_manager.h
src/theory/strings/sequences_stats.cpp
src/theory/strings/sequences_stats.h
src/theory/strings/solver_state.cpp
src/theory/strings/solver_state.h
src/theory/strings/theory_strings.cpp