ToySolver.Data.Delta

Augmenting number types with infinitesimal parameter δ.

Reference:

• Bruno Dutertre and Leonardo de Moura, "A Fast Linear-Arithmetic Solver for DPLL(T)", Computer Aided Verification In Computer Aided Verification, Vol. 4144 (2006), pp. 81-94. http://dx.doi.org/10.1007/11817963_11 http://yices.csl.sri.com/cav06.pdf

The Delta type

data Delta r

Delta r k represents r + kδ for symbolic infinitesimal parameter δ.

Constructors

Delta !r !r

Instances

Eq r => Eq (Delta r)

Ord r => Ord (Delta r)

Show r => Show (Delta r)

Num r => VectorSpace (Delta r)

Num r => AdditiveGroup (Delta r)

SolverValue (Delta Rational)

type Scalar (Delta r) = r

Construction

fromReal :: Num r => r -> Delta r

Conversion from a base r value to Delta r.

delta :: Num r => Delta r

symbolic infinitesimal parameter δ.

Query

realPart :: Delta r -> r

Extracts the real part..

deltaPart :: Delta r -> r

Extracts the δ part..

Relationship with integers

floor' :: (RealFrac r, Integral a) => Delta r -> a

Delta version of floor. floor' x returns the greatest integer not greater than x

ceiling' :: (RealFrac r, Integral a) => Delta r -> a

Delta version of ceiling. ceiling' x returns the least integer not less than x

isInteger' :: RealFrac r => Delta r -> Bool

Is this a integer?