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

Eq r => Eq (Expr r)

Fractional r => Fractional (Expr r)

Num r => Num (Expr r)

Ord r => Ord (Expr r)

Show r => Show (Expr r)

Variables (Expr r)

IsRel (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.ArithRel

type Atom c = Rel (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)

Ord r => Ord (SatResult r)

Show r => Show (SatResult r)