Copyright | (c) Masahiro Sakai 2015 |
---|---|
License | BSD-style |
Maintainer | masahiro.sakai@gmail.com |
Stability | unstable |
Portability | non-portable (MultiParamTypeClasses, FlexibleInstances, DeriveDataTypeable, CPP) |
Safe Haskell | None |
Language | Haskell2010 |
- data Solver
- newSolver :: IO Solver
- data Exception
- data SSym
- ssymArity :: SSym -> Int
- data Sort = Sort SSym [Sort]
- sBool :: Sort
- sReal :: Sort
- type FunType = ([Sort], Sort)
- data Expr
- exprSort :: Solver -> Expr -> IO Sort
- type FSym = String
- 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
- | ValBool !Bool
- | ValUninterpreted !Int !Sort
- getModel :: Solver -> IO Model
- eval :: Model -> Expr -> Value
- valSort :: Model -> Value -> Sort
- data FunDef = FunDef [([Value], Value)] Value
- evalFSym :: Model -> FSym -> FunDef
- getUnsatAssumptions :: Solver -> IO [Expr]
- getUnsatCore :: Solver -> IO [String]
The Solver type
Problem Specification
Sort symbols
Eq Expr Source # | |
Fractional Expr Source # | |
Num Expr Source # | |
Ord Expr Source # | |
Show Expr Source # | |
Boolean Expr Source # | |
Complement Expr Source # | |
MonotoneBoolean Expr Source # | |
VAFun Expr Source # | |
IfThenElse Expr Expr Source # | |
IsOrdRel Expr Expr Source # | |
IsEqRel Expr Expr Source # | |
VAFun a => VAFun (Expr -> a) Source # | |
withSortVArgs, arityVASortFun
withVArgs, arityVAFun