Remove option to ignore negative memberships (#6665)

Fixes #6661. The option `--strings-inm` could be used to ignore negative
membership constraints. However, this option made the string solver
model-unsound or produced incorrect models if the user provided a
benchmark that actually contained negative membership constraints. The
solver did not check for negative membership constraints and did not
warn the user about them. Because the option is not really being used,
this commit removes it.

2 files changed, 1 insertions, 13 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 958136494..8ee25c265 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -26,14 +26,6 @@ name   = "Strings Theory"
   help       = "strings eager check"
 
 [[option]]
-  name       = "stringIgnNegMembership"
-  category   = "regular"
-  long       = "strings-inm"
-  type       = "bool"
-  default    = "false"
-  help       = "internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now)"
-
-[[option]]
   name       = "stringLazyPreproc"
   category   = "regular"
   long       = "strings-lazy-pp"
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 164e4e1c0..18815c731 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -125,11 +125,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
     {
       for (const Node& m : mr.second)
       {
-        bool polarity = m.getKind() != NOT;
-        if (polarity || !options::stringIgnNegMembership())
-        {
-          allMems[m] = mr.first;
-        }
+        allMems[m] = mr.first;
       }
     }