diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-08-01 23:56:27 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-01 23:56:27 -0700 |
| commit | 475985ccc80b1ddb38d912a3c6658912f1fc6207 (patch) | |
| tree | ffc5cf8164e9bbc8a1e2edf169833463b26df693 /test/regress/regress0 | |
| parent | 5be889668bfb52d6705c2dc37ec05c291c7c9445 (diff) | |
Ensure strict length constraint for decompose rule (#4821)
Fixes #4820. The performance issue was caused by
0988217562006d3f59e01dc261f39121df6d75f5. That commit introduced an
option (`--strings-len-conc`) that optionally moves the length
constraint for skolems to the conclusion of an inference instead of
making it part of the term registration. However, for
`DEQ_DISL_STRINGS_SPLIT`, we were only asserting that `LENGTH_GEQ_ONE`
in the case where this option was not enabled, instead of asserting that
the length of the skolem is equal to the component on the other side of
the disequality. This lead to an infinite loop of inferences because we
effectively were just splitting a component into two skolems and the
only restriction was that the first one was non-empty. We guessed the
second skolem to be empty, so the first skolem was equal to the
component, the skolem was marked congruent, and we ended up with the
same normal form as before.
The commit fixes the issue by adding an argument to
`getDecomposeConclusion()` that specifies whether to add the length
constraint or not. This option is used to always add the length
constraint in the case of `DEQ_DISL_STRINGS_SPLIT`.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/strings/issue4820.smt2 | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/issue4820.smt2 b/test/regress/regress0/strings/issue4820.smt2 new file mode 100644 index 000000000..0bf0fac65 --- /dev/null +++ b/test/regress/regress0/strings/issue4820.smt2 @@ -0,0 +1,15 @@ +; EXPECT: sat +(set-logic QF_S) +(declare-fun _substvar_270_ () String) +(declare-fun _substvar_273_ () Bool) +(declare-fun _substvar_275_ () Bool) +(declare-fun _substvar_293_ () Bool) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const Str3 String) +(declare-const Str7 String) +(declare-const Str15 String) +(assert (or (xor true true (xor v0 v3 false v1 false v2 v2 v1 false v2 v1) true true (=> (or v1 (distinct Str15 _substvar_270_ Str3 (str.++ Str7 Str7)) v2) false) false true) _substvar_275_)) +(check-sat) |