Statistics

Overview

Z3 provides detailed statistics about solver execution, including conflict counts, decision counts, memory usage, and theory-specific metrics. These statistics are essential for performance analysis, debugging, and optimization.

Collecting Statistics

Basic Statistics Retrieval

Z3_solver solver = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, solver);

// Add constraints and check satisfiability
Z3_solver_assert(ctx, solver, formula);
Z3_lbool result = Z3_solver_check(ctx, solver);

// Get statistics after solving
Z3_stats stats = Z3_solver_get_statistics(ctx, solver);
Z3_stats_inc_ref(ctx, stats);

// Use statistics...

Z3_stats_dec_ref(ctx, stats);
Z3_solver_dec_ref(ctx, solver);

Reading Statistics

Iterating Through All Statistics

Z3_stats stats = Z3_solver_get_statistics(ctx, solver);
Z3_stats_inc_ref(ctx, stats);

unsigned size = Z3_stats_size(ctx, stats);
printf("Statistics count: %u\n", size);

for (unsigned i = 0; i < size; i++) {
    Z3_string key = Z3_stats_get_key(ctx, stats, i);
    
    if (Z3_stats_is_uint(ctx, stats, i)) {
        unsigned value = Z3_stats_get_uint_value(ctx, stats, i);
        printf("  %s: %u\n", key, value);
    } else if (Z3_stats_is_double(ctx, stats, i)) {
        double value = Z3_stats_get_double_value(ctx, stats, i);
        printf("  %s: %.2f\n", key, value);
    }
}

Z3_stats_dec_ref(ctx, stats);

Formatted Statistics Output

Z3_stats stats = Z3_solver_get_statistics(ctx, solver);
Z3_stats_inc_ref(ctx, stats);

// Convert to SMT2 format string
Z3_string stats_str = Z3_stats_to_string(ctx, stats);
printf("Statistics:\n%s\n", stats_str);

Z3_stats_dec_ref(ctx, stats);

Example output:

(:max-memory   12.34
 :memory       10.50
 :num-allocs   1234567
 :rlimit-count 543210
 :time         2.45
 :mk-bool-var  128
 :conflicts    4567
 :decisions    8901)

Key Statistics Categories

Core Solver Statistics

// Helper function to get a specific statistic
unsigned get_stat_uint(Z3_context ctx, Z3_stats stats, const char* key_name) {
    unsigned size = Z3_stats_size(ctx, stats);
    for (unsigned i = 0; i < size; i++) {
        Z3_string key = Z3_stats_get_key(ctx, stats, i);
        if (strcmp(key, key_name) == 0 && Z3_stats_is_uint(ctx, stats, i)) {
            return Z3_stats_get_uint_value(ctx, stats, i);
        }
    }
    return 0;
}

double get_stat_double(Z3_context ctx, Z3_stats stats, const char* key_name) {
    unsigned size = Z3_stats_size(ctx, stats);
    for (unsigned i = 0; i < size; i++) {
        Z3_string key = Z3_stats_get_key(ctx, stats, i);
        if (strcmp(key, key_name) == 0 && Z3_stats_is_double(ctx, stats, i)) {
            return Z3_stats_get_double_value(ctx, stats, i);
        }
    }
    return 0.0;
}

// Get key solver statistics
Z3_stats stats = Z3_solver_get_statistics(ctx, solver);
Z3_stats_inc_ref(ctx, stats);

unsigned conflicts = get_stat_uint(ctx, stats, "conflicts");
unsigned decisions = get_stat_uint(ctx, stats, "decisions");
unsigned propagations = get_stat_uint(ctx, stats, "propagations");
double time = get_stat_double(ctx, stats, "time");

printf("Conflicts: %u\n", conflicts);
printf("Decisions: %u\n", decisions);
printf("Propagations: %u\n", propagations);
printf("Time: %.3f seconds\n", time);

Z3_stats_dec_ref(ctx, stats);

Memory Statistics

Z3_stats stats = Z3_solver_get_statistics(ctx, solver);
Z3_stats_inc_ref(ctx, stats);

double memory_mb = get_stat_double(ctx, stats, "memory");
double max_memory_mb = get_stat_double(ctx, stats, "max-memory");
unsigned num_allocs = get_stat_uint(ctx, stats, "num-allocs");

printf("Current memory: %.2f MB\n", memory_mb);
printf("Peak memory: %.2f MB\n", max_memory_mb);
printf("Allocations: %u\n", num_allocs);

