From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 13 Nov 2020 02:02:20 +0000 (-0600)
Subject: Make regular expression difference left associative (#5430)
X-Git-Tag: cvc5-1.0.0~2602
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=151a4bb262713a94c488f2e4e8c1f5d498098253;p=cvc5.git

Make regular expression difference left associative (#5430)

Fixes #5428.
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 566bcc3c7..24902b888 100644
--- 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 78c6ab1f1..020cedb30 100644
--- 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 ac62452e5..ac6d91e7c 100644
--- 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
index 000000000..64455f2c3
--- /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)