Copyright	(c) Masahiro Sakai 2011-2013
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	TypeSynonymInstances FlexibleInstances ConstrainedClassMethods MultiParamTypeClasses

ToySolver.Data.FOL.Arith

Contents

Arithmetic expressions
Atomic formula
Arithmetic formula
Misc

Description

Arithmetic language (not limited to linear ones).

Synopsis

data Expr r
- = Const r
- | Var Var
- | (Expr r) :+: (Expr r)
- | (Expr r) :*: (Expr r)
- | (Expr r) :/: (Expr r)
var :: Var -> Expr r
evalExpr :: Fractional r => Model r -> Expr r -> r
module ToySolver.Data.OrdRel
type Atom c = OrdRel (Expr c)
evalAtom :: (Real r, Fractional r) => Model r -> Atom r -> Bool
module ToySolver.Data.FOL.Formula
data SatResult r
- = Unknown
- | Unsat
- | Sat (Model r)

Arithmetic expressions

data Expr r Source #

Constructors

Const r
Var Var
(Expr r) :+: (Expr r)
(Expr r) :*: (Expr r)
(Expr r) :/: (Expr r)

Instances

Instances details

Functor Expr Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods fmap :: (a -> b) -> Expr a -> Expr b # (<$) :: a -> Expr b -> Expr a #
Num r => Num (Expr r) Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods (+) :: Expr r -> Expr r -> Expr r # (-) :: Expr r -> Expr r -> Expr r # (*) :: Expr r -> Expr r -> Expr r # negate :: Expr r -> Expr r # abs :: Expr r -> Expr r # signum :: Expr r -> Expr r # fromInteger :: Integer -> Expr r #
Fractional r => Fractional (Expr r) Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods (/) :: Expr r -> Expr r -> Expr r # recip :: Expr r -> Expr r # fromRational :: Rational -> Expr r #
Show r => Show (Expr r) Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods showsPrec :: Int -> Expr r -> ShowS # show :: Expr r -> String # showList :: [Expr r] -> ShowS #
Eq r => Eq (Expr r) Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods (==) :: Expr r -> Expr r -> Bool # (/=) :: Expr r -> Expr r -> Bool #
Ord r => Ord (Expr r) Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods compare :: Expr r -> Expr r -> Ordering # (<) :: Expr r -> Expr r -> Bool # (<=) :: Expr r -> Expr r -> Bool # (>) :: Expr r -> Expr r -> Bool # (>=) :: Expr r -> Expr r -> Bool # max :: Expr r -> Expr r -> Expr r # min :: Expr r -> Expr r -> Expr r #
Variables (Expr r) Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods vars :: Expr r -> VarSet Source #
IsEqRel (Expr c) (Formula (Atom c)) Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods (.==.) :: Expr c -> Expr c -> Formula (Atom c) Source # (./=.) :: Expr c -> Expr c -> Formula (Atom c) Source #
IsOrdRel (Expr c) (Formula (Atom c)) Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods (.<.) :: Expr c -> Expr c -> Formula (Atom c) Source # (.<=.) :: Expr c -> Expr c -> Formula (Atom c) Source # (.>.) :: Expr c -> Expr c -> Formula (Atom c) Source # (.>=.) :: Expr c -> Expr c -> Formula (Atom c) Source # ordRel :: RelOp -> Expr c -> Expr c -> Formula (Atom c) Source #
Fractional r => Eval (Model r) (Expr r) r Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods eval :: Model r -> Expr r -> r Source #

var :: Var -> Expr r Source #

single variable expression

evalExpr :: Fractional r => Model r -> Expr r -> r Source #

evaluate an Expr with respect to a Model

Atomic formula

module ToySolver.Data.OrdRel

type Atom c = OrdRel (Expr c) Source #

Atomic formula

evalAtom :: (Real r, Fractional r) => Model r -> Atom r -> Bool Source #

Arithmetic formula

module ToySolver.Data.FOL.Formula

Misc

data SatResult r Source #

results of satisfiability checking

Constructors

Unknown
Unsat
Sat (Model r)

Instances

Instances details

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