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 calculateCuts in elim to ignore cyclic constraints instead of crashing #674

Open K9-guardian opened 8 months ago

K9-guardian commented 8 months ago

Currently Language.Fixpoint.Horn.Transformations.elim crashes the program if the constraint contains cycles. As outlined in ICFP2017, the intended behavior should be to ignore the cyclic constraints and use predicate abstraction to solve them. This change uses calculateCuts to remove the set of refinement variables that cause the constraint to be cyclic before running the elimination algorithm.

ranjitjhala commented 8 months ago

Thanks @K9-guardian !! I’m traveling atm but have started the CI … will take a closer look and merge when back in town tomorrow!