Simplify heuristic in `processNEqc` (#4129)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sat, 21 Mar 2020 19:57:22 +0000 (12:57 -0700)
committerGitHub <noreply@github.com>
Sat, 21 Mar 2020 19:57:22 +0000 (14:57 -0500)
commita507aa5f1904055782e1ba01083faf1fd0fb86f7
treee31fb4ce520c26efecd1f92b5b14231c46321f59
parentd80192cf77c7beeb26c783a2f53064e2eddb654b
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