Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

String formulae #250

Merged
merged 59 commits into from
Nov 27, 2021
Merged

String formulae #250

merged 59 commits into from
Nov 27, 2021

Commits on Aug 17, 2021

  1. Initial support for String formulae

    @serras
    serras committed Aug 17, 2021
    Configuration menu
    Copy the full SHA
    0520718 View commit details
    Browse the repository at this point in the history

  2. Run formatting

    @serras
    serras committed Aug 17, 2021
    Configuration menu
    Copy the full SHA
    e66962a View commit details
    Browse the repository at this point in the history

  3. Return BooleanFormula on equals

    @serras
    serras committed Aug 17, 2021
    Configuration menu
    Copy the full SHA
    5ff9e5b View commit details
    Browse the repository at this point in the history

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

    @serras
    serras committed Aug 17, 2021
    Configuration menu
    Copy the full SHA
    0c37762 View commit details
    Browse the repository at this point in the history

  5. Fix style problem

    @serras
    serras committed Aug 17, 2021
    Configuration menu
    Copy the full SHA
    5eae506 View commit details
    Browse the repository at this point in the history

Commits on Aug 24, 2021

  1. SMTInterpol doesn't really support strings

    @serras
    serras committed Aug 24, 2021
    Configuration menu
    Copy the full SHA
    abfba6c View commit details
    Browse the repository at this point in the history

  2. Update UFElimination procedure

    @serras
    serras committed Aug 24, 2021
    Configuration menu
    Copy the full SHA
    991b737 View commit details
    Browse the repository at this point in the history

  3. Finish removal of SMTInterpol string support

    @serras
    serras committed Aug 24, 2021
    Configuration menu
    Copy the full SHA
    64896de View commit details
    Browse the repository at this point in the history

  4. Another reversal

    @serras
    serras committed Aug 24, 2021
    Configuration menu
    Copy the full SHA
    4509941 View commit details
    Browse the repository at this point in the history

Commits on Oct 29, 2021

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

    @serras
    serras committed Oct 29, 2021
    Configuration menu
    Copy the full SHA
    5808d2c View commit details
    Browse the repository at this point in the history

  2. Add regular expression support + more tests

    @serras
    serras committed Oct 29, 2021
    Configuration menu
    Copy the full SHA
    75cc067 View commit details
    Browse the repository at this point in the history

Commits on Nov 13, 2021

  1. fix: add forgotten method for encapsulating Regex formulas.

    @kfriedberger
    kfriedberger committed Nov 13, 2021
    Configuration menu
    Copy the full SHA
    e5fd0be View commit details
    Browse the repository at this point in the history

  2. formatting. 

    Please always apply 'ant format-diff' before committing to avoid such changes later.
    @kfriedberger
    kfriedberger committed Nov 13, 2021
    Configuration menu
    Copy the full SHA
    70936a6 View commit details
    Browse the repository at this point in the history

  3. fix type of empty and full regex.

    @kfriedberger
    kfriedberger committed Nov 13, 2021
    Configuration menu
    Copy the full SHA
    94c04ea View commit details
    Browse the repository at this point in the history

  4. add more operations for String theory: prefix and suffix. 

    And simple JUnit tests.
    @kfriedberger
    kfriedberger committed Nov 13, 2021
    Configuration menu
    Copy the full SHA
    4220e30 View commit details
    Browse the repository at this point in the history

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

    … Strings or Regexs, add range operations.
    @kfriedberger
    kfriedberger committed Nov 13, 2021
    Configuration menu
    Copy the full SHA
    238ce26 View commit details
    Browse the repository at this point in the history

  6. update Readme with upcoming support for String and Regex theory.

    @kfriedberger
    kfriedberger committed Nov 13, 2021
    Configuration menu
    Copy the full SHA
    b1a622e View commit details
    Browse the repository at this point in the history

  7. improve assertion message.

    @kfriedberger
    kfriedberger committed Nov 13, 2021
    Configuration menu
    Copy the full SHA
    1be548c View commit details
    Browse the repository at this point in the history

  8. move JUnit tests for Strings into a separate class. 

    There are several operations on Strings and Regexs