Z3_stats_dec_ref(ctx, stats);

Resource Limits

Z3_stats stats = Z3_solver_get_statistics(ctx, solver);
Z3_stats_inc_ref(ctx, stats);

unsigned rlimit_count = get_stat_uint(ctx, stats, "rlimit-count");

printf("Resource limit count: %u\n", rlimit_count);

// Compare with configured limit
Z3_params params = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, params);
Z3_symbol rlimit_sym = Z3_mk_string_symbol(ctx, "rlimit");
Z3_params_set_uint(ctx, params, rlimit_sym, 1000000);
Z3_solver_set_params(ctx, solver, params);

printf("Configured limit: 1000000\n");
printf("Used: %u (%.1f%%)\n", rlimit_count, (rlimit_count / 1000000.0) * 100);

Z3_params_dec_ref(ctx, params);
Z3_stats_dec_ref(ctx, stats);

Theory-Specific Statistics

SAT Solver Statistics

Z3_stats stats = Z3_solver_get_statistics(ctx, solver);
Z3_stats_inc_ref(ctx, stats);

// SAT-specific metrics
unsigned mk_bool_var = get_stat_uint(ctx, stats, "mk-bool-var");
unsigned conflicts = get_stat_uint(ctx, stats, "conflicts");
unsigned decisions = get_stat_uint(ctx, stats, "decisions");
unsigned restarts = get_stat_uint(ctx, stats, "restarts");
unsigned minimized_lits = get_stat_uint(ctx, stats, "minimized-lits");

printf("Boolean variables: %u\n", mk_bool_var);
printf("Conflicts: %u\n", conflicts);
printf("Decisions: %u\n", decisions);
printf("Restarts: %u\n", restarts);
printf("Minimized literals: %u\n", minimized_lits);

Z3_stats_dec_ref(ctx, stats);

Arithmetic Theory Statistics

Z3_stats stats = Z3_solver_get_statistics(ctx, solver);
Z3_stats_inc_ref(ctx, stats);

// Arithmetic-specific metrics
unsigned arith_conflicts = get_stat_uint(ctx, stats, "arith-conflicts");
unsigned arith_bound_prop = get_stat_uint(ctx, stats, "arith-bound-propagations");
unsigned arith_fixed = get_stat_uint(ctx, stats, "arith-fixed");

printf("Arithmetic conflicts: %u\n", arith_conflicts);
printf("Bound propagations: %u\n", arith_bound_prop);
printf("Fixed variables: %u\n", arith_fixed);

Z3_stats_dec_ref(ctx, stats);

Array Theory Statistics

Z3_stats stats = Z3_solver_get_statistics(ctx, solver);
Z3_stats_inc_ref(ctx, stats);

// Array-specific metrics
unsigned array_axiom1 = get_stat_uint(ctx, stats, "array-axiom1");
unsigned array_axiom2 = get_stat_uint(ctx, stats, "array-axiom2");
unsigned array_extensionality = get_stat_uint(ctx, stats, "array-extensionality");

printf("Array select-store axioms: %u\n", array_axiom1);
printf("Array congruence axioms: %u\n", array_axiom2);
printf("Array extensionality: %u\n", array_extensionality);

Z3_stats_dec_ref(ctx, stats);

Performance Analysis

Identifying Bottlenecks

typedef struct {
    double time;
    unsigned conflicts;
    unsigned decisions;
    unsigned restarts;
    double memory;
} solver_profile;

solver_profile get_profile(Z3_context ctx, Z3_stats stats) {
    solver_profile profile;
    profile.time = get_stat_double(ctx, stats, "time");
    profile.conflicts = get_stat_uint(ctx, stats, "conflicts");
    profile.decisions = get_stat_uint(ctx, stats, "decisions");
    profile.restarts = get_stat_uint(ctx, stats, "restarts");
    profile.memory = get_stat_double(ctx, stats, "max-memory");
    return profile;
}

