Copyright	(c) Masahiro Sakai 2015
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	unstable
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	ScopedTypeVariables OverloadedStrings DeriveDataTypeable TypeSynonymInstances FlexibleInstances ConstrainedClassMethods MultiParamTypeClasses ExplicitForAll

ToySolver.SMT

Contents

The Solver type
Problem Specification
Solving
Inspecting models
Inspecting proofs

Description

Synopsis

data Solver
newSolver :: IO Solver
data Exception
- = Error String
- | Unsupported
data SSym
- = SSymBool
- | SSymReal
- | SSymBitVec !Int
- | SSymUninterpreted !InternedText !Int
ssymArity :: SSym -> Int
data Sort = Sort SSym [Sort]
sBool :: Sort
sReal :: Sort
sBitVec :: Int -> Sort
type FunType = ([Sort], Sort)
data Expr
- = EAp FSym [Expr]
- | EValue !Value
exprSort :: Solver -> Expr -> IO Sort
data Index
- = IndexNumeral !Integer
- | IndexSymbol !InternedText
data FSym = FSym !InternedText [Index]
declareSSym :: Solver -> String -> Int -> IO SSym
declareSort :: VASortFun a => Solver -> String -> Int -> IO a
class VASortFun a
declareFSym :: Solver -> String -> [Sort] -> Sort -> IO FSym
declareFun :: VAFun a => Solver -> String -> [Sort] -> Sort -> IO a
declareConst :: Solver -> String -> Sort -> IO Expr
class VAFun a
assert :: Solver -> Expr -> IO ()
assertNamed :: Solver -> String -> Expr -> IO ()
getGlobalDeclarations :: Solver -> IO Bool
setGlobalDeclarations :: Solver -> Bool -> IO ()
checkSAT :: Solver -> IO Bool
checkSATAssuming :: Solver -> [Expr] -> IO Bool
push :: Solver -> IO ()
pop :: Solver -> IO ()
data Model
data Value
- = ValRational !Rational
- | ValBitVec !BV
- | ValBool !Bool
- | ValUninterpreted !Int !Sort
getModel :: Solver -> IO Model
eval :: Model -> Expr -> Value
valSort :: Value -> Sort
data FunDef = FunDef [([Value], Value)] Value
evalFSym :: Model -> FSym -> FunDef
modelGetAssertions :: Model -> [Expr]
getUnsatAssumptions :: Solver -> IO [Expr]
getUnsatCore :: Solver -> IO [String]

The Solver type

data Solver Source #

newSolver :: IO Solver Source #

data Exception Source #

Constructors

Error String
Unsupported

Instances

Instances details

Exception Exception Source #
Instance details Defined in ToySolver.SMT Methods toException :: Exception -> SomeException # fromException :: SomeException -> Maybe Exception # displayException :: Exception -> String #
Show Exception Source #
Instance details Defined in ToySolver.SMT Methods showsPrec :: Int -> Exception -> ShowS # show :: Exception -> String # showList :: [Exception] -> ShowS #

Problem Specification

data SSym Source #

Sort symbols

Constructors

SSymBool
SSymReal
SSymBitVec !Int
SSymUninterpreted !InternedText !Int

Instances

Instances details

Show SSym Source #
Instance details Defined in ToySolver.SMT Methods showsPrec :: Int -> SSym -> ShowS # show :: SSym -> String # showList :: [SSym] -> ShowS #
Eq SSym Source #
Instance details Defined in ToySolver.SMT Methods (==) :: SSym -> SSym -> Bool # (/=) :: SSym -> SSym -> Bool #
Ord SSym Source #
Instance details Defined in ToySolver.SMT 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 #

ssymArity :: SSym -> Int Source #

data Sort Source #

Constructors

Sort SSym [Sort]

Instances

Instances details

Show Sort Source #
Instance details Defined in ToySolver.SMT Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #
Eq Sort Source #
Instance details Defined in ToySolver.SMT Methods (==) :: Sort -> Sort -> Bool # (/=) :: Sort -> Sort -> Bool #
Ord Sort Source #
Instance details Defined in ToySolver.SMT 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 #
VASortFun Sort Source #
Instance details Defined in ToySolver.SMT Methods withSortVArgs :: ([Sort] -> Sort) -> Sort arityVASortFun :: Sort -> Int
VASortFun a => VASortFun (Sort -> a) Source #
Instance details Defined in ToySolver.SMT Methods withSortVArgs :: ([Sort] -> Sort) -> Sort -> a arityVASortFun :: (Sort -> a) -> Int

