You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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…
The text was updated successfully, but these errors were encountered:
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…
The text was updated successfully, but these errors were encountered: