search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
132 stars 60 forks source link

Use SMTLIB style serialization/deserialization for Horn queries #683

Closed ranjitjhala closed 6 months ago

ranjitjhala commented 6 months ago

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.hs for backwards compatibility with flux guarded by the --noHornSMT flag; will delete it after moving flux over to this new format.

@facundominguez -- there was some odd glitch with the --ple-with-undecided-guards I had to remove the - as otherwise somehow it wasn't parsing? [ totally unrelated to this PR but it was breaking the CI! ]

ranjitjhala commented 6 months ago

(I reverted the flag, will just deal with the local failure on my mac :-) )