Copyright	(c) Masahiro Sakai 2011-2014
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	TypeSynonymInstances FlexibleInstances ConstrainedClassMethods MultiParamTypeClasses

ToySolver.Arith.Cooper.Base

Contents

Language of presburger arithmetics
Projection
Constraint solving

Description

Naive implementation of Cooper's algorithm

Reference:

Language of presburger arithmetics

type ExprZ = Expr Integer Source #

Linear arithmetic expression over integers.

data Lit Source #

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

Instances details

Show Lit Source #
Instance details Defined in ToySolver.Arith.Cooper.Base Methods showsPrec :: Int -> Lit -> ShowS # show :: Lit -> String # showList :: [Lit] -> ShowS #
Eq Lit Source #
Instance details Defined in ToySolver.Arith.Cooper.Base Methods (==) :: Lit -> Lit -> Bool # (/=) :: Lit -> Lit -> Bool #
Ord Lit Source #
Instance details 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 #
Complement Lit Source #
Instance details Defined in ToySolver.Arith.Cooper.Base Methods notB :: Lit -> Lit Source #
Variables Lit Source #
Instance details Defined in ToySolver.Arith.Cooper.Base Methods vars :: Lit -> VarSet Source #
IsEqRel (Expr Integer) QFFormula Source #
Instance details Defined in ToySolver.Arith.Cooper.Base Methods (.==.) :: Expr Integer -> Expr Integer -> QFFormula Source # (./=.) :: Expr Integer -> Expr Integer -> QFFormula Source #
IsOrdRel (Expr Integer) QFFormula Source #
Instance details Defined in ToySolver.Arith.Cooper.Base Methods (.<.) :: Expr Integer -> Expr Integer -> QFFormula Source # (.<=.) :: Expr Integer -> Expr Integer -> QFFormula Source # (.>.) :: Expr Integer -> Expr Integer -> QFFormula Source # (.>=.) :: Expr Integer -> Expr Integer -> QFFormula Source # ordRel :: RelOp -> Expr Integer -> Expr Integer -> QFFormula Source #
Eval (Model Integer) Lit Bool Source #
Instance details Defined in ToySolver.Arith.Cooper.Base Methods eval :: Model Integer -> Lit -> Bool Source #

type QFFormula = BoolExpr Lit Source #

Quantifier-free formula of Presburger arithmetic.

fromLAAtom :: Atom Rational -> QFFormula Source #

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

d | e means e can be divided by d.

type Model r = VarMap r Source #

A Model is a map from variables to values.

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

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

Methods

eval :: m -> e -> v Source #

Instances

Instances details

Eval m a Bool => Eval m (BoolExpr a) Bool Source #
Instance details Defined in ToySolver.Data.BoolExpr Methods eval :: m -> BoolExpr a -> Bool Source #
(Eval m e a, Ord a) => Eval m (OrdRel e) Bool Source #
Instance details Defined in ToySolver.Data.OrdRel Methods eval :: m -> OrdRel e -> Bool Source #
Eval (Model Rational) Constr Bool Source #
Instance details Defined in ToySolver.Arith.FourierMotzkin.Base Methods eval :: Model Rational -> Constr -> Bool Source #
Eval (Model Integer) Lit Bool Source #
Instance details Defined in ToySolver.Arith.Cooper.Base Methods eval :: Model Integer -> Lit -> Bool Source #
Fractional r => Eval (Model r) (Expr r) r Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods eval :: Model r -> Expr r -> r Source #
Num r => Eval (Model r) (Expr r) r Source #
Instance details Defined in ToySolver.Data.LA Methods eval :: Model r -> Expr r -> r Source #

Projection

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

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

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

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

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

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

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

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