ToySolver.CAD

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/

Basic data structures

data Point c

Constructors

NegInf

RootOf (UPolynomial c) Int

PosInf

Instances

Eq c => Eq (Point c)

Ord c => Ord (Point c)

Show c => Show (Point c)

data Cell c

Constructors

Point (Point c)

Interval (Point c) (Point c)

Instances

Eq c => Eq (Cell c)

Ord c => Ord (Cell c)

Show c => Show (Cell c)

Projection

project :: forall v. (Ord v, Show v, PrettyVar v) => [(UPolynomial (Polynomial Rational v), [Sign])] -> [([(Polynomial Rational v, [Sign])], [Cell (Polynomial Rational v)])]

Solving

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)

Model

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