sBool :: Sort Source #

sReal :: Sort Source #

sBitVec :: Int -> Sort Source #

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

data Expr Source #

Constructors

EAp FSym [Expr]
EValue !Value

Instances

Instances details

Num Expr Source #
Instance details Defined in ToySolver.SMT Methods (+) :: Expr -> Expr -> Expr # (-) :: Expr -> Expr -> Expr # (*) :: Expr -> Expr -> Expr # negate :: Expr -> Expr # abs :: Expr -> Expr # signum :: Expr -> Expr # fromInteger :: Integer -> Expr #
Fractional Expr Source #
Instance details Defined in ToySolver.SMT Methods (/) :: Expr -> Expr -> Expr # recip :: Expr -> Expr # fromRational :: Rational -> Expr #
Show Expr Source #
Instance details Defined in ToySolver.SMT Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
Eq Expr Source #
Instance details Defined in ToySolver.SMT Methods (==) :: Expr -> Expr -> Bool # (/=) :: Expr -> Expr -> Bool #
Ord Expr Source #
Instance details Defined in ToySolver.SMT 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 #
Boolean Expr Source #
Instance details Defined in ToySolver.SMT Methods (.=>.) :: Expr -> Expr -> Expr Source # (.<=>.) :: Expr -> Expr -> Expr Source #
Complement Expr Source #
Instance details Defined in ToySolver.SMT Methods notB :: Expr -> Expr Source #
MonotoneBoolean Expr Source #
Instance details Defined in ToySolver.SMT Methods true :: Expr Source # false :: Expr Source # (.&&.) :: Expr -> Expr -> Expr Source # (.\|\|.) :: Expr -> Expr -> Expr Source # andB :: [Expr] -> Expr Source # orB :: [Expr] -> Expr Source #
VAFun Expr Source #
Instance details Defined in ToySolver.SMT Methods withVArgs :: ([Expr] -> Expr) -> Expr arityVAFun :: Expr -> Int
IfThenElse Expr Expr Source #
Instance details Defined in ToySolver.SMT Methods ite :: Expr -> Expr -> Expr -> Expr Source #
IsEqRel Expr Expr Source #
Instance details Defined in ToySolver.SMT Methods (.==.) :: Expr -> Expr -> Expr Source # (./=.) :: Expr -> Expr -> Expr Source #
IsOrdRel Expr Expr Source #
Instance details Defined in ToySolver.SMT Methods (.<.) :: Expr -> Expr -> Expr Source # (.<=.) :: Expr -> Expr -> Expr Source # (.>.) :: Expr -> Expr -> Expr Source # (.>=.) :: Expr -> Expr -> Expr Source # ordRel :: RelOp -> Expr -> Expr -> Expr Source #
VAFun a => VAFun (Expr -> a) Source #
Instance details Defined in ToySolver.SMT Methods withVArgs :: ([Expr] -> Expr) -> Expr -> a arityVAFun :: (Expr -> a) -> Int

exprSort :: Solver -> Expr -> IO Sort Source #

data Index Source #

Constructors

IndexNumeral !Integer
IndexSymbol !InternedText

Instances

Instances details

Show Index Source #
Instance details Defined in ToySolver.SMT Methods showsPrec :: Int -> Index -> ShowS # show :: Index -> String # showList :: [Index] -> ShowS #
Eq Index Source #
Instance details Defined in ToySolver.SMT Methods (==) :: Index -> Index -> Bool # (/=) :: Index -> Index -> Bool #
Ord Index Source #
Instance details Defined in ToySolver.SMT 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 #

data FSym Source #

Constructors

FSym !InternedText [Index]

Instances

Instances details

