abs function

Expr abs(
  1. Expr x, [
  2. Sort? sort
])

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');
  }
}