Automatically scrape qualifiers from predicates in Horn clauses

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types

BSD 3-Clause "New" or "Revised" License

141 stars 61 forks source link

Closed ranjitjhala closed 1 year ago

ranjitjhala commented 1 year ago

This is experimental hence hidden behind a flag:

--scrape=no (default) do nothing, only use user specified qualifiers
--scrape=head : scrape qualifiers from the head of the horn clauses (RHS)
--scrape=both : scrape qualifiers from the head and the body of the clauses (RHS+LHS)