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 |
|
Synopsis
- data Solver
- newSolver :: IO Solver
- data Exception
- data SSym
- ssymArity :: SSym -> Int
- data Sort = Sort SSym [Sort]
- sBool :: Sort
- sReal :: Sort
- sBitVec :: Int -> Sort
- type FunType = ([Sort], Sort)
- data Expr
- exprSort :: Solver -> Expr -> IO Sort
- data Index
- 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
Instances
Exception Exception Source # | |
Defined in ToySolver.SMT toException :: Exception -> SomeException # fromException :: SomeException -> Maybe Exception # displayException :: Exception -> String # | |
Show Exception Source # | |
Problem Specification
Instances
Show Sort Source # | |
Eq Sort Source # | |
Ord Sort Source # | |
VASortFun Sort Source # | |
Defined in ToySolver.SMT withSortVArgs :: ([Sort] -> Sort) -> Sort arityVASortFun :: Sort -> Int | |
VASortFun a => VASortFun (Sort -> a) Source # | |
Defined in ToySolver.SMT withSortVArgs :: ([Sort] -> Sort) -> Sort -> a arityVASortFun :: (Sort -> a) -> Int |
Instances
Num Expr Source # | |
Fractional Expr Source # | |
Show Expr Source # | |
Eq Expr Source # | |
Ord Expr Source # | |
Boolean Expr Source # | |
Complement Expr Source # | |
MonotoneBoolean Expr Source # | |
VAFun Expr Source # | |
Defined in ToySolver.SMT | |
IfThenElse Expr Expr Source # | |
IsEqRel Expr Expr Source # | |
IsOrdRel Expr Expr Source # | |
VAFun a => VAFun (Expr -> a) Source # | |
Defined in ToySolver.SMT |
withSortVArgs, arityVASortFun
Instances
VASortFun Sort Source # | |
Defined in ToySolver.SMT withSortVArgs :: ([Sort] -> Sort) -> Sort arityVASortFun :: Sort -> Int | |
VASortFun a => VASortFun (Sort -> a) Source # | |
Defined in ToySolver.SMT withSortVArgs :: ([Sort] -> Sort) -> Sort -> a arityVASortFun :: (Sort -> a) -> Int |
withVArgs, arityVAFun
Solving
Inspecting models
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.