search

Gbury / dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
BSD 2-Clause "Simplified" License
80 stars 17 forks source link

Support `bv2nat` as a "relaxed mode" #206

Closed hansjoergschurr closed 8 months ago

hansjoergschurr commented 8 months ago

The bv2nat function is non-standard function to convert bitvectors to natural numbers.

However, those functions appear often in generated benchmarks (esp. the why3 pipeline). Since SMT-LIB will likely support these operators in the future, it would be useful to know if an SMT-LIB benchmark is standard-complied otherwise.

I think a nice way to expose this to the user would be a switch that adds bv2nat as a function if the theory is BitVector + Natural Numbers. If you imagine supporting other extensions to SMT-LIB this could be something like --accept-extension=T where T is a list (only bv2nat for now).

Gbury commented 8 months ago

That's the plan indeed, see my comments in #205

hansjoergschurr commented 8 months ago

Ahhh, sorry for the duplicate