Skip to main content

​
Overview

The Model API provides functions for extracting and interpreting models - satisfying assignments returned by the solver when a formula is satisfiable.

​
Types

​
Z3_model

A model for the constraints asserted into the logical context. Contains interpretations for constants and functions.

​
Z3_func_interp

Interpretation of a function in a model. Represents the graph of a function.

​
Z3_func_entry

Representation of a function interpretation entry at a particular point.

​
Model Creation and Reference Counting

​
Z3_mk_model

Z3_model Z3_API Z3_mk_model(Z3_context c);
Create an empty model.
​
return
Z3_model
New empty model

​
Z3_model_inc_ref

void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m);
Increment the reference counter of the model.

​
Z3_model_dec_ref

void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m);
Decrement the reference counter of the model. Example: 
Z3_model model = Z3_solver_get_model(ctx, solver);
Z3_model_inc_ref(ctx, model);
// Use model...
Z3_model_dec_ref(ctx, model);

​
Evaluating Expressions

​
Z3_model_eval

bool Z3_API Z3_model_eval(
    Z3_context c, 
    Z3_model m, 
    Z3_ast t,
    bool model_completion, 
    Z3_ast* v
);
Evaluate an expression in the model.
​
return
bool
True if evaluation succeeded
Description: Model completion assigns default values to constants not assigned by the model. Example: 
Z3_model model = Z3_solver_get_model(ctx, solver);
Z3_model_inc_ref(ctx, model);

Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), Z3_mk_int_sort(ctx));
Z3_ast value;

if (Z3_model_eval(ctx, model, x, true, &value)) {
    printf("x = %s\n", Z3_ast_to_string(ctx, value));
}

Z3_model_dec_ref(ctx, model);

​
Constant Interpretation

​
Z3_model_get_num_consts

unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m);
Return the number of constants assigned by the model.
​
return
unsigned
Number of constants

​
Z3_model_get_const_decl

Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i);
Return the i-th constant declaration.
​
return
Z3_func_decl
Constant declaration

​
Z3_model_get_const_interp

Z3_ast Z3_API Z3_model_get_const_interp(
    Z3_context c, 
    Z3_model m, 
    Z3_func_decl a
);
Return the interpretation of a constant.
​
return
Z3_ast
Value of the constant (NULL if not assigned)
Example: 
Z3_model model = Z3_solver_get_model(ctx, solver);
Z3_model_inc_ref(ctx, model);

unsigned num_consts = Z3_model_get_num_consts(ctx, model);
for (unsigned i = 0; i < num_consts; i++) {
    Z3_func_decl cnst = Z3_model_get_const_decl(ctx, model, i);
    Z3_symbol name = Z3_get_decl_name(ctx, cnst);
    Z3_ast value = Z3_model_get_const_interp(ctx, model, cnst);
    
    printf("%s = %s\n", 
           Z3_get_symbol_string(ctx, name),
           Z3_ast_to_string(ctx, value));
}

Z3_model_dec_ref(ctx, model);

​
Z3_model_has_interp

bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a);
Check if model has an interpretation for a declaration.
​
return
bool
True if interpretation exists

​
Function Interpretation

​
Z3_model_get_num_funcs

unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m);
Return the number of function interpretations.
​
return
unsigned
Number of functions

​
Z3_model_get_func_decl

Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i);
Return the i-th function declaration.
​
return
Z3_func_decl
Function declaration

​
Z3_model_get_func_interp

Z3_func_interp Z3_API Z3_model_get_func_interp(
    Z3_context c,
    Z3_model m, 
    Z3_func_decl f
);
Return the interpretation of a function.
​
return
Z3_func_interp
Function interpretation

​
Function Interpretation Details

​
Z3_func_interp_get_num_entries

unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f);
Return the number of entries in the function graph.
​
return
unsigned
Number of entries

​
Z3_func_interp_get_entry

Z3_func_entry Z3_API Z3_func_interp_get_entry(
    Z3_context c,
    Z3_func_interp f,
    unsigned i
);
Return the i-th entry in the function graph.
​
return
Z3_func_entry
Function entry

