diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-26 09:52:28 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-26 09:52:28 -0500 |
| commit | c9fd28a391cfff767b899a65ad365742745910fe (patch) | |
| tree | 663ffc3b744c9df9de3781aaf292fa6b79851fdc /src/theory/strings/extf_solver.h | |
| parent | 9523b4248da9764fa14f078659b42085a7fe2654 (diff) | |
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.
Diffstat (limited to 'src/theory/strings/extf_solver.h')
| -rw-r--r-- | src/theory/strings/extf_solver.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index 4c848f430..040871ffa 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -26,6 +26,7 @@ #include "theory/strings/base_solver.h" #include "theory/strings/core_solver.h" #include "theory/strings/inference_manager.h" +#include "theory/strings/sequences_stats.h" #include "theory/strings/skolem_cache.h" #include "theory/strings/solver_state.h" #include "theory/strings/theory_strings_preprocess.h" @@ -88,7 +89,8 @@ class ExtfSolver SkolemCache& skc, BaseSolver& bs, CoreSolver& cs, - ExtTheory* et); + ExtTheory* et, + SequencesStatistics& stats); ~ExtfSolver(); /** check extended functions evaluation |