ToySolver.FourierMotzkin.Core

Naïve implementation of Fourier-Motzkin Variable Elimination

Reference:

• http://users.cecs.anu.edu.au/~michaeln/pubs/arithmetic-dps.pdf

Documentation

type ExprZ = Expr Integer

type Rat = (ExprZ, Integer)

(t,c) represents t/c, and c must be >0.

toRat :: Expr Rational -> Rat

fromRat :: Rat -> Expr Rational

data Lit

Literal

Constructors

Nonneg ExprZ

Pos ExprZ

Instances

Eq Lit

Ord Lit

Show Lit

Complement Lit

Variables Lit

leR :: Rat -> Rat -> Lit

ltR :: Rat -> Rat -> Lit

geR :: Rat -> Rat -> Lit

gtR :: Rat -> Rat -> Lit

simplify :: [Lit] -> Maybe [Lit]

fromLAAtom :: Atom Rational -> DNF Lit

toLAAtom :: Lit -> Atom Rational

constraintsToDNF :: [Atom Rational] -> DNF Lit

type BoundsR = ([Rat], [Rat], [Rat], [Rat])

collectBounds :: Var -> [Lit] -> (BoundsR, [Lit])

boundsToLits :: BoundsR -> Maybe [Lit]

evalBounds :: Model Rational -> BoundsR -> Interval Rational

project :: Var -> [Atom Rational] -> [([Atom Rational], Model Rational -> Model Rational)]

project' :: Var -> [Lit] -> Maybe ([Lit], Model Rational -> Model Rational)

projectN :: VarSet -> [Atom Rational] -> [([Atom Rational], Model Rational -> Model Rational)]

projectN' :: VarSet -> [Lit] -> Maybe ([Lit], Model Rational -> Model Rational)

solve :: VarSet -> [Atom Rational] -> Maybe (Model Rational)

solve' :: VarSet -> [Lit] -> Maybe (Model Rational)