| Portability | non-portable (ScopedTypeVariables, BangPatterns) |
|---|---|
| Stability | provisional |
| Maintainer | masahiro.sakai@gmail.com |
| Safe Haskell | None |
Algorithm.CAD
Contents
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
- module Data.Sign
- project :: forall v. (Ord v, Show v, PrettyVar v) => [(UPolynomial (Polynomial Rational v), [Sign])] -> [([(Polynomial Rational v, [Sign])], [Cell (Polynomial Rational v)])]
- solve :: forall v. (Ord v, Show v, PrettyVar v) => Set v -> [Rel (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 |
module Data.Sign
Projection
project :: forall v. (Ord v, Show v, PrettyVar v) => [(UPolynomial (Polynomial Rational v), [Sign])] -> [([(Polynomial Rational v, [Sign])], [Cell (Polynomial Rational v)])]Source
Solving
solve :: forall v. (Ord v, Show v, PrettyVar v) => Set v -> [Rel (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 ARealSource