Copyright	(c) Masahiro Sakai 2011-2013
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	MonoLocalBinds TypeFamilies KindSignatures ExplicitNamespaces

ToySolver.Data.Delta

Contents

The Delta type
Construction
Query
Relationship with integers

Description

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. https://doi.org/10.1007/11817963_11 http://yices.csl.sri.com/cav06.pdf

Synopsis

data Delta r = Delta !r !r
fromReal :: Num r => r -> Delta r
delta :: Num r => Delta r
realPart :: Delta r -> r
deltaPart :: Delta r -> r
floor' :: (RealFrac r, Integral a) => Delta r -> a
ceiling' :: (RealFrac r, Integral a) => Delta r -> a
isInteger' :: RealFrac r => Delta r -> Bool

The Delta type

data Delta r Source #

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

Constructors

Delta !r !r

Instances

Instances details

(Num r, Ord r) => Num (Delta r) Source #	This instance assumes the symbolic infinitesimal parameter δ is a nilpotent with δ² = 0.
Instance details Defined in ToySolver.Data.Delta 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 #
(Fractional r, Ord r) => Fractional (Delta r) Source #	This is unsafe instance in the sense that only a proper real can be a divisor.
Instance details Defined in ToySolver.Data.Delta Methods (/) :: Delta r -> Delta r -> Delta r # recip :: Delta r -> Delta r # fromRational :: Rational -> Delta r #
(Real r, Eq r) => Real (Delta r) Source #
Instance details Defined in ToySolver.Data.Delta Methods toRational :: Delta r -> Rational #
(RealFrac r, Eq r) => RealFrac (Delta r) Source #
Instance details Defined in ToySolver.Data.Delta 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) Source #
Instance details Defined in ToySolver.Data.Delta Methods showsPrec :: Int -> Delta r -> ShowS # show :: Delta r -> String # showList :: [Delta r] -> ShowS #
Eq r => Eq (Delta r) Source #
Instance details Defined in ToySolver.Data.Delta Methods (==) :: Delta r -> Delta r -> Bool # (/=) :: Delta r -> Delta r -> Bool #
Ord r => Ord (Delta r) Source #
Instance details Defined in ToySolver.Data.Delta 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 #
SolverValue (Delta Rational) Source #
Instance details Defined in ToySolver.Arith.Simplex Methods toValue :: Rational -> Delta Rational Source # showValue :: Bool -> Delta Rational -> String Source # getModel :: PrimMonad m => GenericSolverM m (Delta Rational) -> m Model Source #
Num r => AdditiveGroup (Delta r) Source #
Instance details Defined in ToySolver.Data.Delta Methods zeroV :: Delta r # (^+^) :: Delta r -> Delta r -> Delta r # negateV :: Delta r -> Delta r # (^-^) :: Delta r -> Delta r -> Delta r #
Num r => VectorSpace (Delta r) Source #
Instance details Defined in ToySolver.Data.Delta Associated Types type Scalar (Delta r) # Methods (*^) :: Scalar (Delta r) -> Delta r -> Delta r #
type Scalar (Delta r) Source #
Instance details Defined in ToySolver.Data.Delta type Scalar (Delta r) = r