IsString FSym Source #
Instance details Defined in ToySolver.SMT Methods fromString :: String -> FSym #
Show FSym Source #
Instance details Defined in ToySolver.SMT Methods showsPrec :: Int -> FSym -> ShowS # show :: FSym -> String # showList :: [FSym] -> ShowS #
Eq FSym Source #
Instance details Defined in ToySolver.SMT Methods (==) :: FSym -> FSym -> Bool # (/=) :: FSym -> FSym -> Bool #
Ord FSym Source #
Instance details Defined in ToySolver.SMT 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 #

declareSSym :: Solver -> String -> Int -> IO SSym Source #

declareSort :: VASortFun a => Solver -> String -> Int -> IO a Source #

class VASortFun a Source #

Minimal complete definition

withSortVArgs, arityVASortFun

Instances

Instances details

VASortFun Sort Source #
Instance details Defined in ToySolver.SMT Methods withSortVArgs :: ([Sort] -> Sort) -> Sort arityVASortFun :: Sort -> Int
VASortFun a => VASortFun (Sort -> a) Source #
Instance details Defined in ToySolver.SMT Methods withSortVArgs :: ([Sort] -> Sort) -> Sort -> a arityVASortFun :: (Sort -> a) -> Int

declareFSym :: Solver -> String -> [Sort] -> Sort -> IO FSym Source #

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

declareConst :: Solver -> String -> Sort -> IO Expr Source #

class VAFun a Source #

Minimal complete definition

withVArgs, arityVAFun

Instances

Instances details

VAFun Expr Source #
Instance details Defined in ToySolver.SMT Methods withVArgs :: ([Expr] -> Expr) -> Expr arityVAFun :: Expr -> Int
VAFun a => VAFun (Expr -> a) Source #
Instance details Defined in ToySolver.SMT Methods withVArgs :: ([Expr] -> Expr) -> Expr -> a arityVAFun :: (Expr -> a) -> Int

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

assertNamed :: Solver -> String -> Expr -> IO () Source #

getGlobalDeclarations :: Solver -> IO Bool Source #

setGlobalDeclarations :: Solver -> Bool -> IO () Source #

Solving

checkSAT :: Solver -> IO Bool Source #

checkSATAssuming :: Solver -> [Expr] -> IO Bool Source #

push :: Solver -> IO () Source #

pop :: Solver -> IO () Source #

Inspecting models

data Model Source #

Instances

Instances details

Show Model Source #
Instance details Defined in ToySolver.SMT Methods showsPrec :: Int -> Model -> ShowS # show :: Model -> String # showList :: [Model] -> ShowS #

data Value Source #

Constructors

ValRational !Rational
ValBitVec !BV
ValBool !Bool
ValUninterpreted !Int !Sort

Instances

Instances details

Show Value Source #
Instance details Defined in ToySolver.SMT Methods showsPrec :: Int -> Value -> ShowS # show :: Value -> String # showList :: [Value] -> ShowS #
Eq Value Source #
Instance details Defined in ToySolver.SMT Methods (==) :: Value -> Value -> Bool # (/=) :: Value -> Value -> Bool #
Ord Value Source #
Instance details Defined in ToySolver.SMT Methods compare :: Value -> Value -> Ordering # (<) :: Value -> Value -> Bool # (<=) :: Value -> Value -> Bool # (>) :: Value -> Value -> Bool # (>=) :: Value -> Value -> Bool # max :: Value -> Value -> Value # min :: Value -> Value -> Value #

getModel :: Solver -> IO Model Source #

eval :: Model -> Expr -> Value Source #

valSort :: Value -> Sort Source #

data FunDef Source #

Constructors

FunDef [([Value], Value)] Value

Instances

Instances details

Show FunDef Source #
Instance details Defined in ToySolver.SMT Methods showsPrec :: Int -> FunDef -> ShowS # show :: FunDef -> String # showList :: [FunDef] -> ShowS #
Eq FunDef Source #
Instance details Defined in ToySolver.SMT Methods (==) :: FunDef -> FunDef -> Bool # (/=) :: FunDef -> FunDef -> Bool #

evalFSym :: Model -> FSym -> FunDef Source #

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

getUnsatAssumptions :: Solver -> IO [Expr] Source #

getUnsatCore :: Solver -> IO [String] Source #