ToySolver.Data.FOL.Arith

Arithmetic language (not limited to linear ones).

Arithmetic expressions

data Expr r

Arithmetic expressions

Constructors

Const r

Var Var

(Expr r) :+: (Expr r)

(Expr r) :*: (Expr r)

(Expr r) :/: (Expr r)

Instances

Functor Expr

Methods

fmap :: (a -> b) -> Expr a -> Expr b

(<$) :: a -> Expr b -> Expr a

Eq r => Eq (Expr r)

Methods

(==) :: Expr r -> Expr r -> Bool

(/=) :: Expr r -> Expr r -> Bool

Fractional r => Fractional (Expr r)

Methods

(/) :: Expr r -> Expr r -> Expr r

recip :: Expr r -> Expr r

fromRational :: Rational -> Expr r

Num r => Num (Expr r)

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

Ord r => Ord (Expr r)

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

Show r => Show (Expr r)

Methods

showsPrec :: Int -> Expr r -> ShowS

show :: Expr r -> String

showList :: [Expr r] -> ShowS

Variables (Expr r)

Methods

vars :: Expr r -> VarSet

IsOrdRel (Expr c) (Formula (Atom c))

Methods

(.<.) :: Expr c -> Expr c -> Formula (Atom c)

(.<=.) :: Expr c -> Expr c -> Formula (Atom c)

(.>.) :: Expr c -> Expr c -> Formula (Atom c)

(.>=.) :: Expr c -> Expr c -> Formula (Atom c)

ordRel :: RelOp -> Expr c -> Expr c -> Formula (Atom c)

IsEqRel (Expr c) (Formula (Atom c))

Methods

(.==.) :: Expr c -> Expr c -> Formula (Atom c)

(./=.) :: Expr c -> Expr c -> Formula (Atom c)

var :: Var -> Expr r

single variable expression

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

evaluate an Expr with respect to a Model

Atomic formula

module ToySolver.Data.OrdRel

type Atom c = OrdRel (Expr c)

Atomic formula

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

Arithmetic formula

module ToySolver.Data.FOL.Formula

Misc

data SatResult r

results of satisfiability checking

Constructors

Unknown

Unsat

Sat (Model r)

Instances

Eq r => Eq (SatResult r)

Methods

(==) :: SatResult r -> SatResult r -> Bool

(/=) :: SatResult r -> SatResult r -> Bool

Ord r => Ord (SatResult r)

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

Show r => Show (SatResult r)

Methods

showsPrec :: Int -> SatResult r -> ShowS

show :: SatResult r -> String

showList :: [SatResult r] -> ShowS