From 49c5a2aef84d1c17b4401eae9c60a92190b0b5a7 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 6 Apr 2020 13:56:35 -0700 Subject: 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. --- src/theory/strings/inference_manager.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'src/theory/strings/inference_manager.cpp') 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& 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); -- cgit v1.2.3