ToySolver.SMT

The Solver type

data Solver

newSolver

data Exception

Problem Specification

data SSym

ssymArity

data Sort

sBool

sReal

sBitVec

type FunType

data Expr

exprSort

data Index

data FSym

declareSSym

declareSort

class VASortFun a

declareFSym

declareFun

declareConst

class VAFun a

assert

assertNamed

getGlobalDeclarations

setGlobalDeclarations

Solving

checkSAT

checkSATAssuming

push

pop

Inspecting models

data Model

data Value

getModel

eval

valSort

data FunDef

evalFSym

modelGetAssertions

Inspecting proofs

getUnsatAssumptions

getUnsatCore