| Copyright | (c) Masahiro Sakai 2011 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
ToySolver.Arith.OmegaTest
Contents
Description
(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:
- type Model r = VarMap r
- solve :: Options -> VarSet -> [Atom Rational] -> Maybe (Model Integer)
- solveQFLIRAConj :: Options -> VarSet -> [Atom Rational] -> VarSet -> Maybe (Model Rational)
- data Options = Options {
- optCheckReal :: VarSet -> [Atom Rational] -> Bool
- 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
Solving
solve :: Options -> VarSet -> [Atom Rational] -> Maybe (Model Integer) Source
solve opt {x1,…,xn} φ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) Source
solveQFLIRAConj {x1,…,xn} φ IJust M that M ⊧_LIRA φ when
such M exists, returns Nothing otherwise.
FV(φ)must be a subset of{x1,…,xn}.Iis a set of integer variables and must be a subset of{x1,…,xn}.