search

uclid-org / uclid

UCLID5: formal modeling, verification, and synthesis of computational systems
Other
136 stars 32 forks source link

[request] will UCLID support a division operator? #68

Closed sxysun-zz closed 3 years ago

sxysun-zz commented 3 years ago

Hi! I have been using UCLID for our project deepsea in a model extractor for our programming language. And I have some questions about its features

I noticed that UCLID an interesting software and easier to use compared with things like PlusCal, however, UCLID does not have a division operator, so what we are doing now is to have some hacks like: procedure div (x : integer, y : integer) returns (r : integer) { assume(y == r * x); } and then use divisions as function calls (statements), but since normally divisions are expressions, that makes it a bit weird to translate (I am aware that I can write an ast pre-processing to solve this, but that would be a bit heavy-weight). So it would be nice if we could have a division operator in UCLID. Also, I wonder why UCLID did not support divisions right now, is it because it makes solving hard of non-linearity?

polgreen commented 3 years ago

Hi,

Thanks for the request. Yes, a division operator will make the resulting SMT query harder to solve since it potentially introduces non-linear arithmetic. I would be happy to have UCLID support the operator though and leave the choice up to the user whether to use it or not.

I'll can add it this week, or, if you would like to add it yourself, I would be happy to receive and review a PR.

sxysun-zz commented 3 years ago

Thanks for the explanation! It would be great if you can kindly add that support!