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.

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

Merged
merged 4 commits into from
Jan 4, 2025
Merged

Fixing JS binding tests #207

merged 4 commits into from
Jan 4, 2025

Conversation

vhavlena
Copy link
Collaborator

@vhavlena vhavlena commented Jan 2, 2025

This PR fixes tests for JS binding.

@vhavlena vhavlena requested a review from jurajsic January 2, 2025 19:59
@vhavlena
Copy link
Collaborator Author

vhavlena commented Jan 3, 2025

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.

Comment on lines +128 to +131
// quantified variable
if(is_var(ex)) {
return;
}
Copy link
Member

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.

Copy link
Member

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.

Copy link
Collaborator Author

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).

Copy link
Member

@jurajsic jurajsic left a 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.

@jurajsic
Copy link
Member

jurajsic commented Jan 4, 2025

I think you can merge

@vhavlena vhavlena merged commit 44820d7 into devel Jan 4, 2025
2 checks passed
@vhavlena vhavlena deleted the fix-npm-test branch January 4, 2025 19:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants