Refactor disequality processing in string solver (#4209)

This commit refactors disequality processing in the core string solver.
It also adds statistics for the inferences and splits in those methods.
No semantic changes intended.

1 files changed, 8 insertions, 0 deletions

diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index bd2f85d29..2a361aa44 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -184,6 +184,14 @@ class InferenceManager
    * otherwise. A split is trivial if a=b rewrites to a constant.
    */
   bool sendSplit(Node a, Node b, const char* c, bool preq = true);
+
+  /**
+   * The same as `sendSplit()` above but with an `Inference` instead of a
+   * string.  This variant updates the statistics about the number of
+   * inferences made of each type.
+   */
+  bool sendSplit(Node a, Node b, Inference infer, bool preq = true);
+
   /** Send phase requirement
    *
    * This method is called to indicate this class should send a phase