Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/Z3Prover/z3/llms.txt

Use this file to discover all available pages before exploring further.

​
Overview

The Context API provides functions for creating and managing Z3 contexts, which are the central objects for all Z3 operations. A context manages memory, configuration, and all Z3 objects.

​
Types

​
Z3_config

Configuration object used to initialize logical contexts. Created before context creation to set parameters.

​
Z3_context

Manager of all other Z3 objects, global configuration options, etc. All interaction with Z3 happens through a context.

​
Z3_lbool

Lifted Boolean type for three-valued logic:

​
Configuration Functions

​
Z3_mk_config

Z3_config Z3_API Z3_mk_config(void);
Create a configuration object for the Z3 context.
​
return
Z3_config
New configuration object
Description: Configurations are created to assign parameters prior to creating contexts. Available parameters:
  • proof (Boolean) - Enable proof generation
  • debug_ref_count (Boolean) - Enable debug support for Z3_ast reference counting
  • trace (Boolean) - Tracing support
  • timeout (unsigned) - Default timeout in milliseconds for solvers
  • well_sorted_check (Boolean) - Type checker
  • auto_config (Boolean) - Use heuristics to automatically select solver
  • model (Boolean) - Model generation for solvers
  • unsat_core (Boolean) - Unsat-core generation for solvers
Example: 
Z3_config cfg = Z3_mk_config();
Z3_set_param_value(cfg, "proof", "true");
Z3_set_param_value(cfg, "model", "true");

​
Z3_del_config

void Z3_API Z3_del_config(Z3_config c);
Delete the given configuration object.

​
Z3_set_param_value

void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value);
Set a configuration parameter.

​
Context Creation

​
Z3_mk_context

Z3_context Z3_API Z3_mk_context(Z3_config c);
Create a context using the given configuration.
​
return
Z3_context
New Z3 context
Description: After a context is created, the configuration cannot be changed. Z3_ast objects persist with the context lifetime (automatic memory management). Thread Safety: Objects created using a given context should not be accessed from different threads without synchronization. To use Z3 from different threads, create separate context objects. Example: 
Z3_config cfg = Z3_mk_config();
Z3_set_param_value(cfg, "model", "true");
Z3_context ctx = Z3_mk_context(cfg);
Z3_del_config(cfg);

// Use context...

Z3_del_context(ctx);

​
Z3_mk_context_rc

Z3_context Z3_API Z3_mk_context_rc(Z3_config c);
Create a context with manual reference counting for Z3_ast objects.
​
return
Z3_context
New Z3 context with manual reference counting
Description: In this context, the user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref when the Z3_ast is not needed anymore. This is more efficient but error-prone. Example: 
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context_rc(cfg);
Z3_del_config(cfg);

Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_inc_ref(ctx, Z3_sort_to_ast(ctx, int_sort));

// Use int_sort...

Z3_dec_ref(ctx, Z3_sort_to_ast(ctx, int_sort));
Z3_del_context(ctx);

​
Z3_del_context

void Z3_API Z3_del_context(Z3_context c);
Delete the given logical context.

​
Reference Counting

​
Z3_inc_ref

void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a);
Increment the reference counter of the given AST. Note: This is a NOOP if context was created using Z3_mk_context.

​
Z3_dec_ref

void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a);
Decrement the reference counter of the given AST. Note: This is a NOOP if context was created using Z3_mk_context.

​
Z3_enable_concurrent_dec_ref

void Z3_API Z3_enable_concurrent_dec_ref(Z3_context c);
Enable concurrency control for reference counting decrements. Description: Allows reference counting decrements in separate threads from the context. Must be called before using dec_ref from multiple threads.

​
Parameter Management

​
Z3_update_param_value

void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value);
Set a value of a context parameter.

​
Z3_interrupt

void Z3_API Z3_interrupt(Z3_context c);
Interrupt the execution of a Z3 procedure. Description: This procedure can be used to interrupt solvers, simplifiers, and tactics. Can be called from a different thread.

​
Global Parameters

​
Z3_global_param_set

void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value);
Set a global (or module) parameter shared by all Z3 contexts. Example: 
Z3_global_param_set("pp.decimal", "true");
Z3_global_param_set("smt.mbqi", "false");

​
Z3_global_param_reset_all

void Z3_API Z3_global_param_reset_all(void);
Restore the value of all global parameters to defaults.

​
Z3_global_param_get

bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value);
Get a global parameter value.
​
return
bool
True if parameter exists, false otherwise

Build docs developers (and LLMs) love

Get started for freeTalk to us