From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sat, 21 Mar 2020 19:57:22 +0000 (-0700)
Subject: Simplify heuristic in `processNEqc` (#4129)
X-Git-Tag: cvc5-1.0.0~3459
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a507aa5f1904055782e1ba01083faf1fd0fb86f7;p=cvc5.git

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.
---

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<NormalForm>& 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<NormalForm>& normal_forms)
         {
           return;
         }
-        else if (!pinfer.empty() && pinfer.back().d_id == 1)
-        {
-          break;
-        }
       }
     }
   }