ToySolver.Arith.FourierMotzkin.Base

Naïve implementation of Fourier-Motzkin Variable Elimination

Reference:

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

Primitive constraints

data Constr

Atomic constraint

Constructors

IsNonneg ExprZ

e ≥ 0

IsPos ExprZ

e > 0

IsZero ExprZ

e = 0

Instances

Eq Constr

Methods

(==) :: Constr -> Constr -> Bool

(/=) :: Constr -> Constr -> Bool

Ord Constr

Methods

compare :: Constr -> Constr -> Ordering

(<) :: Constr -> Constr -> Bool

(<=) :: Constr -> Constr -> Bool

(>) :: Constr -> Constr -> Bool

(>=) :: Constr -> Constr -> Bool

max :: Constr -> Constr -> Constr

min :: Constr -> Constr -> Constr

Show Constr

Methods

showsPrec :: Int -> Constr -> ShowS

show :: Constr -> String

showList :: [Constr] -> ShowS

Variables Constr

Methods

vars :: Constr -> VarSet

eqR :: Rat -> Rat -> Constr

type ExprZ = Expr Integer

fromLAAtom :: Atom Rational -> DNF Constr

toLAAtom :: Constr -> Atom Rational

constraintsToDNF :: [Atom Rational] -> DNF Constr

simplify :: [Constr] -> Maybe [Constr]

Simplify conjunction of Constrs. It returns Nothing when a inconsistency is detected.

Bounds

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

evalBounds :: Model Rational -> Bounds -> Interval Rational

boundsToConstrs :: Bounds -> Maybe [Constr]

collectBounds :: Var -> [Constr] -> (Bounds, [Constr])

Projection

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

project x φ returns [(ψ_1, lift_1), …, (ψ_m, lift_m)] such that:

• ⊢_LRA ∀y1, …, yn. (∃x. φ) ↔ (ψ_1 ∨ … ∨ φ_m) where {y1, …, yn} = FV(φ) \ {x}, and
• if M ⊧_LRA ψ_i then lift_i M ⊧_LRA φ.

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

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

projectN {x1,…,xm} φ returns [(ψ_1, lift_1), …, (ψ_n, lift_n)] such that:

• ⊢_LRA ∀y1, …, yp. (∃x. φ) ↔ (ψ_1 ∨ … ∨ φ_n) where {y1, …, yp} = FV(φ) \ {x1,…,xm}, and
• if M ⊧_LRA ψ_i then lift_i M ⊧_LRA φ.

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

Solving

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

solve {x1,…,xn} φ returns Just M that M ⊧_LRA φ when such M exists, returns Nothing otherwise.

FV(φ) must be a subset of {x1,…,xn}.

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

Utilities used by other modules

type Rat = (ExprZ, Integer)

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

toRat :: Expr Rational -> Rat