and the number of JUnit tests might increase.
    @kfriedberger
    kfriedberger committed Nov 13, 2021
    Configuration menu
    Copy the full SHA
    587cdf0 View commit details
    Browse the repository at this point in the history

  9. formatting Junit test

    @kfriedberger
    kfriedberger committed Nov 13, 2021
    Configuration menu
    Copy the full SHA
    49a52ef View commit details
    Browse the repository at this point in the history

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

    …arameters.

This fulfills our Checkstyle criteria.
    @kfriedberger
    kfriedberger committed Nov 13, 2021
    Configuration menu
    Copy the full SHA
    95ab89f View commit details
    Browse the repository at this point in the history

Commits on Nov 14, 2021

  1. cleanup 

    - more documentation
- reduced visibility,
- move solver-independent code into abstract superclass
    @kfriedberger
    kfriedberger committed Nov 14, 2021
    Configuration menu
    Copy the full SHA
    88fa084 View commit details
    Browse the repository at this point in the history

  2. add support for String theory with CVC4. 

    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
    kfriedberger committed Nov 14, 2021
    Configuration menu
    Copy the full SHA
    a184697 View commit details
    Browse the repository at this point in the history

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

    …String seem to be important.
    @kfriedberger
    kfriedberger committed Nov 14, 2021
    Configuration menu
    Copy the full SHA
    00fc6ee View commit details
    Browse the repository at this point in the history

Commits on Nov 17, 2021

  1. Remove allChar + translation from Java regex

    @serras
    serras committed Nov 17, 2021
    Configuration menu
    Copy the full SHA
    cce8309 View commit details
    Browse the repository at this point in the history

  2. fixing GEQ,LEQ,LT for String theory, and shortening some code.

    @kfriedberger
    kfriedberger committed Nov 17, 2021
    Configuration menu
    Copy the full SHA
    bab867b View commit details
    Browse the repository at this point in the history

  3. remove unused test for removed method "allChar()".

    @kfriedberger
    kfriedberger committed Nov 17, 2021
    Configuration menu
    Copy the full SHA
    1281b86 View commit details
    Browse the repository at this point in the history

  4. add more operations for String theory: IntToString and StringToInt. 

    and some JUnit tests.
    @kfriedberger
    kfriedberger committed Nov 17, 2021
    Configuration menu
    Copy the full SHA
    1d4c133 View commit details
    Browse the repository at this point in the history

Commits on Nov 18, 2021

  1. more junit tests for String theory.

    @kfriedberger
    kfriedberger committed Nov 18, 2021
    Configuration menu
    Copy the full SHA
    685bf4c View commit details
    Browse the repository at this point in the history

  2. fix Checkstyle warning.

    @kfriedberger
    kfriedberger committed Nov 18, 2021
    Configuration menu
    Copy the full SHA
    a562121 View commit details
    Browse the repository at this point in the history

Commits on Nov 19, 2021

  1. More tests for String equality constraints + negative length

    @baierd
    baierd committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    a89caac View commit details
    Browse the repository at this point in the history

  2. Add String length inequality tests for < <= > >=

    @baierd
    baierd committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    92357b0 View commit details
    Browse the repository at this point in the history

  3. Enable CVC4 to use all String methods by setting its options

    @baierd
    baierd committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    67de78a View commit details
    Browse the repository at this point in the history

  4. Enable Strings in CVC4 to use unicode by default

    @baierd
    baierd committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    d0d7d71 View commit details
    Browse the repository at this point in the history

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

    @baierd
    baierd committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    6c71f93 View commit details
    Browse the repository at this point in the history

  6. fix String comparison in Z3.

    @kfriedberger
    kfriedberger committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    9e27bdd View commit details
    Browse the repository at this point in the history

  7. more JUnit tests 

    and simplification,
and formatting,
and fix JavaDoc.
    @kfriedberger
    kfriedberger committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    90f8b38 View commit details
    Browse the repository at this point in the history

  8. introduce variable to apply a common operation only once.

    @kfriedberger
    kfriedberger committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    2728ed5 View commit details
    Browse the repository at this point in the history

  9. fix model retrieval for Strings in CVC4. 

    Unicode with non-ascii chars remains an open problem for now.
    @kfriedberger
    kfriedberger committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    d849dfb View commit details
    Browse the repository at this point in the history

  10. remove unused variables.

    @kfriedberger
    kfriedberger committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    ab3f235 View commit details
    Browse the repository at this point in the history

