| Copyright | (c) Masahiro Sakai 2012 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | non-portable (ScopedTypeVariables, BangPatterns) |
| Safe Haskell | None |
| Language | Haskell2010 |
ToySolver.Arith.CAD
Description
References:
- Christian Michaux and Adem Ozturk. Quantifier Elimination following Muchnik https://math.umons.ac.be/preprints/src/Ozturk020411.pdf
- Arnab Bhattacharyya. Something you should know about: Quantifier Elimination (Part I) http://cstheory.blogoverflow.com/2011/11/something-you-should-know-about-quantifier-elimination-part-i/
- Arnab Bhattacharyya. Something you should know about: Quantifier Elimination (Part II) http://cstheory.blogoverflow.com/2012/02/something-you-should-know-about-quantifier-elimination-part-ii/
- data Point c
- = NegInf
- | RootOf (UPolynomial c) Int
- | PosInf
- data Cell c
- project :: (Ord v, Show v, PrettyVar v) => v -> [ArithRel (Polynomial Rational v)] -> [([ArithRel (Polynomial Rational v)], Model v -> Model v)]
- project' :: forall v. (Ord v, Show v, PrettyVar v) => [(UPolynomial (Polynomial Rational v), [Sign])] -> [([(Polynomial Rational v, [Sign])], [Cell (Polynomial Rational v)])]
- projectN :: (Ord v, Show v, PrettyVar v) => Set v -> [ArithRel (Polynomial Rational v)] -> [([ArithRel (Polynomial Rational v)], Model v -> Model v)]
- projectN' :: (Ord v, Show v, PrettyVar v) => Set v -> [(Polynomial Rational v, [Sign])] -> [([(Polynomial Rational v, [Sign])], Model v -> Model v)]
- solve :: forall v. (Ord v, Show v, PrettyVar v) => Set v -> [ArithRel (Polynomial Rational v)] -> Maybe (Model v)
- solve' :: forall v. (Ord v, Show v, PrettyVar v) => Set v -> [(Polynomial Rational v, [Sign])] -> Maybe (Model v)
- type Model v = Map v AReal
- findSample :: Ord v => Model v -> Cell (Polynomial Rational v) -> Maybe AReal
- evalCell :: Ord v => Model v -> Cell (Polynomial Rational v) -> Cell Rational
- evalPoint :: Ord v => Model v -> Point (Polynomial Rational v) -> Point Rational
Basic data structures
Constructors
| NegInf | |
| RootOf (UPolynomial c) Int | |
| PosInf |
Projection
project :: (Ord v, Show v, PrettyVar v) => v -> [ArithRel (Polynomial Rational v)] -> [([ArithRel (Polynomial Rational v)], Model v -> Model v)] Source
project' :: forall v. (Ord v, Show v, PrettyVar v) => [(UPolynomial (Polynomial Rational v), [Sign])] -> [([(Polynomial Rational v, [Sign])], [Cell (Polynomial Rational v)])] Source
projectN :: (Ord v, Show v, PrettyVar v) => Set v -> [ArithRel (Polynomial Rational v)] -> [([ArithRel (Polynomial Rational v)], Model v -> Model v)] Source
projectN' :: (Ord v, Show v, PrettyVar v) => Set v -> [(Polynomial Rational v, [Sign])] -> [([(Polynomial Rational v, [Sign])], Model v -> Model v)] Source
Solving
solve :: forall v. (Ord v, Show v, PrettyVar v) => Set v -> [ArithRel (Polynomial Rational v)] -> Maybe (Model v) Source
solve' :: forall v. (Ord v, Show v, PrettyVar v) => Set v -> [(Polynomial Rational v, [Sign])] -> Maybe (Model v) Source
Model
findSample :: Ord v => Model v -> Cell (Polynomial Rational v) -> Maybe AReal Source