ToySolver.SMT

The Solver type

data Solver

newSolver

data Exception

Problem Specification

data SSym

ssymArity

data Sort

sBool

sReal

type FunType

data Expr

exprSort

type 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

Inspecting proofs

getUnsatAssumptions

getUnsatCore