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

transformation for introducing destructors #5

Open c-cube opened 8 years ago

c-cube commented 8 years ago

transform exists x. y = s x & p[x] into is-s y && p[select-s-0 y]

note: would apply to backends CVC4 and smbc, at least?