search

stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
Other
114 stars 43 forks source link

How to covert bit vector 1 term expressions to boolean term expressions? #314

Closed fangwenji closed 1 year ago

fangwenji commented 2 years ago

Hi, I'm currently using the cvc5 solver, which distinguishes the boolean and bv1 sorts. So I would like to ask that is there a way to convert bv1 terms to boolean terms, and conversely, from boolean to bv1?

Thank you so much for your time!

yoni206 commented 2 years ago

Hi,

Thanks for your question.

A simple solution can be using ites. In SMT-LIB this would look like this:

(ite (= x (_ bv1 1)) true false)
(ite (= x true) (_ bv1 1) (_ bv0 1))

And the corresponding smt-switch terms can be constructed. Hope this helps, and please let me know if you have any other questions.

On Thu, Nov 10, 2022 at 12:00 PM Wenji Fang @.***> wrote:

Hi, I'm currently using the cvc5 solver, which distinguishes the boolean and bv1 sorts. So I would like to ask that is there a way to convert bv1 terms to boolean terms, and conversely, from boolean to bv1?

Thank you so much for your time!

— Reply to this email directly, view it on GitHub https://github.com/stanford-centaur/smt-switch/issues/314, or unsubscribe https://github.com/notifications/unsubscribe-auth/ADAKGRALAF6ILCHXUGN6TXTWHTBVXANCNFSM6AAAAAAR4LZ54M . You are receiving this because you are subscribed to this thread.Message ID: @.***>

fangwenji commented 2 years ago

Got it! Thank you so much for your help!