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, 7 insertions, 3 deletions

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 772444f90..94051a2bb 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -207,9 +207,7 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
                                      bool asLemma)
 {
   d_statistics.d_inferences << infer;
-  std::stringstream ss;
-  ss << infer;
-  sendInference(exp, eq, ss.str().c_str(), asLemma);
+  sendInference(exp, eq, toString(infer), asLemma);
 }
 
 void InferenceManager::sendInference(const InferInfo& i)
@@ -309,6 +307,12 @@ bool InferenceManager::sendSplit(Node a, Node b, const char* c, bool preq)
   return true;
 }
 
+bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq)
+{
+  d_statistics.d_inferences << infer;
+  return sendSplit(a, b, toString(infer), preq);
+}
+
 void InferenceManager::sendPhaseRequirement(Node lit, bool pol)
 {
   lit = Rewriter::rewrite(lit);