abs package:what4

abs x1 returns the absolute value of x1. The term is expected to have type Int.

This module declares a set of abstract domains used by the solver. These are mostly interval domains on numeric types. Since these abstract domains are baked directly into the term representation, we want to get as much bang-for-buck as possible. Thus, we prioritize compact representations and simple algorithms over precision.

An abstract value represents a disjoint st of values.

This is a function that corresponds to a matlab solver function. It includes the definition as a ExprBuilder expr to enable export to other solvers.

Return solver function associated with ExprSymFn if any.

Get abstract value associated with element.

Return abstract domain associated with a nonce app

Return an unconstrained abstract value.

Builtin functions that can be used to generate symbolic functions. These functions are expected to be total, but the value returned may not be specified. e.g. IntegerToNatFn must return some natural number for every integer, but for negative integers, the particular number is unspecified.

This class is provides functions needed to implement the symbolic array intrinsic functions

Compute the clamped absolute value of a signed bitvector. The only difference between this operation and the usual 2's complement operation is the handling of MIN_INT. The usual 2's complement absolute value function sends MIN_INT to MIN_INT; however, the clamped version instead sends MIN_INT to MAX_INT.