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…
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…