toysolver-0.7.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2011-2013
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010
Extensions
  • TypeSynonymInstances
  • FlexibleInstances
  • ConstrainedClassMethods
  • MultiParamTypeClasses

ToySolver.Data.FOL.Arith

Description

Arithmetic language (not limited to linear ones).

Synopsis

Arithmetic expressions

data Expr r Source #

Arithmetic expressions

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 #

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 #

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 #

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 #

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 #

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 #

Variables (Expr r) Source # 
Instance details

Defined in ToySolver.Data.FOL.Arith

Methods

vars :: Expr r -> VarSet 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 #

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 #

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

type Atom c = OrdRel (Expr c) Source #

Atomic formula

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

Arithmetic formula

Misc

data SatResult r Source #

results of satisfiability checking

Constructors

Unknown 
Unsat 
Sat (Model r) 

Instances

Instances details
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

Show r => Show (SatResult r) Source # 
Instance details

Defined in ToySolver.Data.FOL.Arith