diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-20 10:20:34 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-20 10:20:34 -0500 |
| commit | 7225f8f14ea0de0eca4c49ec3a2616196074d4d3 (patch) | |
| tree | 1abee6df10d3b5631bed1945df703621eca57c2c /test/regress | |
| parent | c010efcdea8e96f3d423d8cebdfd0f3c19a379c7 (diff) | |
Normal form equality conflicts and uniqueness check (#4497)
This adds a new inference schema to strings that was discovered by the internal proof checker. It says that we are in conflict when an equality between the normal forms of two terms in the same equivalence class rewrites to false.
It also improves the efficiency of processing normal forms by only considering normal forms that are unique up to rewriting.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/quad-028-2-2-unsat.smt2 | 21 |
2 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d5174af5e..ea98cf819 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -961,6 +961,7 @@ set(regress_0_tests regress0/strings/norn-31.smt2 regress0/strings/norn-simp-rew.smt2 regress0/strings/parser-syms.cvc + regress0/strings/quad-028-2-2-unsat.smt2 regress0/strings/re.all.smt2 regress0/strings/re-syntax.smt2 regress0/strings/re_diff.smt2 diff --git a/test/regress/regress0/strings/quad-028-2-2-unsat.smt2 b/test/regress/regress0/strings/quad-028-2-2-unsat.smt2 new file mode 100644 index 000000000..2ffe8a7a7 --- /dev/null +++ b/test/regress/regress0/strings/quad-028-2-2-unsat.smt2 @@ -0,0 +1,21 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_SLIA) +(set-info :source | +Generated by: Quang Loc Le +Generated on: 2018-10-22 +Application: Word equations in a decidable fragment +Target solver: Kepler_22 +Publication: "A decision procedure for string logic with quadratic equations, regular expressions and length constraints" by Q.L. Le and M. He, APLAS 2018. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "crafted") +(set-info :status unsat) + +(declare-fun x1 () String ) +(declare-fun x2 () String ) +(declare-fun z () String ) +(declare-fun t () String ) +(assert ( =( str.++( str.++( str.++ x1 "abc" ) x2 ) z ) ( str.++( str.++( str.++ x2 "bab" ) x1 ) t ) ) ) +(check-sat) + +(exit) |