ToySolver.SMT

The Solver type

data Solver

newSolver :: IO Solver

data Exception

Constructors

Error String

Unsupported

Instances

Show Exception

Methods

showsPrec :: Int -> Exception -> ShowS

show :: Exception -> String

showList :: [Exception] -> ShowS

Exception Exception

Methods

toException :: Exception -> SomeException

fromException :: SomeException -> Maybe Exception

displayException :: Exception -> String

Problem Specification

data SSym

Sort symbols

Constructors

SSymBool

SSymReal

SSymUserDeclared String !Int

Instances

Eq SSym

Methods

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

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

Ord SSym

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

Methods

showsPrec :: Int -> SSym -> ShowS

show :: SSym -> String

showList :: [SSym] -> ShowS

ssymArity :: SSym -> Int

data Sort

Constructors

Sort SSym [Sort]

Instances

Eq Sort

Methods

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

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

Ord Sort

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

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

VASortFun Sort

Methods

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

arityVASortFun :: Sort -> Int

VASortFun a => VASortFun (Sort -> a)

Methods

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

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

sBool :: Sort

sReal :: Sort

type FunType = ([Sort], Sort)

data Expr

Constructors

EAp FSym [Expr]

EFrac Rational

Instances

Eq Expr

Methods

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

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

Fractional Expr

Methods

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

recip :: Expr -> Expr

fromRational :: Rational -> Expr

Num Expr

Methods

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

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

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

negate :: Expr -> Expr

abs :: Expr -> Expr

signum :: Expr -> Expr

fromInteger :: Integer -> Expr

Ord Expr

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

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

Boolean Expr

Methods

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

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

Complement Expr

Methods

notB :: Expr -> Expr

MonotoneBoolean Expr

Methods

true :: Expr

false :: Expr

(.&&.) :: Expr -> Expr -> Expr

(.||.) :: Expr -> Expr -> Expr

andB :: [Expr] -> Expr

orB :: [Expr] -> Expr

VAFun Expr

Methods

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

arityVAFun :: Expr -> Int

IfThenElse Expr Expr

Methods

ite :: Expr -> Expr -> Expr -> Expr

IsOrdRel Expr Expr

Methods

(.<.) :: Expr -> Expr -> Expr

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

(.>.) :: Expr -> Expr -> Expr

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

ordRel :: RelOp -> Expr -> Expr -> Expr

IsEqRel Expr Expr

Methods

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

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

VAFun a => VAFun (Expr -> a)

Methods

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

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

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

Minimal complete definition

withSortVArgs, arityVASortFun

Instances

VASortFun Sort

Methods

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

arityVASortFun :: Sort -> Int

VASortFun a => VASortFun (Sort -> a)

Methods

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

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

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

Minimal complete definition

withVArgs, arityVAFun

Instances

VAFun Expr

Methods

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

arityVAFun :: Expr -> Int

VAFun a => VAFun (Expr -> a)

Methods

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

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

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

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

getGlobalDeclarations :: Solver -> IO Bool

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

Solving

checkSAT :: Solver -> IO Bool

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

push :: Solver -> IO ()

pop :: Solver -> IO ()

Inspecting models

data Model

Instances

Show Model

Methods

showsPrec :: Int -> Model -> ShowS

show :: Model -> String

showList :: [Model] -> ShowS

data Value

Constructors

ValRational !Rational

ValBool !Bool

ValUninterpreted !Int !Sort

Instances

Eq Value

Methods

(==) :: Value -> Value -> Bool

(/=) :: Value -> Value -> Bool

Show Value

Methods

showsPrec :: Int -> Value -> ShowS

show :: Value -> String

showList :: [Value] -> ShowS

getModel :: Solver -> IO Model

eval :: Model -> Expr -> Value

valSort :: Model -> Value -> Sort

data FunDef

Constructors

FunDef [([Value], Value)] Value

evalFSym :: Model -> FSym -> FunDef

Inspecting proofs

getUnsatAssumptions :: Solver -> IO [Expr]

getUnsatCore :: Solver -> IO [String]