From 860191bdee70238fb39f6778811b99156415e3b3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Feb 2022 14:05:03 -0600 Subject: [PATCH] Make LFSC side condition for concat unify robust to equality with full string (#8028) Was leading to LFSC proof checking failures. --- proofs/lfsc/signatures/strings_rules.plf | 14 ++++++++++++-- test/regress/CMakeLists.txt | 1 + .../strings/regexp-050-multiply-graft-fuzz-dd.smt2 | 9 +++++++++ 3 files changed, 22 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/strings/regexp-050-multiply-graft-fuzz-dd.smt2 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) -- 2.30.2