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.
CVC4 · Jun 15, 2020 · 5de97c3 · 5de97c3
1 parent 60ed666
commit 5de97c3
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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)