ToySolver.Arith.Cooper.Base

Naive implementation of Cooper's algorithm

Reference:

• http://hagi.is.s.u-tokyo.ac.jp/pub/staff/hagiya/kougiroku/ronri/5.txt
• http://www.cs.cmu.edu/~emc/spring06/home1_files/Presburger%20Arithmetic.ppt

See also:

• http://hackage.haskell.org/package/presburger

Language of presburger arithmetics

type ExprZ = Expr Integer

Linear arithmetic expression over integers.

data Lit

Literals of Presburger arithmetic.

Constructors

IsPos ExprZ

IsPos e means e > 0

Divisible Bool Integer ExprZ

• Divisible True d e means e can be divided by d (i.e. d | e)
• Divisible False d e means e can not be divided by d (i.e. ¬(d | e))

Instances

Eq Lit

Defined in ToySolver.Arith.Cooper.Base

Methods

(==) :: Lit -> Lit -> Bool

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

Ord Lit

Defined in ToySolver.Arith.Cooper.Base

Methods

compare :: Lit -> Lit -> Ordering

(<) :: Lit -> Lit -> Bool

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

(>) :: Lit -> Lit -> Bool

(>=) :: Lit -> Lit -> Bool

max :: Lit -> Lit -> Lit

min :: Lit -> Lit -> Lit

Show Lit

Defined in ToySolver.Arith.Cooper.Base

Methods

showsPrec :: Int -> Lit -> ShowS

show :: Lit -> String

showList :: [Lit] -> ShowS

Complement Lit

Defined in ToySolver.Arith.Cooper.Base

Methods

notB :: Lit -> Lit

Variables Lit

Defined in ToySolver.Arith.Cooper.Base

Methods

vars :: Lit -> VarSet

IsOrdRel (Expr Integer) QFFormula

Defined in ToySolver.Arith.Cooper.Base

Methods

(.<.) :: Expr Integer -> Expr Integer -> QFFormula

(.<=.) :: Expr Integer -> Expr Integer -> QFFormula

(.>.) :: Expr Integer -> Expr Integer -> QFFormula

(.>=.) :: Expr Integer -> Expr Integer -> QFFormula

ordRel :: RelOp -> Expr Integer -> Expr Integer -> QFFormula

IsEqRel (Expr Integer) QFFormula

Defined in ToySolver.Arith.Cooper.Base

Methods

(.==.) :: Expr Integer -> Expr Integer -> QFFormula

(./=.) :: Expr Integer -> Expr Integer -> QFFormula

Eval (Model Integer) Lit Bool

Defined in ToySolver.Arith.Cooper.Base

Methods

eval :: Model Integer -> Lit -> Bool

evalLit :: Model Integer -> Lit -> Bool

Deprecated: Use Eval class instead

type QFFormula = BoolExpr Lit

Quantifier-free formula of Presburger arithmetic.

fromLAAtom :: Atom Rational -> QFFormula

(.|.) :: Integer -> ExprZ -> QFFormula

d | e means e can be divided by d.

evalQFFormula :: Model Integer -> QFFormula -> Bool

Deprecated: Use Eval class instead

evalQFFormula M φ returns whether M ⊧_LIA φ or not.

type Model r = VarMap r

A Model is a map from variables to values.

class Eval m e v | m e -> v where

Evaluataion of something (e.g. expression or formula) under the model.

Methods

eval :: m -> e -> v

Instances

Eval m a Bool => Eval m (BoolExpr a) Bool

Defined in ToySolver.Data.BoolExpr

Methods

eval :: m -> BoolExpr a -> Bool

(Eval m e a, Ord a) => Eval m (OrdRel e) Bool

Defined in ToySolver.Data.OrdRel

Methods

eval :: m -> OrdRel e -> Bool

Eval (Model Integer) Lit Bool

Defined in ToySolver.Arith.Cooper.Base

Methods

eval :: Model Integer -> Lit -> Bool

Eval (Model Rational) Constr Bool

Defined in ToySolver.Arith.FourierMotzkin.Base

Methods

eval :: Model Rational -> Constr -> Bool

Num r => Eval (Model r) (Expr r) r

Defined in ToySolver.Data.LA

Methods

eval :: Model r -> Expr r -> r

Fractional r => Eval (Model r) (Expr r) r

Defined in ToySolver.Data.FOL.Arith

Methods

eval :: Model r -> Expr r -> r

Projection

project :: Var -> QFFormula -> (QFFormula, Model Integer -> Model Integer)

project x φ returns (ψ, lift) such that:

• ⊢_LIA ∀y1, …, yn. (∃x. φ) ↔ ψ where {y1, …, yn} = FV(φ) \ {x}, and
• if M ⊧_LIA ψ then lift M ⊧_LIA φ.

projectN :: VarSet -> QFFormula -> (QFFormula, Model Integer -> Model Integer)

projectN {x1,…,xm} φ returns (ψ, lift) such that:

• ⊢_LIA ∀y1, …, yn. (∃x1, …, xm. φ) ↔ ψ where {y1, …, yn} = FV(φ) \ {x1,…,xm}, and
• if M ⊧_LIA ψ then lift M ⊧_LIA φ.

projectCases :: Var -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]

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

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

projectCasesN :: VarSet -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]

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

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

Constraint solving

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

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

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

solveQFFormula :: VarSet -> QFFormula -> Maybe (Model Integer)

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

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

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

solveQFLIRAConj {x1,…,xn} φ I returns Just M that M ⊧_LIRA φ when such M exists, returns Nothing otherwise.

• FV(φ) must be a subset of {x1,…,xn}.
• I is a set of integer variables and must be a subset of {x1,…,xn}.