ToySolver.Arith.OmegaTest

(incomplete) implementation of Omega Test

References:

• William Pugh. The Omega test: a fast and practical integer programming algorithm for dependence analysis. In Proceedings of the 1991 ACM/IEEE conference on Supercomputing (1991), pp. 4-13.
• http://users.cecs.anu.edu.au/~michaeln/pubs/arithmetic-dps.pdf

See also:

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

Solving

type Model r = VarMap r

A Model is a map from variables to values.

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

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

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

solveQFLIRAConj :: Options -> 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}.

Options for solving

data Options

Constructors

Options

Fields

optCheckReal :: VarSet -> [Atom Rational] -> Bool

optCheckReal is used for checking whether real shadow is satisfiable.

• If it returns True, the real shadow may or may not be satisfiable.
• If it returns False, the real shadow must be unsatisfiable

Instances

Default Options

defaultOptions :: Options

checkRealNoCheck :: VarSet -> [Atom Rational] -> Bool

checkRealByFM :: VarSet -> [Atom Rational] -> Bool

checkRealByCAD :: VarSet -> [Atom Rational] -> Bool

checkRealByVS :: VarSet -> [Atom Rational] -> Bool

checkRealBySimplex :: VarSet -> [Atom Rational] -> Bool