abs function
Implementation
Expr abs(Expr x, [Sort? sort]) {
sort ??= getSort(x);
if (sort is FloatSort) {
return fpaAbs(x);
} else if (sort is BitVecSort) {
return ite(bvSlt(x, sort.zero()), bvNeg(x), x);
} else if (sort is IntSort || sort is RealSort) {
return ite(lt(x, intFrom(0)), unaryMinus(x), x);
} else {
throw ArgumentError('Unsupported sort: $sort');
}
}