Generalize LFSC concat unify for splitting constants (#8077)

Was causing LFSC proof failures on ~5 SMT-LIB strings benchmarks.

diff --git a/proofs/lfsc/signatures/nary_programs.plf b/proofs/lfsc/signatures/nary_programs.plf
index f04e6ba40ec757292e19437ccf5c54ae23581a2f..97af8110dba6c7a6e47d91723ad7400aaf758f09 100644 (file)
--- a/proofs/lfsc/signatures/nary_programs.plf
+++ b/proofs/lfsc/signatures/nary_programs.plf
@@ -177,3 +177,16 @@
 (program nary_reverse ((f term) (t term) (null term)) term
   (nary_reverse_rec f t null null)
 )
+
+; Returns tt if s is a prefix of t. May fail if s or t is not in n-ary form.
+(program nary_is_prefix ((f term) (s term) (t term) (null term)) flag
+  (match s
+    ((apply s1 s2)
+      (let s12 (getarg f s1)
+      (match t
+        ((apply t1 t2)
+          (let t12 (getarg f t1)
+          (ifequal s12 t12 (nary_is_prefix f s2 t2 null) ff)))
+        (null ff))))
+    (default (ifequal s null tt ff)))
+)

diff --git a/proofs/lfsc/signatures/strings_programs.plf b/proofs/lfsc/signatures/strings_programs.plf
index 4e36fc91ffac9be4126b0ea53fec9932a09fac37..8614f953617b7514ae6e99023a3187b9a04a9e09 100644 (file)
--- a/proofs/lfsc/signatures/strings_programs.plf
+++ b/proofs/lfsc/signatures/strings_programs.plf
@@ -36,6 +36,9 @@
 ; Decompose str.++ term t into a head and tail.
 (program sc_string_decompose ((t term)) termPair (nary_decompose f_str.++ t emptystr))
 
+; String is prefix, returns tt if s is a prefix of t
+(program sc_string_is_prefix ((s term) (t term)) flag (nary_is_prefix f_str.++ s t emptystr))
+
 ; Insert a string into str.++ term t.
 (program sc_string_insert ((elem term) (t term)) term (nary_insert f_str.++ elem t emptystr))
 

diff --git a/proofs/lfsc/signatures/strings_rules.plf b/proofs/lfsc/signatures/strings_rules.plf
index 3439500b2abbeb8a9c2045680591c843de8bc9c3..301d6f77b8d7e6366956ec97af0876c569e5ae83 100644 (file)
--- a/proofs/lfsc/signatures/strings_rules.plf
+++ b/proofs/lfsc/signatures/strings_rules.plf
@@ -20,14 +20,20 @@
                    (! 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.
+; Helper method for PfRule::CONCAT_UNIFY. Returns ok if s or a prefix of its
+; head is equal to s1, where the (suffix of 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
+    (let sh (sc_string_head (sc_string_rev s rev))
+    (ifequal sh s1
       ok
-      (fail Ok)))
+      ; otherwise we may be splitting a constant, we reverse the characters in sh
+      (ifequal (sc_string_is_prefix
+                 (sc_string_rev (sc_string_nary_intro s1) rev)
+                 (sc_string_rev sh rev))
+          tt ok (fail Ok)))))
 )
 
 ; Computes whether the heads of the premise (= s t) match s1 and t1 for the

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 40414a89c2cc18f3d8490018b004ae9bdbee8b8a..ad5918ee8457277c5e440bb4596d8d91d2d7dc41 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2344,6 +2344,7 @@ set(regress_1_tests
   regress1/strings/instance1079-re-loop-cong.smt2
   regress1/strings/instance2984-null-term.smt2
   regress1/strings/instance3303-delta.smt2
+  regress1/strings/instance6561-dd-concat-unify-char.smt2
   regress1/strings/instance7075-delta.smt2
   regress1/strings/issue1105.smt2
   regress1/strings/issue1684-regex.smt2

diff --git a/test/regress/regress1/strings/instance6561-dd-concat-unify-char.smt2 b/test/regress/regress1/strings/instance6561-dd-concat-unify-char.smt2
new file mode 100644 (file)
index 0000000..13bb64e
--- /dev/null
+++ b/test/regress/regress1/strings/instance6561-dd-concat-unify-char.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-const X String)
+(assert (str.in_re X (re.++ ((_ re.loop 2 3) (re.range "a" "z")) (re.++ (str.to_re ".") (re.range "A" "Z")) (re.range "A" "Z") (re.range "a" "z"))))
+(assert (str.in_re X (re.++ (re.* re.allchar) (str.to_re "{0") (re.union (str.to_re "t") (str.to_re "f")) (str.to_re "tp"))))
+(check-sat)