toysolver-0.8.1: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc

Copyright	(c) Masahiro Sakai 2012
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	ScopedTypeVariables BangPatterns ExplicitForAll

ToySolver.Arith.CAD

Contents

Basic data structures
Projection
Solving
Model

Description

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/

Synopsis

data Point c
- = NegInf
- | RootOf (UPolynomial c) Int
- | PosInf
data Cell c
- = Point (Point c)
- | Interval (Point c) (Point c)
project :: (Ord v, Show v, PrettyVar v) => v -> [OrdRel (Polynomial Rational v)] -> [([OrdRel (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 -> [OrdRel (Polynomial Rational v)] -> [([OrdRel (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 -> [OrdRel (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

data Point c Source #

Constructors

NegInf
RootOf (UPolynomial c) Int
PosInf

Instances

Instances details

Show c => Show (Point c) Source #
Instance details Defined in ToySolver.Arith.CAD Methods showsPrec :: Int -> Point c -> ShowS # show :: Point c -> String # showList :: [Point c] -> ShowS #
Eq c => Eq (Point c) Source #
Instance details Defined in ToySolver.Arith.CAD Methods (==) :: Point c -> Point c -> Bool # (/=) :: Point c -> Point c -> Bool #
Ord c => Ord (Point c) Source #
Instance details Defined in ToySolver.Arith.CAD Methods compare :: Point c -> Point c -> Ordering # (<) :: Point c -> Point c -> Bool # (<=) :: Point c -> Point c -> Bool # (>) :: Point c -> Point c -> Bool # (>=) :: Point c -> Point c -> Bool # max :: Point c -> Point c -> Point c # min :: Point c -> Point c -> Point c #

data Cell c Source #

Constructors

Point (Point c)
Interval (Point c) (Point c)

Instances

Instances details

Show c => Show (Cell c) Source #
Instance details Defined in ToySolver.Arith.CAD Methods showsPrec :: Int -> Cell c -> ShowS # show :: Cell c -> String # showList :: [Cell c] -> ShowS #
Eq c => Eq (Cell c) Source #
Instance details Defined in ToySolver.Arith.CAD Methods (==) :: Cell c -> Cell c -> Bool # (/=) :: Cell c -> Cell c -> Bool #
Ord c => Ord (Cell c) Source #
Instance details Defined in ToySolver.Arith.CAD Methods compare :: Cell c -> Cell c -> Ordering # (<) :: Cell c -> Cell c -> Bool # (<=) :: Cell c -> Cell c -> Bool # (>) :: Cell c -> Cell c -> Bool # (>=) :: Cell c -> Cell c -> Bool # max :: Cell c -> Cell c -> Cell c # min :: Cell c -> Cell c -> Cell c #

Projection

project :: (Ord v, Show v, PrettyVar v) => v -> [OrdRel (Polynomial Rational v)] -> [([OrdRel (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 -> [OrdRel (Polynomial Rational v)] -> [([OrdRel (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 -> [OrdRel (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

type Model v = Map v AReal Source #

findSample :: Ord v => Model v -> Cell (Polynomial Rational v) -> Maybe AReal Source #

evalCell :: Ord v => Model v -> Cell (Polynomial Rational v) -> Cell Rational Source #

evalPoint :: Ord v => Model v -> Point (Polynomial Rational v) -> Point Rational Source #