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

Ord Lit

Show Lit

Complement Lit

Variables Lit

IsArithRel (Expr Integer) QFFormula

evalLit :: Model Integer -> Lit -> Bool

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

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

type Model r = VarMap r

A Model is a map from variables to values.

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