ToySolver.Arith.Cooper

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

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

Quantifier elimination

eliminateQuantifiers :: Formula (Atom Rational) -> Maybe QFFormula

Eliminate quantifiers and returns equivalent quantifier-free formula.

eliminateQuantifiers φ returns (ψ, lift) such that:

• ψ is a quantifier-free formula and LIA ⊢ ∀y1, …, yn. φ ↔ ψ where {y1, …, yn} = FV(φ) ⊇ FV(ψ), and
• if M ⊧_LIA ψ then lift M ⊧_LIA φ.

φ may or may not be a closed formula.

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

solveFormula :: VarSet -> Formula (Atom Rational) -> SatResult Integer

solveFormula {x1,…,xm} φ

• returns Sat M such that M ⊧_LIA φ when such M exists,
• returns Unsat when such M does not exists, and
• returns Unknown when φ is beyond LIA.

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