​
Z3_func_interp_get_else

Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f);
Return the ‘else’ value (default) for a function interpretation.
​
return
Z3_ast
Default value

​
Z3_func_entry_get_value

Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e);
Return the result value of a function entry.
​
return
Z3_ast
Result value

​
Z3_func_entry_get_num_args

unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e);
Return the number of arguments in a function entry.
​
return
unsigned
Number of arguments

​
Z3_func_entry_get_arg

Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i);
Return the i-th argument of a function entry.
​
return
Z3_ast
Argument value

​
Sort Universe

​
Z3_model_get_num_sorts

unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m);
Return the number of uninterpreted sorts with finite interpretations.
​
return
unsigned
Number of sorts

​
Z3_model_get_sort

Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i);
Return the i-th uninterpreted sort.
​
return
Z3_sort
Uninterpreted sort

​
Z3_model_get_sort_universe

Z3_ast_vector Z3_API Z3_model_get_sort_universe(
    Z3_context c,
    Z3_model m,
    Z3_sort s
);
Return the finite set of elements representing the interpretation of sort s.
​
return
Z3_ast_vector
Vector of elements in the sort’s universe

​
Model Conversion

​
Z3_model_to_string

Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m);
Convert model to a string representation.
​
return
Z3_string
String representation
Example: 
Z3_model model = Z3_solver_get_model(ctx, solver);
Z3_model_inc_ref(ctx, model);
printf("%s\n", Z3_model_to_string(ctx, model));
Z3_model_dec_ref(ctx, model);

​
Complete Example

#include <z3.h>
#include <stdio.h>

int main() {
    Z3_config cfg = Z3_mk_config();
    Z3_set_param_value(cfg, "model", "true");
    Z3_context ctx = Z3_mk_context(cfg);
    Z3_del_config(cfg);
    
    Z3_solver solver = Z3_mk_solver(ctx);
    Z3_solver_inc_ref(ctx, solver);
    
    // Create variables
    Z3_sort int_sort = Z3_mk_int_sort(ctx);
    Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), int_sort);
    Z3_ast y = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "y"), int_sort);
    
    // Assert x + y = 10 and x > 5
    Z3_ast args[2] = {x, y};
    Z3_ast sum = Z3_mk_add(ctx, 2, args);
    Z3_ast ten = Z3_mk_int(ctx, 10, int_sort);
    Z3_ast five = Z3_mk_int(ctx, 5, int_sort);
    
    Z3_solver_assert(ctx, solver, Z3_mk_eq(ctx, sum, ten));
    Z3_solver_assert(ctx, solver, Z3_mk_gt(ctx, x, five));
    
    if (Z3_solver_check(ctx, solver) == Z3_L_TRUE) {
        Z3_model model = Z3_solver_get_model(ctx, solver);
        Z3_model_inc_ref(ctx, model);
        
        // Evaluate expressions
        Z3_ast x_value, y_value;
        Z3_model_eval(ctx, model, x, true, &x_value);
        Z3_model_eval(ctx, model, y, true, &y_value);
        
        printf("x = %s\n", Z3_ast_to_string(ctx, x_value));
        printf("y = %s\n", Z3_ast_to_string(ctx, y_value));
        
        // Print full model
        printf("\nFull model:\n%s\n", Z3_model_to_string(ctx, model));
        
        // Iterate through constants
        printf("\nConstants:\n");
        unsigned num_consts = Z3_model_get_num_consts(ctx, model);
        for (unsigned i = 0; i < num_consts; i++) {
            Z3_func_decl cnst = Z3_model_get_const_decl(ctx, model, i);
            Z3_symbol name = Z3_get_decl_name(ctx, cnst);
            Z3_ast value = Z3_model_get_const_interp(ctx, model, cnst);
            printf("  %s = %s\n",
                   Z3_get_symbol_string(ctx, name),
                   Z3_ast_to_string(ctx, value));
        }
        
        Z3_model_dec_ref(ctx, model);
    }
    
    Z3_solver_dec_ref(ctx, solver);
    Z3_del_context(ctx);
    return 0;
}

Build docs developers (and LLMs) love

Get started for freeTalk to us