search

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
182 stars 46 forks source link

Support for abs() on Integer and Floating-Point Theories #173

Closed blizzard4591 closed 4 years ago

blizzard4591 commented 4 years ago

Dear developers, I was trying to encode a program using JavaSMT and found no matching calls on the FormulaManagers for the abs() functions. I am using MathSAT5 as the backend. Should this be done using an ITE expression or is there some other, more clever way?

Thank you!

kfriedberger commented 4 years ago

Hi, you are right, currently our API does not yet offer abs(x) for numerals. You can easily implement it on top of the API by using ITE(x>=0,x,-x).

It seems as if the function abs is part of the SMTlib standard, thus we could add it (for some future release).

blizzard4591 commented 4 years ago

Ok, will do - Thanks!