toysolver-0.0.6: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc

Portability non-portable (TypeFamilies) provisional masahiro.sakai@gmail.com None

Data.LA

Description

Some definition for Theory of Linear Arithmetics.

Synopsis

# Expression of linear arithmetics

data Expr r Source

Linear combination of variables and constants. Non-negative keys are used for variables's coefficients. key `unitVar` is used for constants.

Instances

 Eq r => Eq (Expr r) Ord r => Ord (Expr r) (Num r, Eq r, Read r) => Read (Expr r) Show r => Show (Expr r) NFData r => NFData (Expr r) (Num r, Eq r) => VectorSpace (Expr r) (Num r, Eq r) => AdditiveGroup (Expr r) Variables (Expr r) IsRel (Expr Integer) QFFormula

## Conversion

var :: Num r => Var -> Expr rSource

variable

constant :: (Num r, Eq r) => r -> Expr rSource

constant

terms :: Expr r -> [(r, Var)]Source

terms contained in the expression.

fromTerms :: (Num r, Eq r) => [(r, Var)] -> Expr rSource

Create a `Expr` from a list of terms.

coeffMap :: Expr r -> IntMap rSource

a mapping from variables to coefficients

fromCoeffMap :: (Num r, Eq r) => IntMap r -> Expr rSource

Create a `Expr` from a mapping from variables to coefficients.

Special variable that should always be evaluated to 1.

asConst :: Num r => Expr r -> Maybe rSource

## Query

coeff :: Num r => Var -> Expr r -> rSource

lookup a coefficient of the variable. ``` coeff v e == fst (extract v e) ```

lookupCoeff :: Num r => Var -> Expr r -> Maybe rSource

lookup a coefficient of the variable. It returns `Nothing` if the expression does not contain `v`. ``` lookupCoeff v e == fmap fst (extractMaybe v e) ```

extract :: Num r => Var -> Expr r -> (r, Expr r)Source

`extract v e` returns `(c, e')` such that `e == c *^ v ^+^ e'`

extractMaybe :: Num r => Var -> Expr r -> Maybe (r, Expr r)Source

`extractMaybe v e` returns `Just (c, e')` such that `e == c *^ v ^+^ e'` if `e` contains v, and returns `Nothing` otherwise.

## Operations

mapCoeff :: (Num b, Eq b) => (a -> b) -> Expr a -> Expr bSource

map coefficients.

mapCoeffWithVar :: (Num b, Eq b) => (a -> Var -> b) -> Expr a -> Expr bSource

map coefficients.

evalExpr :: Num r => Model r -> Expr r -> rSource

evaluate the expression under the model.

evalLinear :: VectorSpace a => Model a -> a -> Expr (Scalar a) -> aSource

evaluate the expression under the model.

lift1 :: VectorSpace x => x -> (Var -> x) -> Expr (Scalar x) -> xSource

applySubst :: (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr rSource

applySubst1 :: (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr rSource

applySubst1 x e e1 == e1[e/x]

showExpr :: (Num r, Eq r, Show r) => Expr r -> StringSource

# Atomic formula of linear arithmetics

type Atom r = Rel (Expr r)Source

Atomic Formula of Linear Arithmetics

showAtom :: (Num r, Eq r, Show r) => Atom r -> StringSource

evalAtom :: (Num r, Ord r) => Model r -> Atom r -> BoolSource

evaluate the formula under the model.

solveFor :: (Real r, Fractional r) => Atom r -> Var -> Maybe (RelOp, Expr r)Source

Solve linear (in)equation for the given variable.

`solveFor a v` returns `Just (op, e)` such that `Atom v op e` is equivalent to `a`.

# misc

computeInterval :: (Real r, Fractional r) => BoundsEnv r -> Expr r -> Interval rSource

compute bounds for a `Expr` with respect to `BoundsEnv`.