From 9258aa062ebefb8af7727567470f9a387181d466 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 2 Jun 2021 12:41:14 -0700 Subject: [PATCH] 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. --- src/options/strings_options.toml | 8 -------- src/theory/strings/regexp_solver.cpp | 6 +----- test/regress/regress1/strings/regexp002.smt2 | 4 ---- 3 files changed, 1 insertion(+), 17 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 @@ -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 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 >& 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 35501ac10..7bb4e8aca 100644 --- 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) -- 2.30.2