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 SortKind

data ASTKind

data Tactic

data ApplyResult

data Goal

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

mkDatatypes

mkSetSort

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

Sets

mkEmptySet

mkFullSet

mkSetAdd

mkSetDel

mkSetUnion

mkSetIntersect

mkSetDifference

mkSetComplement

mkSetMember

mkSetSubset

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

getSortKind

getBvSortSize

getDatatypeSortConstructors

getDatatypeSortRecognizers

getDatatypeSortConstructorAccessors

getDeclName

getArity

getDomain

getRange

appToAst

getAppDecl

getAppNumArgs

getAppArg

getAppArgs

getSort

getArraySortDomain

getArraySortRange

getBoolValue

getAstKind

isApp

toApp

getNumeralString

simplify

simplifyEx

getIndexValue

isQuantifierForall

isQuantifierExists

getQuantifierWeight

getQuantifierNumPatterns

getQuantifierPatternAST

getQuantifierPatterns

getQuantifierNumNoPatterns

getQuantifierNoPatternAST

getQuantifierNoPatterns

getQuantifierNumBound

getQuantifierBoundName

getQuantifierBoundSort

getQuantifierBoundVars

getQuantifierBody

Helpers

getBool

getInt

getReal

getBv

Modifiers

substituteVars

Models

modelEval

evalArray

getConstInterp

getFuncInterp

hasInterp

numConsts

numFuncs

getConstDecl

getFuncDecl

getConsts

getFuncs

isAsArray

addFuncInterp

addConstInterp

getAsArrayFuncDecl

funcInterpGetNumEntries

funcInterpGetEntry

funcInterpGetElse

funcInterpGetArity

funcEntryGetValue

funcEntryGetNumArgs

funcEntryGetArg

modelToString

showModel

Helpers

type EvalAst a

eval

evalBool

evalInt

evalReal

evalBv

mapEval

evalT

data FuncModel

evalFunc

Tactics

mkTactic

andThenTactic

orElseTactic

skipTactic

tryForTactic

mkQuantifierEliminationTactic

mkAndInverterGraphTactic

applyTactic

getApplyResultNumSubgoals

getApplyResultSubgoal

getApplyResultSubgoals

mkGoal

goalAssert

getGoalSize

getGoalFormula

getGoalFormulas

String Conversion

data ASTPrintMode

setASTPrintMode

astToString

patternToString

sortToString

funcDeclToString

benchmarkToSMTLibString

Parser interface

parseSMTLib2String

parseSMTLib2File

getParserError

Error Handling

data Z3Error

data Z3ErrorCode

Miscellaneous

data Version

getVersion

Fixedpoint

data Fixedpoint

mkFixedpoint

fixedpointPush

fixedpointPop

fixedpointAddRule

fixedpointSetParams

fixedpointRegisterRelation

fixedpointQueryRelations

fixedpointGetAnswer

fixedpointGetAssertions

Interpolation

data InterpolationProblem

mkInterpolant

mkInterpolationContext

getInterpolant

computeInterpolant

readInterpolationProblem

checkInterpolant

interpolationProfile

writeInterpolationProblem

Solvers

data Logic

mkSolver

mkSimpleSolver

mkSolverForLogic

solverGetHelp

solverSetParams

solverPush

solverPop

solverReset

solverGetNumScopes

solverAssertCnstr

solverAssertAndTrack

solverCheck

solverCheckAssumptions

solverGetModel

solverGetUnsatCore

solverGetReasonUnknown

solverToString

Helpers

solverCheckAndGetModel