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

Copyright(c) Masahiro Sakai 2011-2013
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

ToySolver.Arith.FourierMotzkin.Base

Contents

Description

Naïve implementation of Fourier-Motzkin Variable Elimination

Reference:

Synopsis

Primitive constraints

data Constr Source

Atomic constraint

Constructors

IsNonneg ExprZ

e ≥ 0

IsPos ExprZ

e > 0

IsZero ExprZ

e = 0

Instances

eqR :: Rat -> Rat -> Constr Source

type ExprZ = Expr Integer Source

fromLAAtom :: Atom Rational -> DNF Constr Source

toLAAtom :: Constr -> Atom Rational Source

constraintsToDNF :: [Atom Rational] -> DNF Constr Source

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

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

Bounds

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

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

boundsToConstrs :: Bounds -> Maybe [Constr] Source

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

Projection

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

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

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

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

Solving

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

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

Utilities used by other modules

type Rat = (ExprZ, Integer) Source

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

toRat :: Expr Rational -> Rat Source