SVF Python Z3 API

Z3Mgr API Documentation

Z3Mgr

Method	Description
getZ3Expr(var_id: int, ctx)	Retrieves the Z3 expression for a given variable ID within a context.
getZ3Val(int literal)	Return the z3 expression for int literal (e.g., 0 and 1). DO NOT use getZ3Expr(0) or getZ3Expr(1) for int constants in Assignment-2.
addToSolver(expr)	Adds an expression to the Z3 solver.
solver.push()	Pushes a context onto the solver stack.
solver.pop()	Pops a context from the solver stack.
solver.check()	Checks the satisfiability of the current solver context.
getMemObjAddress(var_id: int)	Retrieves the memory object address for a given variable ID.
loadValue(expr)	Loads a value from a given Z3 expression.
storeValue(lhs, rhs)	Stores a value into a location.
getGepOffset(stmt, ctx)	Retrieves the offset for a GEP statement.
getGepObjAddress(rhs, offset)	Retrieves the address for a GEP object with a given offset.
updateZ3Expr(idx: int, target)	Updates the Z3 expression for a given index.
getEvalExpr(e)	Evaluates a Z3 expression and returns the result.
checkNegateAssert	For assert (Q), add ¬Q to the solver to prove the absence of counterexamples; It returns true if it is the absence of counterexamples, otherwise it has at least one counterexample

SSE

Method	Description
createExprForObjVar(obj_var)	Creates a Z3 expression for an object variable.
getGepOffset(gep, callingCtx)	Retrieves the offset for a GEP statement within a calling context.
printExprValues(callingCtx)	Prints the values of all Z3 expressions within a calling context.
callingCtxToStr(callingCtx)	Converts a calling context to a string representation.
getZ3Expr(idx, callingCtx)	Retrieves the Z3 expression for a given index and calling context.
getEvalExpr(e)	Evaluates a Z3 expression and returns the result.

Z3 Python API Reference

If you cannot find the following API, please install python3 -m pip install z3-solver

1️⃣ Creating Z3 Expressions

API	Description
z3.Int(name, ctx=...)	Creates a symbolic integer variable.
z3.IntVal(value, ctx=...)	Creates a constant integer value as a Z3 expression.
z3.Bool(name, ctx=...) ✳️	Creates a symbolic boolean variable.
z3.Real(name, ctx=...) ✳️	Creates a symbolic real variable.
z3.RealVal(value, ctx=...) ✳️	Creates a constant real number as a Z3 expression.

2️⃣ Conditional and Logical Expressions

API	Description
z3.If(cond, then_expr, else_expr)	Constructs a conditional expression (if-then-else).
z3.And(e1, e2, ...)	Logical conjunction (AND) of multiple boolean expressions.
z3.Or(e1, e2, ...) ✳️	Logical disjunction (OR) of multiple boolean expressions.
z3.Not(expr)	Logical negation.
z3.Implies(a, b) ✳️	Logical implication (a implies b).
z3.Equals(a, b) ✳️	Explicit equality expression (alternative to a == b).

3️⃣ Memory Modeling (Arrays)

API	Description
z3.ArraySort(index_sort, elem_sort)	Defines the type of arrays from index_sort to elem_sort.
z3.Const(name, sort)	Declares a named constant of a given sort (e.g., memory array).
z3.Store(array, index, value)	Returns a new array with the value at index updated to value.
z3.Select(array, index)	Retrieves the value stored at a given index of an array.

4️⃣ Solver and Model Interaction

API	Description
z3.Solver(ctx=...)	Creates a new Z3 solver instance.
solver.add(expr)	Adds a constraint expression to the solver.
solver.check()	Checks satisfiability of the current constraint set.
solver.model()	Returns a model (variable assignment) if satisfiable.
model.eval(expr, model_completion=True)	Evaluates an expression under the model, filling in undefined values if needed.
solver.push() / solver.pop()	Saves and restores the solver state (for backtracking and scoping).

5️⃣ Contexts and Basic Types

API	Description
z3.Context()	Creates a new isolated Z3 context to manage expressions and solvers.
z3.IntSort(ctx=...)	Returns the integer sort, used for defining array types.
z3.BoolSort(ctx=...) ✳️	Returns the boolean sort type.
z3.unsat	A constant representing an unsatisfiable result from the solver.
z3.sat ✳️	A constant representing a satisfiable result from the solver.
z3.unknown ✳️	Indicates that the solver could not determine satisfiability.