void analyze_performance(solver_profile profile) {
    printf("\nPerformance Analysis:\n");
    
    if (profile.time > 10.0) {
        printf("  WARNING: Long solving time (%.2f seconds)\n", profile.time);
    }
    
    if (profile.conflicts > 100000) {
        printf("  INFO: High conflict count (%u) - complex problem\n", 
               profile.conflicts);
    }
    
    if (profile.memory > 1000.0) {
        printf("  WARNING: High memory usage (%.2f MB)\n", profile.memory);
    }
    
    if (profile.decisions > 0 && profile.conflicts > 0) {
        double conflict_rate = (double)profile.conflicts / profile.decisions;
        printf("  Conflict rate: %.2f conflicts per decision\n", conflict_rate);
    }
    
    if (profile.restarts > 0 && profile.conflicts > 0) {
        double conflicts_per_restart = (double)profile.conflicts / profile.restarts;
        printf("  Conflicts per restart: %.2f\n", conflicts_per_restart);
    }
}

// Usage
Z3_stats stats = Z3_solver_get_statistics(ctx, solver);
Z3_stats_inc_ref(ctx, stats);

solver_profile profile = get_profile(ctx, stats);
analyze_performance(profile);

Z3_stats_dec_ref(ctx, stats);

Comparing Solver Configurations

void compare_configurations(Z3_context ctx, Z3_ast formula) {
    printf("Comparing solver configurations...\n\n");
    
    // Configuration 1: Default
    Z3_solver s1 = Z3_mk_solver(ctx);
    Z3_solver_inc_ref(ctx, s1);
    Z3_solver_assert(ctx, s1, formula);
    Z3_solver_check(ctx, s1);
    Z3_stats stats1 = Z3_solver_get_statistics(ctx, s1);
    Z3_stats_inc_ref(ctx, stats1);
    
    printf("Default configuration:\n");
    printf("  Time: %.3f\n", get_stat_double(ctx, stats1, "time"));
    printf("  Conflicts: %u\n", get_stat_uint(ctx, stats1, "conflicts"));
    
    // Configuration 2: Custom parameters
    Z3_solver s2 = Z3_mk_solver(ctx);
    Z3_solver_inc_ref(ctx, s2);
    
    Z3_params params = Z3_mk_params(ctx);
    Z3_params_inc_ref(ctx, params);
    Z3_symbol restart = Z3_mk_string_symbol(ctx, "sat.restart");
    Z3_symbol geometric = Z3_mk_string_symbol(ctx, "geometric");
    Z3_params_set_symbol(ctx, params, restart, geometric);
    Z3_solver_set_params(ctx, s2, params);
    
    Z3_solver_assert(ctx, s2, formula);
    Z3_solver_check(ctx, s2);
    Z3_stats stats2 = Z3_solver_get_statistics(ctx, s2);
    Z3_stats_inc_ref(ctx, stats2);
    
    printf("\nCustom configuration:\n");
    printf("  Time: %.3f\n", get_stat_double(ctx, stats2, "time"));
    printf("  Conflicts: %u\n", get_stat_uint(ctx, stats2, "conflicts"));
    
    // Cleanup
    Z3_stats_dec_ref(ctx, stats1);
    Z3_stats_dec_ref(ctx, stats2);
    Z3_params_dec_ref(ctx, params);
    Z3_solver_dec_ref(ctx, s1);
    Z3_solver_dec_ref(ctx, s2);
}

Global Memory Statistics

Estimated Allocation Size

// Get global memory allocation estimate
uint64_t allocated = Z3_get_estimated_alloc_size();
printf("Estimated total allocation: %llu bytes (%.2f MB)\n",
       allocated, allocated / (1024.0 * 1024.0));

This function returns an estimate of total memory allocated by Z3, useful for monitoring memory consumption across multiple solvers and contexts.

Best Practices

When to Collect Statistics

Collect statistics to:

Profile solver performance on benchmarks
Debug timeout or memory issues
Compare different solving strategies
Monitor production system health
Identify theory-specific bottlenecks

Interpreting Statistics

High conflict count: Problem is complex, consider preprocessing or simplification
Low decision count: Problem is easy or well-structured
High restart count: SAT solver is struggling, try different restart strategies
Memory growth: Problem size is large, consider incremental solving or memory limits
Long solving time with low conflicts: Theory solver may be slow, try different theory options

Statistical Logging

void log_statistics(FILE* log_file, Z3_context ctx, Z3_stats stats, 
                   const char* problem_name) {
    fprintf(log_file, "Problem: %s\n", problem_name);
    fprintf(log_file, "Time: %.3f\n", get_stat_double(ctx, stats, "time"));
    fprintf(log_file, "Memory: %.2f MB\n", get_stat_double(ctx, stats, "max-memory"));
    fprintf(log_file, "Conflicts: %u\n", get_stat_uint(ctx, stats, "conflicts"));
    fprintf(log_file, "Decisions: %u\n", get_stat_uint(ctx, stats, "decisions"));
    fprintf(log_file, "\n");
    fflush(log_file);
}

