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

Copyright(c) Masahiro Sakai 2011
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable (TypeFamilies)
Safe HaskellSafe
LanguageHaskell2010

ToySolver.Data.LA

Contents

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) Source # 

Methods

(==) :: Expr r -> Expr r -> Bool #

(/=) :: Expr r -> Expr r -> Bool #

Ord r => Ord (Expr r) Source # 

Methods

compare :: Expr r -> Expr r -> Ordering #

(<) :: Expr r -> Expr r -> Bool #

(<=) :: Expr r -> Expr r -> Bool #

(>) :: Expr r -> Expr r -> Bool #

(>=) :: Expr r -> Expr r -> Bool #

max :: Expr r -> Expr r -> Expr r #

min :: Expr r -> Expr r -> Expr r #

(Num r, Eq r, Read r) => Read (Expr r) Source # 
Show r => Show (Expr r) Source # 

Methods

showsPrec :: Int -> Expr r -> ShowS #

show :: Expr r -> String #

showList :: [Expr r] -> ShowS #

NFData r => NFData (Expr r) Source # 

Methods

rnf :: Expr r -> () #

(Num r, Eq r) => VectorSpace (Expr r) Source # 

Associated Types

type Scalar (Expr r) :: * #

Methods

(*^) :: Scalar (Expr r) -> Expr r -> Expr r #

(Num r, Eq r) => AdditiveGroup (Expr r) Source # 

Methods

zeroV :: Expr r #

(^+^) :: Expr r -> Expr r -> Expr r #

negateV :: Expr r -> Expr r #

(^-^) :: Expr r -> Expr r -> Expr r #

Variables (Expr r) Source # 

Methods

vars :: Expr r -> VarSet Source #

IsOrdRel (Expr Integer) QFFormula Source # 
IsEqRel (Expr Integer) QFFormula Source # 
type Scalar (Expr r) Source # 
type Scalar (Expr r) = r

type Var = Int Source #

Variables are represented as non-negative integers

Conversion

var :: Num r => Var -> Expr r Source #

variable

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

constant

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

terms contained in the expression.

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

Create a Expr from a list of terms.

coeffMap :: Expr r -> IntMap r Source #

a mapping from variables to coefficients

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

Create a Expr from a mapping from variables to coefficients.

unitVar :: Var Source #

Special variable that should always be evaluated to 1.

asConst :: Num r => Expr r -> Maybe r Source #

Query

coeff :: Num r => Var -> Expr r -> r Source #

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

lookupCoeff :: Num r => Var -> Expr r -> Maybe r Source #

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 b Source #

map coefficients.

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

map coefficients.

evalExpr :: Num r => Model r -> Expr r -> r Source #

evaluate the expression under the model.

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

evaluate the expression under the model.

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

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

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

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

showExpr :: (Num r, Eq r, Show r) => Expr r -> String Source #

Atomic formula of linear arithmetics

type Atom r = OrdRel (Expr r) Source #

Atomic Formula of Linear Arithmetics

showAtom :: (Num r, Eq r, Show r) => Atom r -> String Source #

evalAtom :: (Num r, Ord r) => Model r -> Atom r -> Bool Source #

evaluate the formula under the model.

applySubstAtom :: (Num r, Eq r) => VarMap (Expr r) -> Atom r -> Atom r Source #

applySubst1Atom :: (Num r, Eq r) => Var -> Expr r -> Atom r -> Atom r Source #

applySubst1 x e phi == phi[e/x]

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 r Source #

compute bounds for a Expr with respect to BoundsEnv.