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.

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

Strings Theory #458

Merged
merged 7 commits into from Nov 27, 2017

Conversation

Projects
None yet
2 participants
@marcogario
Contributor

marcogario commented Nov 18, 2017

Add support for the theory of Strings with CVC4 as main solver.

Merge master into branch strings
This merge solves several conflicts due to the branch being more than 1
year old. Most notably, the handling of types and the walkers changed.

@marcogario marcogario requested a review from mikand Nov 18, 2017

@marcogario marcogario referenced this pull request Nov 18, 2017

Open

Strings Theory (Z3) #260

@marcogario marcogario added this to the 0.7.5 milestone Nov 18, 2017

@mikand

The PR is ok code-wise, modulo some quite minor comments.

What I really do not know is how standard this theory is... Do we want to commit to the CVC4 implementation? Is the Z3 one compatible?

Another more practical question is which alhpabet is used to define the strings: ASCII? UTF-8? What else?

# Strings
#
def is_python_string(str1):
return type(str1) == str

This comment has been minimized.

@mikand

mikand Nov 20, 2017

Contributor

I assume unicode is not supported, so this should be OK....

@mikand

mikand Nov 20, 2017

Contributor

I assume unicode is not supported, so this should be OK....

This comment has been minimized.

@marcogario

marcogario Nov 22, 2017

Contributor

👍

@marcogario

marcogario Nov 22, 2017

Contributor

👍

"""
return self.create_node(node_type=op.STR_SUFFIXOF, args=(s, t))
def StrToInt(self, s):

This comment has been minimized.

@mikand

mikand Nov 20, 2017

Contributor

Is this basically atoi()?

@mikand

mikand Nov 20, 2017

Contributor

Is this basically atoi()?

This comment has been minimized.

@marcogario

marcogario Nov 22, 2017

Contributor

Yes, with 2 exceptions:

  • If the string does not represent a number, it returns -1
  • It only interprets natural numbers

Indeed the name StrToNat would be better, but both solvers call this function StrToInt

@marcogario

marcogario Nov 22, 2017

Contributor

Yes, with 2 exceptions:

  • If the string does not represent a number, it returns -1
  • It only interprets natural numbers

Indeed the name StrToNat would be better, but both solvers call this function StrToInt

Show outdated Hide outdated pysmt/oracles.py Outdated
self.lbp = lbp
def nud(self, parser):
parser.advance() # OpenPar

This comment has been minimized.

@mikand

mikand Nov 20, 2017

Contributor

Is this advance needed? Having a look at UnaryOpAdapter it doesn't seem to be needed

@mikand

mikand Nov 20, 2017

Contributor

Is this advance needed? Having a look at UnaryOpAdapter it doesn't seem to be needed

This comment has been minimized.

@marcogario

marcogario Nov 22, 2017

Contributor

I am not sure, but the comment suggests that this is to handle the open parenthesis.
In unary op you have an expression such as "(! x)". In FunctionCall you have function like expression "str.to.int(x)".

@marcogario

marcogario Nov 22, 2017

Contributor

I am not sure, but the comment suggests that this is to handle the open parenthesis.
In unary op you have an expression such as "(! x)". In FunctionCall you have function like expression "str.to.int(x)".

@@ -76,7 +76,7 @@ def walk_not(self, formula):
self.write(")")
def walk_symbol(self, formula):
self.write(quote(formula.symbol_name(), style='"'))
self.write(quote(formula.symbol_name(), style="'"))

This comment has been minimized.

@mikand

mikand Nov 20, 2017

Contributor

This is not supported by the parser!

@mikand

mikand Nov 20, 2017

Contributor

This is not supported by the parser!

This comment has been minimized.

@marcogario

marcogario Nov 22, 2017

Contributor

You are right, I lost the corresponding change when splitting the PR.

@marcogario

marcogario Nov 22, 2017

Contributor

You are right, I lost the corresponding change when splitting the PR.

Show outdated Hide outdated pysmt/printers.py Outdated
Show outdated Hide outdated pysmt/simplifier.py Outdated
Show outdated Hide outdated pysmt/type_checker.py Outdated
Show outdated Hide outdated pysmt/type_checker.py Outdated
@@ -186,6 +189,39 @@ def walk_bv_sdiv(self, formula, args, **kwargs):
def walk_bv_srem(self, formula, args, **kwargs):
return self.mgr.BVSRem(args[0], args[1])
def walk_str_length(self, formula, args, **kwargs):

This comment has been minimized.

@mikand

mikand Nov 20, 2017

Contributor

Where is the association of this walk function to the corresponding node type? I cannot find it.

@mikand

mikand Nov 20, 2017

Contributor

Where is the association of this walk function to the corresponding node type? I cannot find it.

This comment has been minimized.

@marcogario

marcogario Nov 22, 2017

Contributor

This is done in walkers/generic.py:26 . The association is by default the lower-case version of the node name.

@marcogario

marcogario Nov 22, 2017

Contributor

This is done in walkers/generic.py:26 . The association is by default the lower-case version of the node name.

@marcogario

This comment has been minimized.

Show comment
Hide comment
@marcogario

marcogario Nov 21, 2017

Contributor

Z3 implements a very similar subset and notation. The other PR is dedicated to Z3, but I split this into 2 parts because the integration of Z3 is taking a long time (there were bugs, and not that the bugs are fixed the nightly build does not seem to work). This branch has been here for 1.5 years and I do not think there has been any progress in formalizing this theory in SMT-LIB. Therefore, I think we should move forward with the current subset. Note that CVC4 implements other operators that we do not support (all the stuff you caught related to uint16, for example).

Regarding the alphabet: it is ASCII
https://rise4fun.com/z3/tutorialcontent/sequences

Contributor

marcogario commented Nov 21, 2017

Z3 implements a very similar subset and notation. The other PR is dedicated to Z3, but I split this into 2 parts because the integration of Z3 is taking a long time (there were bugs, and not that the bugs are fixed the nightly build does not seem to work). This branch has been here for 1.5 years and I do not think there has been any progress in formalizing this theory in SMT-LIB. Therefore, I think we should move forward with the current subset. Note that CVC4 implements other operators that we do not support (all the stuff you caught related to uint16, for example).

Regarding the alphabet: it is ASCII
https://rise4fun.com/z3/tutorialcontent/sequences

marcogario added some commits Nov 22, 2017

Theory Oracle: Integer for str functions
For str_length, str_indexof, and str_to_int, the Theory Oracle now
returns a theory containing also Integers.
@mikand

mikand approved these changes Nov 27, 2017

@mikand mikand merged commit fad65c3 into master Nov 27, 2017

5 checks passed

clahub All contributors have signed the Contributor License Agreement.
Details
continuous-integration/appveyor/branch AppVeyor build succeeded
Details
continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
continuous-integration/travis-ci/push The Travis CI build passed
Details

@mikand mikand deleted the strings_theory branch Nov 27, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment