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

approximate quantifiers in `ElimData` on incomplete types #23

Closed c-cube closed 7 years ago

c-cube commented 7 years ago

For a datatype τ approximated in an incomplete way but with finite cardinal (say, 16), we need to encode ∀x:τ. p x into card(α_τ) ≥ 16 ∧ ∀x:α_τ. p x.

See: bugs/quantifier_kodkod.nun

c-cube commented 7 years ago

cc @blanchette for reference.