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.
Get returns the i-th AST in the vector.
Size returns the number of ASTs in the vector.
String returns the string representation of the AST vector.
Config represents a Z3 configuration object.
SetParamValue sets a configuration parameter.
Context methods (receiver omitted for clarity)
AddRecDef adds the definition (body) for a recursive function created with MkRecFuncDecl.
Boolean operations MkAnd creates a conjunction.
MkApp creates a function application.
MkAtLeast encodes p1 + p2 + ... + pn >= k.
Pseudo-Boolean / cardinality constraints MkAtMost encodes p1 + p2 + ... + pn <= k.
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.
MkPBEq encodes k1*p1 + k2*p2 + ... + kn*pn = k.
MkPBGe encodes k1*p1 + k2*p2 + ... + kn*pn >= k.
MkPBLe encodes k1*p1 + k2*p2 + ... + kn*pn <= k.
MkQuantifier creates a quantifier with patterns
MkQuantifierConst creates a quantifier using constant bound variables
MkRecFuncDecl creates a recursive function declaration. After creating, use AddRecDef to provide the function body.
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.
Arg returns the i-th argument of an application expression.
Equal checks if two expressions are equal.
GetDecl returns the function declaration of an application expression.
GetSort returns the sort of the expression.
NumArgs returns the number of arguments of an application expression.
Simplify simplifies an expression.
String returns the string representation of the expression.
Substitute replaces every occurrence of from[i] in the expression with to[i]. The from and to slices must have the same length.
SubstituteFuns replaces every occurrence of from[i] applied to arguments with to[i] in the expression. The from and to slices must have the same length.
SubstituteVars replaces free variables in the expression with the expressions in to. Variable with de-Bruijn index i is replaced with to[i].
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.
GetGlobalParam retrieves the value of a global Z3 parameter. Returns the value and true if the parameter exists, or empty string and false otherwise.
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.
ResetAllGlobalParams resets all global Z3 parameters to their default values.
SetGlobalParam sets a global Z3 parameter.