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 |

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 :: 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

NegInf | |

RootOf (UPolynomial c) Int | |

PosInf |

# 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 AReal Source