Add stats for string reductions, lemmas and conflicts (#4149)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 26 Mar 2020 14:52:28 +0000 (09:52 -0500)
committerGitHub <noreply@github.com>
Thu, 26 Mar 2020 14:52:28 +0000 (09:52 -0500)
commitc9fd28a391cfff767b899a65ad365742745910fe
tree663ffc3b744c9df9de3781aaf292fa6b79851fdc
parent9523b4248da9764fa14f078659b42085a7fe2654
Add stats for string reductions, lemmas and conflicts (#4149)

This PR adds comprehensive stats for reductions, lemmas and conflicts in TheoryStrings. Remaining stats will track all inferences (which are finer grained steps that may lead to lemmas/conflicts).

Additionally this PR refactors calls to OutputChannel::lemma in TheoryStrings / InferenceManager. There are now only 2 calls to lemma(...) during registerTerm(...), one for "atomic" string terms (corresponding to length splits typically) and one for non-atomic terms.
src/theory/strings/core_solver.cpp
src/theory/strings/extf_solver.cpp
src/theory/strings/extf_solver.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/theory_strings.cpp
src/theory/strings/theory_strings_preprocess.cpp
src/theory/strings/theory_strings_preprocess.h