Copyright	(c) Masahiro Sakai 2015
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	unstable
Portability	non-portable
Safe Haskell	None
Language	Haskell2010
Extensions	Cpp 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

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

Problem Specification

data SSym Source #

Sort symbols

Constructors

SSymBool
SSymReal
SSymBitVec !Int
SSymUninterpreted !InternedText !Int

Instances

Instances details

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

ssymArity :: SSym -> Int Source #

data Sort Source #

Constructors

Sort SSym [Sort]

Instances

Instances details

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 #
Show Sort Source #
Instance details Defined in ToySolver.SMT Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #
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

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

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

data FSym Source #

Constructors

FSym !InternedText [Index]

Instances

Instances details

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

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 #
Show Value Source #
Instance details Defined in ToySolver.SMT Methods showsPrec :: Int -> Value -> ShowS # show :: Value -> String # showList :: [Value] -> ShowS #

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

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

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 #