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

Process GRASShopper output back into Starling #146

Open
MattWindsor91 opened this issue Feb 17, 2017 · 0 comments
Open

Process GRASShopper output back into Starling #146

MattWindsor91 opened this issue Feb 17, 2017 · 0 comments

Comments

@MattWindsor91
Copy link
Collaborator

We should ideally parse the output from GRASShopper and then format it in similar ways to the Z3 output, both for consistency's sake and also so we can then hook GRASShopper up to any future postprocessing we do (inference, composite proofs, etc).

This could be helped if GRASShopper had a more machine-readable output format, but presently I don't think it does.

Alternatively, we could get GRASShopper to output its SMT predicates in smtlib2 format, then see if we can read them back through and push them into Z3, but this seems rather circuitous…

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

No branches or pull requests

1 participant