-
Notifications
You must be signed in to change notification settings - Fork 6
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
Fixing JS binding tests #207
Conversation
Now it should handle unquantified length variables inside quantified subformulae. Unfortunately, we are still not able to solve quantified string formulae. There is still quite a lot of things to do. |
// quantified variable | ||
if(is_var(ex)) { | ||
return; | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should we put some test that if ex
is string variable, we throw error? So we do not accidentally handle some formula with string quantifiers incorrectly.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm, now that I think about it, it will probably fail somewhere further in the solver if we get quantifiers, so it might not be needed.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If there is a quantification over non-string variables (ints or whatever), it could be correct. For a quantification over string variables it likely fails somewhere else (we need to look at it properly at some point).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good, just two minor things.
I think you can merge |
This PR fixes tests for JS binding.