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.

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 958136494276c153f77423dff5da7f9b42f0b7da..8ee25c26520c9223d4d804d915f827788812512b 100644 (file)
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -25,14 +25,6 @@ name   = "Strings Theory"
   default    = "false"
   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"

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 164e4e1c056959eaa96bd3bd294a3fddbc579ed5..18815c731ee0eeae4490841c1812d0931c150f63 100644 (file)
--- 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;
       }
     }
 

diff --git a/test/regress/regress1/strings/regexp002.smt2 b/test/regress/regress1/strings/regexp002.smt2
index 35501ac1036b1d88b6f3c3cea5c298259f33f126..7bb4e8aca190bc4596af57bf41c78888032f71c0 100644 (file)
--- a/test/regress/regress1/strings/regexp002.smt2
+++ b/test/regress/regress1/strings/regexp002.smt2
@@ -2,10 +2,6 @@
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
-; this option requires user to check whether the constraint is in the fragment
-; currently we do not provide only positive membership constraint checking
-; if users use this option but the constraint is not in this fragment, the result will fail
-(set-option :strings-inm true)
 
 (declare-fun x () String)
 (declare-fun y () String)