// Usage
FILE* log = fopen("solver_stats.log", "a");
Z3_stats stats = Z3_solver_get_statistics(ctx, solver);
Z3_stats_inc_ref(ctx, stats);
log_statistics(log, ctx, stats, "my_problem_001");
Z3_stats_dec_ref(ctx, stats);
fclose(log);

Common Statistics Keys

Universal Statistics

time - Total solving time in seconds
memory - Current memory usage in MB
max-memory - Peak memory usage in MB
rlimit-count - Resource limit counter
num-allocs - Number of allocations

SAT Statistics

conflicts - Number of conflicts
decisions - Number of decisions
propagations - Number of propagations
restarts - Number of restarts
mk-bool-var - Boolean variables created

Theory Statistics

arith-conflicts - Arithmetic conflicts
arith-bound-propagations - Bound propagations
array-axiom1 - Array select-store axioms
bv-conflicts - Bit-vector conflicts

API Reference

Statistics Management

Z3_solver_get_statistics - Get statistics from solver (api_solver.cpp:789)
Z3_stats_inc_ref - Increment reference counter (api_stats.cpp:39)
Z3_stats_dec_ref - Decrement reference counter (api_stats.cpp:47)
Z3_stats_to_string - Convert to string (api_stats.cpp:25)

Reading Statistics

Z3_stats_size - Get number of statistics (api_stats.cpp:56)
Z3_stats_get_key - Get statistic key name (api_stats.cpp:64)
Z3_stats_is_uint - Check if unsigned integer (api_stats.cpp:76)
Z3_stats_is_double - Check if double (api_stats.cpp:88)
Z3_stats_get_uint_value - Get unsigned value (api_stats.cpp:100)
Z3_stats_get_double_value - Get double value (api_stats.cpp:116)

Global Statistics

Z3_get_estimated_alloc_size - Get global memory estimate (api_stats.cpp:132)

Core API

Theory Solvers

Advanced

Overview

Collecting Statistics

Basic Statistics Retrieval

Reading Statistics

Iterating Through All Statistics

Formatted Statistics Output

Key Statistics Categories

Core Solver Statistics

Memory Statistics

Resource Limits

Theory-Specific Statistics

SAT Solver Statistics

Arithmetic Theory Statistics

Array Theory Statistics

Performance Analysis

Identifying Bottlenecks

Comparing Solver Configurations

Global Memory Statistics

Estimated Allocation Size

Best Practices

When to Collect Statistics

Interpreting Statistics

Statistical Logging

Common Statistics Keys

Universal Statistics

SAT Statistics

Theory Statistics

API Reference

Statistics Management

Reading Statistics

Global Statistics

See Also

​Overview

​Collecting Statistics

​Basic Statistics Retrieval

​Reading Statistics

​Iterating Through All Statistics

​Formatted Statistics Output

​Key Statistics Categories

​Core Solver Statistics

​Memory Statistics

​Resource Limits

​Theory-Specific Statistics

​SAT Solver Statistics

​Arithmetic Theory Statistics

​Array Theory Statistics

​Performance Analysis

​Identifying Bottlenecks

​Comparing Solver Configurations

​Global Memory Statistics

​Estimated Allocation Size

​Best Practices

​When to Collect Statistics

​Interpreting Statistics

​Statistical Logging

​Common Statistics Keys

​Universal Statistics

​SAT Statistics

​Theory Statistics

​API Reference

​Statistics Management

​Reading Statistics

​Global Statistics

​See Also

Overview

Collecting Statistics

Basic Statistics Retrieval

Reading Statistics

Iterating Through All Statistics

Formatted Statistics Output

Key Statistics Categories

Core Solver Statistics

Memory Statistics

Resource Limits

Theory-Specific Statistics

SAT Solver Statistics

Arithmetic Theory Statistics

Array Theory Statistics

Performance Analysis

Identifying Bottlenecks

Comparing Solver Configurations

Global Memory Statistics

Estimated Allocation Size

Best Practices

When to Collect Statistics

Interpreting Statistics

Statistical Logging

Common Statistics Keys

Universal Statistics

SAT Statistics

Theory Statistics

API Reference

Statistics Management

Reading Statistics

Global Statistics

See Also