ToySolver.Arith.FourierMotzkin

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

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 φ.

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 φ.

Quantifier elimination

eliminateQuantifiers :: Formula (Atom Rational) -> Maybe (Formula (Atom Rational))

Eliminate quantifiers and returns equivalent quantifier-free formula.

eliminateQuantifiers φ returns (ψ, lift) such that:

• ψ is a quantifier-free formula and LRA ⊢ ∀y1, …, yn. φ ↔ ψ where {y1, …, yn} = FV(φ) ⊇ FV(ψ), and
• if M ⊧_LRA ψ then lift M ⊧_LRA φ.

φ may or may not be a closed formula.

Constraint solving

solveFormula :: VarSet -> Formula (Atom Rational) -> SatResult Rational

• solveFormula {x1,…,xm} φ returns Sat M such that M ⊧_LRA φ when such M exists,
• returns Unsat when such M does not exists, and
• returns Unknown when φ is beyond LRA.

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}.