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)

Methods

(==) :: Delta r -> Delta r -> Bool

(/=) :: Delta r -> Delta r -> Bool

(Fractional r, Ord r) => Fractional (Delta r)

This is unsafe instance in the sense that only a proper real can be a divisor.

Methods

(/) :: Delta r -> Delta r -> Delta r

recip :: Delta r -> Delta r

fromRational :: Rational -> Delta r

(Num r, Ord r) => Num (Delta r)

This instance assumes the symbolic infinitesimal parameter δ is a nilpotent with δ² = 0.

Methods

(+) :: Delta r -> Delta r -> Delta r

(-) :: Delta r -> Delta r -> Delta r

(*) :: Delta r -> Delta r -> Delta r

negate :: Delta r -> Delta r

abs :: Delta r -> Delta r

signum :: Delta r -> Delta r

fromInteger :: Integer -> Delta r

Ord r => Ord (Delta r)

Methods

compare :: Delta r -> Delta r -> Ordering

(<) :: Delta r -> Delta r -> Bool

(<=) :: Delta r -> Delta r -> Bool

(>) :: Delta r -> Delta r -> Bool

(>=) :: Delta r -> Delta r -> Bool

max :: Delta r -> Delta r -> Delta r

min :: Delta r -> Delta r -> Delta r

(Real r, Eq r) => Real (Delta r)

Methods

toRational :: Delta r -> Rational

(RealFrac r, Eq r) => RealFrac (Delta r)

Methods

properFraction :: Integral b => Delta r -> (b, Delta r)

truncate :: Integral b => Delta r -> b

round :: Integral b => Delta r -> b

ceiling :: Integral b => Delta r -> b

floor :: Integral b => Delta r -> b

Show r => Show (Delta r)

Methods

showsPrec :: Int -> Delta r -> ShowS

show :: Delta r -> String

showList :: [Delta r] -> ShowS

Num r => VectorSpace (Delta r)

Associated Types

type Scalar (Delta r) :: *

Methods

(*^) :: Scalar (Delta r) -> Delta r -> Delta r

Num r => AdditiveGroup (Delta r)

Methods

zeroV :: Delta r

(^+^) :: Delta r -> Delta r -> Delta r

negateV :: Delta r -> Delta r

(^-^) :: Delta r -> Delta r -> Delta r

SolverValue (Delta Rational)

Methods

toValue :: Rational -> Delta Rational

showValue :: Bool -> Delta Rational -> String

getModel :: GenericSolver (Delta Rational) -> IO Model

type Scalar (Delta r)

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?