Z3.Base

Types

data Config

data Context

data Symbol

data AST

data Sort

data FuncDecl

data App

data Pattern

data Constructor

data Model

data FuncInterp

data FuncEntry

data Params

data Solver

data ASTKind

Satisfiability result

data Result

Create configuration

mkConfig

delConfig

setParamValue

Helpers

withConfig

Create context

mkContext

withContext

Parameters

mkParams

paramsSetBool

paramsSetUInt

paramsSetDouble

paramsSetSymbol

paramsToString

Symbols

mkIntSymbol

mkStringSymbol

Sorts

mkUninterpretedSort

mkBoolSort

mkIntSort

mkRealSort

mkBvSort

mkArraySort

mkTupleSort

mkConstructor

mkDatatype

Constants and Applications

mkFuncDecl

mkApp

mkConst

mkFreshFuncDecl

mkFreshConst

Helpers

mkVar

mkBoolVar

mkRealVar

mkIntVar

mkBvVar

mkFreshVar

mkFreshBoolVar

mkFreshRealVar

mkFreshIntVar

mkFreshBvVar

Propositional Logic and Equality

mkTrue

mkFalse

mkEq

mkNot

mkIte

mkIff

mkImplies

mkXor

mkAnd

mkOr

mkDistinct

Helpers

mkBool

Arithmetic: Integers and Reals

mkAdd

mkMul

mkSub

mkUnaryMinus

mkDiv

mkMod

mkRem

mkLt

mkLe

mkGt

mkGe

mkInt2Real

mkReal2Int

mkIsInt

Bit-vectors

mkBvnot

mkBvredand

mkBvredor

mkBvand

mkBvor

mkBvxor

mkBvnand

mkBvnor

mkBvxnor

mkBvneg

mkBvadd

mkBvsub

mkBvmul

mkBvudiv

mkBvsdiv

mkBvurem

mkBvsrem

mkBvsmod

mkBvult

mkBvslt

mkBvule

mkBvsle

mkBvuge

mkBvsge

mkBvugt

mkBvsgt

mkConcat

mkExtract

mkSignExt

mkZeroExt

mkRepeat

mkBvshl

mkBvlshr

mkBvashr

mkRotateLeft

mkRotateRight

mkExtRotateLeft

mkExtRotateRight

mkInt2bv

mkBv2int

mkBvnegNoOverflow

mkBvaddNoOverflow

mkBvaddNoUnderflow

mkBvsubNoOverflow

mkBvsubNoUnderflow

mkBvmulNoOverflow

mkBvmulNoUnderflow

mkBvsdivNoOverflow

Arrays

mkSelect

mkStore

mkConstArray

mkMap

mkArrayDefault

Numerals

mkNumeral

mkReal

mkInt

mkUnsignedInt

mkInt64

mkUnsignedInt64

Helpers

mkIntegral

mkRational

mkFixed

mkRealNum

mkInteger

mkIntNum

mkBitvector

mkBvNum

Quantifiers

mkPattern

mkBound

mkForall

mkExists

mkForallConst

mkExistsConst

Accessors

getSymbolString

getBvSortSize

getDatatypeSortConstructors

getDatatypeSortRecognizers

getDeclName

getSort

getBoolValue

getAstKind

toApp

getNumeralString

Helpers

getBool

getInt

getReal

getBv

Models

modelEval

evalArray

getFuncInterp

isAsArray

getAsArrayFuncDecl

funcInterpGetNumEntries

funcInterpGetEntry

funcInterpGetElse

funcInterpGetArity

funcEntryGetValue

funcEntryGetNumArgs

funcEntryGetArg

modelToString

showModel

Helpers

type EvalAst a

eval

evalBool

evalInt

evalReal

evalBv

mapEval

evalT

data FuncModel

evalFunc

String Conversion

data ASTPrintMode

setASTPrintMode

astToString

patternToString

sortToString

funcDeclToString

benchmarkToSMTLibString

Error Handling

data Z3Error

data Z3ErrorCode

Miscellaneous

data Version

getVersion

Solvers

data Logic

mkSolver

mkSimpleSolver

mkSolverForLogic

solverGetHelp

solverSetParams

solverPush

solverPop

solverReset

solverGetNumScopes

solverAssertCnstr

solverAssertAndTrack

solverCheck

solverCheckAssumptions

solverGetModel

solverGetUnsatCore

solverGetReasonUnknown

solverToString

Helpers

solverCheckAndGetModel