search

cvc5 / cvc5_pythonic_api

A Z3Py-compatible interface to cvc5
Other
6 stars 9 forks source link

Boolean overloads #28

Closed alex-ozdemir closed 3 years ago

alex-ozdemir commented 3 years ago

Yeah. Not clear why they couldn't just use AND. Do you know of any difference in SMT semantics between (ite a b 0) and (and a b)?

makaimann commented 3 years ago

I don't think there's any semantic difference from an SMT perspective, because you have to consider all the constraints at once. I'd actually think the encoding would usually be worse because typically an ITE would be rewritten into two equalities for each case. But I'm not an expert on this so I could definitely be missing something.

alex-ozdemir commented 3 years ago

I don't think there's any semantic difference from an SMT perspective,

My thoughts as well. The only reason I can imagine would be some difference in the semantics of partial functions, but SMT tries to avoid those.... Perhaps this is another mystery to ask the Z3 devs about sometime.