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

Copyright(c) Masahiro Sakai 2011-2013
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable (FlexibleInstances, MultiParamTypeClasses)
Safe HaskellSafe-Inferred
LanguageHaskell2010

ToySolver.Data.FOL.Arith

Contents

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

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

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

Eq r => Eq (SatResult r) 
Ord r => Ord (SatResult r) 
Show r => Show (SatResult r)