From a507aa5f1904055782e1ba01083faf1fd0fb86f7 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 21 Mar 2020 12:57:22 -0700 Subject: [PATCH] Simplify heuristic in `processNEqc` (#4129) This commit removes a special case in `CoreSolver::processNEqc()` where we stopped looking for inferences for a given normal form as soon as we found the highest priority inference (currently that an element in the normal form is empty). This effectively elevates the priority of this inference to the other inferences that are done immediately instead of being added to the `pinfer` vector that holds the possible inferences. The experiments that I've run seem to confirm that it is unnecessary to have this special case. --- src/theory/strings/core_solver.cpp | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index f250647af..447af00e8 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -953,10 +953,6 @@ void CoreSolver::processNEqc(std::vector& normal_forms) { return; } - else if (!pinfer.empty() && pinfer.back().d_id == 1) - { - break; - } //AJR: for less aggressive endpoint inference //rindex = 0; @@ -966,10 +962,6 @@ void CoreSolver::processNEqc(std::vector& normal_forms) { return; } - else if (!pinfer.empty() && pinfer.back().d_id == 1) - { - break; - } } } } -- 2.30.2