Do RE derivation inference only for concrete constant RE (#4609)

The RE derive inference was not designed to handle re.comp. This makes the application of this inference more conservative.

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index db7e2d8364774605fac0297ca925bb6a802dc007..c9cee97a034bada068209ccc5873e9e25a716cdd 100644 (file)
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -599,7 +599,8 @@ bool RegExpSolver::deriveRegExp(Node x,
   Trace("regexp-derive") << "RegExpSolver::deriveRegExp: x=" << x
                          << ", r= " << r << std::endl;
   CVC4::String s = getHeadConst(x);
-  if (!s.empty() && d_regexp_opr.checkConstRegExp(r))
+  // only allow RE_DERIVE for concrete constant regular expressions
+  if (!s.empty() && d_regexp_opr.getRegExpConstType(r) == RE_C_CONRETE_CONSTANT)
   {
     Node conc = Node::null();
     Node dc = r;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 69378a5598020114e3e0fd00db4684b61267b77b..fb0b381431ab1097b145a13145217d4599358d88 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1774,6 +1774,7 @@ set(regress_1_tests
   regress1/strings/issue3357.smt2
   regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
   regress1/strings/issue4379.smt2
+  regress1/strings/issue4608-re-derive.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress1/strings/issue4608-re-derive.smt2 b/test/regress/regress1/strings/issue4608-re-derive.smt2
new file mode 100644 (file)
index 0000000..c11f7de
--- /dev/null
+++ b/test/regress/regress1/strings/issue4608-re-derive.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_S)
+(set-info :status sat)
+(declare-fun a () String)
+(assert (str.in_re (str.++ "AB" a) (re.inter (re.comp (str.to_re "AB")) 
+(re.* (re.diff (str.to_re "AB") (str.to_re ""))))))
+(check-sat)