From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Feb 2022 20:05:03 +0000 (-0600)
Subject: Make LFSC side condition for concat unify robust to equality with full string (#8028)
X-Git-Tag: cvc5-1.0.0~476
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=860191bdee70238fb39f6778811b99156415e3b3;p=cvc5.git

Make LFSC side condition for concat unify robust to equality with full string (#8028)

Was leading to LFSC proof checking failures.
---

diff --git a/proofs/lfsc/signatures/strings_rules.plf b/proofs/lfsc/signatures/strings_rules.plf
index af981096a..3439500b2 100644
--- a/proofs/lfsc/signatures/strings_rules.plf
+++ b/proofs/lfsc/signatures/strings_rules.plf
@@ -20,11 +20,21 @@
                    (! r (^ (sc_concat_eq s t rev) res) 
                       (holds res))))))))
 
+; Helper method for PfRule::CONCAT_UNIFY. Returns ok if s or its head is equal to s1,
+; where the head of the reverse of s is checked if rev is tt. Fails otherwise.
+(program sc_concat_head_or_self ((s term) (s1 term) (rev flag)) Ok
+  (ifequal s s1
+    ok
+    (ifequal (sc_string_head (sc_string_rev s rev)) s1
+      ok
+      (fail Ok)))
+)
+
 ; Computes whether the heads of the premise (= s t) match s1 and t1 for the
 ; PfRule::CONCAT_UNIFY rule
 (program sc_concat_unify ((s term) (t term) (s1 term) (t1 term) (rev flag)) Ok
-  (ifequal (sc_string_head (sc_string_rev s rev)) s1
-    (ifequal (sc_string_head (sc_string_rev t rev)) t1
+  (ifequal (sc_concat_head_or_self s s1 rev) ok
+    (ifequal (sc_concat_head_or_self t t1 rev) ok
       ok
       (fail Ok))
     (fail Ok)))
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index aded275b6..72d8b0cc9 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2437,6 +2437,7 @@ set(regress_1_tests
   regress1/strings/regexp001.smt2
   regress1/strings/regexp002.smt2
   regress1/strings/regexp003.smt2
+  regress1/strings/regexp-050-multiply-graft-fuzz-dd.smt2
   regress1/strings/regexp-strat-fix.smt2
   regress1/strings/reloop.smt2
   regress1/strings/repl-empty-sem.smt2
diff --git a/test/regress/regress1/strings/regexp-050-multiply-graft-fuzz-dd.smt2 b/test/regress/regress1/strings/regexp-050-multiply-graft-fuzz-dd.smt2
new file mode 100644
index 000000000..f453d933c
--- /dev/null
+++ b/test/regress/regress1/strings/regexp-050-multiply-graft-fuzz-dd.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-const y String)
+(assert (= 2 (str.len y)))
+(assert (str.in_re y (re.+ (re.range "!" "3"))))
+(assert (str.contains "1kN" y))
+(check-sat)