Core types (Context, Config, Symbol, Sort, Expr, FuncDecl, Quantifier, Lambda) and basic operations
AST represents a Z3 abstract syntax tree node.
Equal checks if two ASTs are equal.
Hash returns the hash code of the AST.
String returns the string representation of the AST.
ASTVector represents a vector of Z3 ASTs.
Config represents a Z3 configuration object.
SetParamValue sets a configuration parameter.
Context methods (receiver omitted for clarity)
Boolean operations MkAnd creates a conjunction.
MkApp creates a function application.
MkBool creates a Boolean constant.
MkBoolConst creates a Boolean constant (variable) with the given name.
MkBoolSort creates the Boolean sort.
MkBvSort creates a bit-vector sort of the given size.
MkConst creates a constant (variable) with the given name and sort.
MkDistinct creates a distinct constraint.
Comparison operations MkEq creates an equality.
MkExists creates an existential quantifier.
MkFalse creates the Boolean constant false.
Quantifier operations MkForall creates a universal quantifier.
MkFuncDecl creates a function declaration.
MkIff creates a bi-implication (if and only if).
MkImplies creates an implication.
MkIntSymbol creates an integer symbol.
MkLambda creates a lambda expression with sorts and names
MkLambdaConst creates a lambda expression using constant bound variables
MkNot creates a negation.
MkNumeral creates a numeral from a string.
MkOr creates a disjunction.
MkQuantifier creates a quantifier with patterns
MkQuantifierConst creates a quantifier using constant bound variables
MkStringSymbol creates a string symbol.
MkTrue creates the Boolean constant true.
MkTypeVariable creates a type variable sort for use in polymorphic functions and datatypes
MkXor creates exclusive or.
SetParam sets a global or context parameter.
Expr represents a Z3 expression.
Equal checks if two expressions are equal.
GetSort returns the sort of the expression.
Simplify simplifies an expression.
String returns the string representation of the expression.
FuncDecl represents a function declaration.
GetArity returns the arity (number of parameters) of the function.
GetDomain returns the sort of the i-th parameter.
GetName returns the name of the function declaration.
GetRange returns the sort of the return value.
String returns the string representation of the function declaration.
Lambda represents a lambda expression
AsExpr converts a Lambda to an Expr
GetBody returns the body of the lambda expression
GetBoundName returns the name of the bound variable at the given index
GetBoundSort returns the sort of the bound variable at the given index
GetNumBound returns the number of bound variables
String returns the string representation of the lambda
ParamDescrs represents parameter descriptions for Z3 objects.
Pattern represents a Z3 pattern for quantifier instantiation.
Quantifier represents a quantified formula (forall or exists)
AsExpr converts a Quantifier to an Expr
GetBody returns the body of the quantifier
GetBoundName returns the name of the bound variable at the given index
GetBoundSort returns the sort of the bound variable at the given index
GetNoPattern returns the no-pattern at the given index
GetNumBound returns the number of bound variables
GetNumNoPatterns returns the number of no-patterns
GetNumPatterns returns the number of patterns
GetPattern returns the pattern at the given index
GetWeight returns the weight of the quantifier
IsExistential returns true if this is an existential quantifier (exists)
IsUniversal returns true if this is a universal quantifier (forall)
String returns the string representation of the quantifier
Sort represents a Z3 sort (type).
Equal checks if two sorts are equal.
String returns the string representation of the sort.
Symbol represents a Z3 symbol.
String returns the string representation of the symbol.
NewConfig creates a new Z3 configuration.
NewContext creates a new Z3 context with default configuration.
NewContextWithConfig creates a new Z3 context with the given configuration.