search

nunchaku-inria / nunchaku

Model finder for higher-order logic
https://nunchaku-inria.github.io/nunchaku/
BSD 2-Clause "Simplified" License
42 stars 3 forks source link

improve cardinality analysis for kodkod #22

Closed c-cube closed 7 years ago

c-cube commented 7 years ago

see bugs/better_card_kodkod.nun

c-cube commented 7 years ago

Now the issue is that the Kodkod backend doesn't know it can stop if current cardinality exceeds all bounds. Might be of interest for @blanchette .