String formulae #250

serras · 2021-08-24T08:41:05Z

This PR adds initial support for strings, the only available operations are creation of constants and equality. A concrete implementation of the theory for Z3 is also provided.

Note: there are some attempts at implementing the theory for SMTInterpol. However, this comment suggests that the string theory is not really supported. For that reason, those changes have been reverted (but you may want to squash everything).

kfriedberger

I like this PR. Overall it is clean and simple.
It would be nice to merge after fixing a few small points:

the set of supported methods from String theory. Maybe we should add some more operations, like concat, length, and lessThan/greaterThan.
missing tests.

src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java

src/org/sosy_lab/java_smt/api/StringFormulaManager.java

kfriedberger · 2021-08-24T20:16:12Z

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

-                + Native.sortToString(z3context, pSort)
-                + " with sort "
-                + sortKind);
+        if (Native.isStringSort(z3context, pSort)) {


Is there an enum value for Z3_STRING_SORT? I could only find Z3_RE_SORT, is this the same sort and would match here, too?

src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java

serras · 2021-10-29T12:00:29Z

@kfriedberger I've updated the PR with your suggestions (both in code and more tests), and I've gone all the way to also introduce regular expressions.

Please always apply 'ant format-diff' before committing to avoid such changes later.

And simple JUnit tests.

… Strings or Regexs, add range operations.

There are several operations on Strings and Regexs and the number of JUnit tests might increase.

…arameters. This fulfills our Checkstyle criteria.

- more documentation - reduced visibility, - move solver-independent code into abstract superclass

CVC4 seems to support the full range of String and Regex operations, so JavaSMT can provide them. We should add some more tests for String theory.

kfriedberger · 2021-11-14T12:27:11Z

Current status of this PR:

Z3 and CVC4 support a sufficient range of features in String and Regex theory.

The following parts are still missing or incomplete or can be improved:

a proper definition of the method allChar:
It is unclear whether SMT solvers support the full range of Unicode or just Ascii, as defined in SMTLIB2 (maybe with more escaped characters?). For the current SMT solvers we have the following situation:
- Z3 supports Unicode ranges, but returns unknown when solving with full range.
- CVC4 seems to only accept Ascii, and crashes with full Unicode range.
I would be in favour of removing the method allChar completely. We already provide a way to specify ranges of chars via the API. This should be sufficient.
model evaluation: currently we have not yet any support and tests for model evaluation.
more tests, e.g. for String comparison via LT/LEQ/GT/GEQ, for Regex operations like OPTIONAL, etc.
optional: a way to translate a real Java regex into SMTLIB2 regex. Currently all regex formulas are build from basic parts from scratch.
optional: a nice example, maybe encode a regex crossword puzzle with JavaSMT :-)
conversion between Int and String theory.
more methods for String theory, e.g., replace, charAt, indexOf, contains.

…String seem to be important.

serras · 2021-11-17T13:49:21Z

I've removed allChar and added conversions from regular expression classes (Pattern and Matcher).

I don't know very well how to check the current model evaluation. As far as I understand, it should work on Z3, but I don't know how to add more tests in the corresponding file.

As a third question: what do you mean as conversion between the Int and String theories?

kfriedberger · 2021-11-17T19:07:00Z

Hi @serras

The new API methods for Java regex might not work as expected. They will just return a String that is matches "literally", but not "structurally". If implemented, this feature might need a way to reconstruct a regex based on basic elements from SMTLIB.
I did not list the feature for now, but maybe as a future idea (sorry, should have added this as comment :-) ). This (if missing in the implementation) does not block the PR from merging.
There seem to be methods in Z3 and CVC4 to convert an expression from Int theory to String theory and also back, if the String consists of digits). These operations should be similar to the existing conversion between Int to Bitvector theory. For example, this could allow a query like (= (itos (+ 1 2) (charAt "345" 0))).

Best.

and simplification, and formatting, and fix JavaDoc.

Unicode with non-ascii chars remains an open problem for now.

AbstractBaseFormulaManager

theories

…ern. The only way to build up a regex is directly in JavaSMT from basic blocks. The support to convert a real Java regex to SMTLIB regex is missing (this is no simple step!).

We should think about updating Z3, because the new version 4.8.13 seems to provide several bugfixes. See sosy-lab#249 for details.

kfriedberger · 2021-11-27T11:35:54Z

With the support for formula visitation, this PR looks sufficient for a merge.
I will review the changes again in the afternoon and plan to merge then.

- extract common constant. - simplify replaceAll-test, cubic runtime in a test is too much :-).

…uantifiers. There seems to be a bug in CVC4 that weakens its reasoning, such that UNKNOWN/INCOMPLETE is returned from the SAT check. As CVC4 is no longer actively maintained (there is already CVC5), disabling the tests and having a basic support for String theory is a quick and reasonable step.

serras added 9 commits August 17, 2021 10:35

Initial support for String formulae

0520718

Run formatting

e66962a

Return BooleanFormula on equals

5ff9e5b

