Make regular expression difference left associative (#5430)

Fixes #5428.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 566bcc3c7418847f366c1f40add6552749ad7a79..24902b8880df26eba1d31ad7f169a1af1489f978 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3248,7 +3248,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
   if (echildren.size() > 2)
   {
     if (kind == INTS_DIVISION || kind == XOR || kind == MINUS
-        || kind == DIVISION || kind == HO_APPLY)
+        || kind == DIVISION || kind == HO_APPLY || kind == REGEXP_DIFF)
     {
       // left-associative, but CVC4 internally only supports 2 args
       res = d_exprMgr->mkLeftAssociative(k, echildren);

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 78c6ab1f1d9ad15234eea5da4be0458de5ee3305..020cedb30d7153cf33b7e8c70dd74e62eccaf9f7 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -90,7 +90,7 @@ operator STRING_TO_REGEXP 1 "convert string to regexp"
 operator REGEXP_CONCAT 2: "regexp concat"
 operator REGEXP_UNION 2: "regexp union"
 operator REGEXP_INTER 2: "regexp intersection"
-operator REGEXP_DIFF 2: "regexp difference"
+operator REGEXP_DIFF 2 "regexp difference"
 operator REGEXP_STAR 1 "regexp *"
 operator REGEXP_PLUS 1 "regexp +"
 operator REGEXP_OPT 1 "regexp ?"

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ac62452e5cd4e1b2205cd639afd4fee1ae0baf44..ac6d91e7cdd690f10eb17b7cbae04b96d3b90b61 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1010,6 +1010,7 @@ set(regress_0_tests
   regress0/strings/issue4820.smt2
   regress0/strings/issue4915.smt2
   regress0/strings/issue5090.smt2
+  regress0/strings/issue5428-re-diff-assoc.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2

diff --git a/test/regress/regress0/strings/issue5428-re-diff-assoc.smt2 b/test/regress/regress0/strings/issue5428-re-diff-assoc.smt2
new file mode 100644 (file)
index 0000000..64455f2
--- /dev/null
+++ b/test/regress/regress0/strings/issue5428-re-diff-assoc.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_S)
+(set-info :status unsat)
+(assert (str.in_re "" (re.diff (re.* re.allchar) re.allchar (re.* re.allchar))))
+(check-sat)