Use SMTLIB style serialization/deserialization for Horn queries#683
Merged
Conversation
| , pleWithUndecidedGuards = | ||
| False | ||
| &= name "ple-with-undecided-guards" | ||
| &= name "plewithundecidedguards" |
Collaborator
There was a problem hiding this comment.
Do you mean that keeping dashes here caused CI to fail? It would be helpful to see what the error is.
Member
Author
There was a problem hiding this comment.
Yes keeping the dashes there made the intId test fail (locally) as CmdArgs kept saying “unknown flag”. More mysteriously, the test worked if I just wrote “—ple”…
Member
Author
There was a problem hiding this comment.
I think it may be some strange MacOS thing ... have reverted the config flag name, will leave it be if it works in the CI!
Member
Author
|
(I reverted the flag, will just deal with the local failure on my mac :-) ) |
Merged
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
I want a human readable and machine serializable format for the horn queries, hence SMTLIB-style, to avoid all the knots of the FP parser.
Leaving the
Horn/Parse.hsfor backwards compatibility withfluxguarded by the--noHornSMTflag; will delete it after movingfluxover to this new format.@facundominguez -- there was some odd glitch with the
--ple-with-undecided-guardsI had to remove the-as otherwise somehow it wasn't parsing? [ totally unrelated to this PR but it was breaking the CI! ]