Do not use the string theory until Features.S is enabled

0c37762

Fix style problem

5eae506

SMTInterpol doesn't really support strings

abfba6c

Update UFElimination procedure

991b737

Finish removal of SMTInterpol string support

64896de

Another reversal

4509941

kfriedberger requested changes Aug 24, 2021

View reviewed changes

serras added 2 commits October 29, 2021 09:31

Merge remote-tracking branch 'sosy-lab/master'

5808d2c

Add regular expression support + more tests

75cc067

kfriedberger added 12 commits November 14, 2021 00:39

fix: add forgotten method for encapsulating Regex formulas.

e5fd0be

formatting.

70936a6

Please always apply 'ant format-diff' before committing to avoid such changes later.

fix type of empty and full regex.

94c04ea

add more operations for String theory: prefix and suffix.

4220e30

And simple JUnit tests.

add more operations for String theory: allow concatenation of several…

238ce26

… Strings or Regexs, add range operations.

update Readme with upcoming support for String and Regex theory.

b1a622e

improve assertion message.

1be548c

move JUnit tests for Strings into a separate class.

587cdf0

There are several operations on Strings and Regexs and the number of JUnit tests might increase.

formatting Junit test

49a52ef

replace merged imports by single-class imports, and ignore too many p…

95ab89f

…arameters. This fulfills our Checkstyle criteria.

cleanup

88fa084

- more documentation - reduced visibility, - move solver-independent code into abstract superclass

add support for String theory with CVC4.

a184697

CVC4 seems to support the full range of String and Regex operations, so JavaSMT can provide them. We should add some more tests for String theory.

kfriedberger and others added 2 commits November 14, 2021 16:43

add more operations for String theory: indexOf, contains, charAt, sub…

00fc6ee

…String seem to be important.

Remove allChar + translation from Java regex

cce8309

baierd and others added 22 commits November 19, 2021 20:25

Enable Strings in CVC4 to use unicode by default

d0d7d71

More tests for charAt, unicode and lexicographic ordering + fix a test

6c71f93

fix String comparison in Z3.

9e27bdd

more JUnit tests

90f8b38

and simplification, and formatting, and fix JavaDoc.

introduce variable to apply a common operation only once.

2728ed5

fix model retrieval for Strings in CVC4.

d849dfb

Unicode with non-ascii chars remains an open problem for now.

remove unused variables.

ab3f235

Add startIndex to indexOf in Strings according to SMTLIB2 standard

48f7357

More tests for concat, substring, indexOf, contains

6722500

Add more subString tests

64da1c3

Add more tests for substring based on variables

f0867f4

Add tests for String constants for replace() and replaceAll()

dcf86e0

Add more tests for replace() and replaceAll() for String theories

1cb177d

Fix a bug that StringFormulas used the BooleanFormula type

820c90f

Add StringFormulas in the type selection of the

b2c623d

AbstractBaseFormulaManager

Add a basic String Array test

241a91a

Add tests to check whether or not a solver supports all possible Array

425632f

theories

Add basic tests for quantifiers with strings and array int strings

f885645

Add more general array type combination tests

0659d05

remove API methods for building a regex from Java-based regex or patt…

f8c351e

…ern. The only way to build up a regex is directly in JavaSMT from basic blocks. The support to convert a real Java regex to SMTLIB regex is missing (this is no simple step!).

formatting.

93e53b8

adding basic visitor support for String and Regex theory.

81167e1

We should think about updating Z3, because the new version 4.8.13 seems to provide several bugfixes. See sosy-lab#249 for details.

kfriedberger added 4 commits November 27, 2021 13:33

improve JUnit test for model evaluation.

499275d

improve JUnit test for String theory.

ff4c5b1

- extract common constant. - simplify replaceAll-test, cubic runtime in a test is too much :-).

improve JUnit test for String theory, fix warnings.

2e46c9d

kfriedberger approved these changes Nov 27, 2021

View reviewed changes

kfriedberger merged commit 354b8b9 into sosy-lab:master Nov 27, 2021

Swalkyn mentioned this pull request Sep 13, 2022

re.allchar might be missing from the string formula API #281

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

String formulae #250

String formulae #250

serras commented Aug 24, 2021

kfriedberger left a comment

kfriedberger Aug 24, 2021

serras commented Oct 29, 2021

kfriedberger commented Nov 14, 2021 •

edited

Loading

serras commented Nov 17, 2021

kfriedberger commented Nov 17, 2021

kfriedberger commented Nov 27, 2021

String formulae #250

String formulae #250

Conversation

serras commented Aug 24, 2021

kfriedberger left a comment

Choose a reason for hiding this comment

kfriedberger Aug 24, 2021

Choose a reason for hiding this comment

serras commented Oct 29, 2021

kfriedberger commented Nov 14, 2021 • edited Loading

serras commented Nov 17, 2021

kfriedberger commented Nov 17, 2021

kfriedberger commented Nov 27, 2021

kfriedberger commented Nov 14, 2021 •

edited

Loading