Commits on Nov 20, 2021

  1. Add startIndex to indexOf in Strings according to SMTLIB2 standard

    @baierd
    baierd committed Nov 20, 2021
    Configuration menu
    Copy the full SHA
    48f7357 View commit details
    Browse the repository at this point in the history

  2. More tests for concat, substring, indexOf, contains

    @baierd
    baierd committed Nov 20, 2021
    Configuration menu
    Copy the full SHA
    6722500 View commit details
    Browse the repository at this point in the history

Commits on Nov 21, 2021

  1. Add more subString tests

    @baierd
    baierd committed Nov 21, 2021
    Configuration menu
    Copy the full SHA
    64da1c3 View commit details
    Browse the repository at this point in the history

  2. Add more tests for substring based on variables

    @baierd
    baierd committed Nov 21, 2021
    Configuration menu
    Copy the full SHA
    f0867f4 View commit details
    Browse the repository at this point in the history

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

    @baierd
    baierd committed Nov 21, 2021
    Configuration menu
    Copy the full SHA
    dcf86e0 View commit details
    Browse the repository at this point in the history

Commits on Nov 26, 2021

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

    @baierd
    baierd committed Nov 26, 2021
    Configuration menu
    Copy the full SHA
    1cb177d View commit details
    Browse the repository at this point in the history

  2. Fix a bug that StringFormulas used the BooleanFormula type

    @baierd
    baierd committed Nov 26, 2021
    Configuration menu
    Copy the full SHA
    820c90f View commit details
    Browse the repository at this point in the history

  3. Add StringFormulas in the type selection of the 

    AbstractBaseFormulaManager
    @baierd
    baierd committed Nov 26, 2021
    Configuration menu
    Copy the full SHA
    b2c623d View commit details
    Browse the repository at this point in the history

  4. Add a basic String Array test

    @baierd
    baierd committed Nov 26, 2021
    Configuration menu
    Copy the full SHA
    241a91a View commit details
    Browse the repository at this point in the history

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

    theories
    @baierd
    baierd committed Nov 26, 2021
    Configuration menu
    Copy the full SHA
    425632f View commit details
    Browse the repository at this point in the history

  6. Add basic tests for quantifiers with strings and array int strings

    @baierd
    baierd committed Nov 26, 2021
    Configuration menu
    Copy the full SHA
    f885645 View commit details
    Browse the repository at this point in the history

  7. Add more general array type combination tests

    @baierd
    baierd committed Nov 26, 2021
    Configuration menu
    Copy the full SHA
    0659d05 View commit details
    Browse the repository at this point in the history

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

    …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!).
    @kfriedberger
    kfriedberger committed Nov 26, 2021
    Configuration menu
    Copy the full SHA
    f8c351e View commit details
    Browse the repository at this point in the history

  9. formatting.

    @kfriedberger
    kfriedberger committed Nov 26, 2021
    Configuration menu
    Copy the full SHA
    93e53b8 View commit details
    Browse the repository at this point in the history

Commits on Nov 27, 2021

  1. adding basic visitor support for String and Regex theory. 

    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
    kfriedberger committed Nov 27, 2021
    Configuration menu
    Copy the full SHA
    81167e1 View commit details
    Browse the repository at this point in the history

  2. improve JUnit test for model evaluation.

    @kfriedberger
    kfriedberger committed Nov 27, 2021
    Configuration menu
    Copy the full SHA
    499275d View commit details
    Browse the repository at this point in the history

  3. improve JUnit test for String theory. 

    - extract  common constant.
- simplify replaceAll-test, cubic runtime in a test is too much :-).
    @kfriedberger
    kfriedberger committed Nov 27, 2021
    Configuration menu
    Copy the full SHA
    ff4c5b1 View commit details
    Browse the repository at this point in the history

  4. improve JUnit test for String theory, fix warnings.

    @kfriedberger
    kfriedberger committed Nov 27, 2021
    Configuration menu
    Copy the full SHA
    2e46c9d View commit details
    Browse the repository at this point in the history

  5. CVC4: disable some JUnit tests for theory combination of Arrays and Q… 

    …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.
    @kfriedberger
    kfriedberger committed Nov 27, 2021
    Configuration menu
    Copy the full SHA
    284eb40 View commit details
    Browse the repository at this point in the history