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

Copyright(c) Masahiro Sakai 2015
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityunstable
Portabilitynon-portable (MultiParamTypeClasses, FlexibleInstances, DeriveDataTypeable, CPP, OverloadedStrings, ScopedTypeVariables)
Safe HaskellNone
LanguageHaskell2010

ToySolver.SMT

Contents

Description

 

Synopsis

The Solver type

Problem Specification

data SSym Source #

Sort symbols

Instances

Eq SSym Source # 

Methods

(==) :: SSym -> SSym -> Bool #

(/=) :: SSym -> SSym -> Bool #

Ord SSym Source # 

Methods

compare :: SSym -> SSym -> Ordering #

(<) :: SSym -> SSym -> Bool #

(<=) :: SSym -> SSym -> Bool #

(>) :: SSym -> SSym -> Bool #

(>=) :: SSym -> SSym -> Bool #

max :: SSym -> SSym -> SSym #

min :: SSym -> SSym -> SSym #

Show SSym Source # 

Methods

showsPrec :: Int -> SSym -> ShowS #

show :: SSym -> String #

showList :: [SSym] -> ShowS #

data Sort Source #

Constructors

Sort SSym [Sort] 

Instances

Eq Sort Source # 

Methods

(==) :: Sort -> Sort -> Bool #

(/=) :: Sort -> Sort -> Bool #

Ord Sort Source # 

Methods

compare :: Sort -> Sort -> Ordering #

(<) :: Sort -> Sort -> Bool #

(<=) :: Sort -> Sort -> Bool #

(>) :: Sort -> Sort -> Bool #

(>=) :: Sort -> Sort -> Bool #

max :: Sort -> Sort -> Sort #

min :: Sort -> Sort -> Sort #

Show Sort Source # 

Methods

showsPrec :: Int -> Sort -> ShowS #

show :: Sort -> String #

showList :: [Sort] -> ShowS #

VASortFun Sort Source # 

Methods

withSortVArgs :: ([Sort] -> Sort) -> Sort

arityVASortFun :: Sort -> Int

VASortFun a => VASortFun (Sort -> a) Source # 

Methods

withSortVArgs :: ([Sort] -> Sort) -> Sort -> a

arityVASortFun :: (Sort -> a) -> Int

type FunType = ([Sort], Sort) Source #

data Expr Source #

Constructors

EAp FSym [Expr] 
EValue !Value 

Instances

Eq Expr Source # 

Methods

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

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

Fractional Expr Source # 

Methods

(/) :: Expr -> Expr -> Expr #

recip :: Expr -> Expr #

fromRational :: Rational -> Expr #

Num Expr Source # 

Methods

(+) :: Expr -> Expr -> Expr #

(-) :: Expr -> Expr -> Expr #

(*) :: Expr -> Expr -> Expr #

negate :: Expr -> Expr #

abs :: Expr -> Expr #

signum :: Expr -> Expr #

fromInteger :: Integer -> Expr #

Ord Expr Source # 

Methods

compare :: Expr -> Expr -> Ordering #

(<) :: Expr -> Expr -> Bool #

(<=) :: Expr -> Expr -> Bool #

(>) :: Expr -> Expr -> Bool #

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

max :: Expr -> Expr -> Expr #

min :: Expr -> Expr -> Expr #

Show Expr Source # 

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

Boolean Expr Source # 

Methods

(.=>.) :: Expr -> Expr -> Expr Source #

(.<=>.) :: Expr -> Expr -> Expr Source #

Complement Expr Source # 

Methods

notB :: Expr -> Expr Source #

MonotoneBoolean Expr Source # 
VAFun Expr Source # 

Methods

withVArgs :: ([Expr] -> Expr) -> Expr

arityVAFun :: Expr -> Int

IfThenElse Expr Expr Source # 

Methods

ite :: Expr -> Expr -> Expr -> Expr Source #

IsOrdRel Expr Expr Source # 
IsEqRel Expr Expr Source # 

Methods

(.==.) :: Expr -> Expr -> Expr Source #

(./=.) :: Expr -> Expr -> Expr Source #

VAFun a => VAFun (Expr -> a) Source # 

Methods

withVArgs :: ([Expr] -> Expr) -> Expr -> a

arityVAFun :: (Expr -> a) -> Int

data Index Source #

Instances

Eq Index Source # 

Methods

(==) :: Index -> Index -> Bool #

(/=) :: Index -> Index -> Bool #

Ord Index Source # 

Methods

compare :: Index -> Index -> Ordering #

(<) :: Index -> Index -> Bool #

(<=) :: Index -> Index -> Bool #

(>) :: Index -> Index -> Bool #

(>=) :: Index -> Index -> Bool #

max :: Index -> Index -> Index #

min :: Index -> Index -> Index #

Show Index Source # 

Methods

showsPrec :: Int -> Index -> ShowS #

show :: Index -> String #

showList :: [Index] -> ShowS #

data FSym Source #

Constructors

FSym !InternedText [Index] 

Instances

Eq FSym Source # 

Methods

(==) :: FSym -> FSym -> Bool #

(/=) :: FSym -> FSym -> Bool #

Ord FSym Source # 

Methods

compare :: FSym -> FSym -> Ordering #

(<) :: FSym -> FSym -> Bool #

(<=) :: FSym -> FSym -> Bool #

(>) :: FSym -> FSym -> Bool #

(>=) :: FSym -> FSym -> Bool #

max :: FSym -> FSym -> FSym #

min :: FSym -> FSym -> FSym #

Show FSym Source # 

Methods

showsPrec :: Int -> FSym -> ShowS #

show :: FSym -> String #

showList :: [FSym] -> ShowS #

IsString FSym Source # 

Methods

fromString :: String -> FSym #

class VASortFun a Source #

Minimal complete definition

withSortVArgs, arityVASortFun

Instances

VASortFun Sort Source # 

Methods

withSortVArgs :: ([Sort] -> Sort) -> Sort

arityVASortFun :: Sort -> Int

VASortFun a => VASortFun (Sort -> a) Source # 

Methods

withSortVArgs :: ([Sort] -> Sort) -> Sort -> a

arityVASortFun :: (Sort -> a) -> Int

declareFun :: VAFun a => Solver -> String -> [Sort] -> Sort -> IO a Source #

class VAFun a Source #

Minimal complete definition

withVArgs, arityVAFun

Instances

VAFun Expr Source # 

Methods

withVArgs :: ([Expr] -> Expr) -> Expr

arityVAFun :: Expr -> Int

VAFun a => VAFun (Expr -> a) Source # 

Methods

withVArgs :: ([Expr] -> Expr) -> Expr -> a

arityVAFun :: (Expr -> a) -> Int

assert :: Solver -> Expr -> IO () Source #

Solving

push :: Solver -> IO () Source #

pop :: Solver -> IO () Source #

Inspecting models

data Model Source #

Instances

data FunDef Source #

Constructors

FunDef [([Value], Value)] Value 

Instances

modelGetAssertions :: Model -> [Expr] Source #

Constraints that cannot represented as function definitions.

For example, zero-division result values cannot be specified by function definition, because division is interpreted function.

Inspecting proofs