toysolver-0.7.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2011-2013
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010
Extensions
  • TypeSynonymInstances
  • FlexibleInstances
  • ConstrainedClassMethods
  • MultiParamTypeClasses

ToySolver.Arith.FourierMotzkin.Base

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

Instances details
Eq Constr Source # 
Instance details

Defined in ToySolver.Arith.FourierMotzkin.Base

Methods

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

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

Ord Constr Source # 
Instance details

Defined in ToySolver.Arith.FourierMotzkin.Base

Show Constr Source # 
Instance details

Defined in ToySolver.Arith.FourierMotzkin.Base

Variables Constr Source # 
Instance details

Defined in ToySolver.Arith.FourierMotzkin.Base

Methods

vars :: Constr -> VarSet Source #

Eval (Model Rational) Constr Bool Source # 
Instance details

Defined in ToySolver.Arith.FourierMotzkin.Base

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 #

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

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

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

Utilities used by other modules

type Rat = (ExprZ, Integer) Source #

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