Solver API

Overview

The Solver API provides an incremental interface for solving satisfiability problems. Solvers support assertions, backtracking (push/pop), and extracting models and unsat cores.

Types

Z3_solver

Incremental solver object that can be specialized by tactics or logics.

Solver Creation

Z3_mk_solver

Z3_solver Z3_API Z3_mk_solver(Z3_context c);

Create a general-purpose solver.

Z3_solver

New solver instance

Description: Creates a solver using the default SMT solver with strategic preprocessing. Example:

Z3_solver solver = Z3_mk_solver(ctx);
// Use solver...
Z3_solver_dec_ref(ctx, solver);

Z3_mk_simple_solver

Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c);

Create a simple solver without strategic preprocessing.

Z3_solver

New simple solver instance

Description: Faster startup but may be less efficient on complex problems.

Z3_mk_solver_for_logic

Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic);

Create a solver optimized for a specific logic.

Z3_solver

New solver instance

Example:

Z3_solver solver = Z3_mk_solver_for_logic(
    ctx, 
    Z3_mk_string_symbol(ctx, "QF_LIA")
);

Z3_mk_solver_from_tactic

Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);

Create a solver from a tactic.

Z3_solver

Solver based on tactic

Reference Counting

Z3_solver_inc_ref

void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s);

Increment the reference counter of the solver.

Z3_solver_dec_ref

void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s);

Decrement the reference counter of the solver.

Assertions

Z3_solver_assert

void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a);

Assert a constraint into the solver. Example:

Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), Z3_mk_int_sort(ctx));
Z3_ast zero = Z3_mk_int(ctx, 0, Z3_mk_int_sort(ctx));
Z3_ast constraint = Z3_mk_gt(ctx, x, zero);
Z3_solver_assert(ctx, solver, constraint); // assert x > 0

Z3_solver_assert_and_track

void Z3_API Z3_solver_assert_and_track(
    Z3_context c, 
    Z3_solver s, 
    Z3_ast a, 
    Z3_ast p
);

Assert a constraint with a tracking literal. Description: The tracking literal allows identification of assertions in unsat cores. Example:

Z3_ast track1 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "t1"), Z3_mk_bool_sort(ctx));
Z3_solver_assert_and_track(ctx, solver, constraint1, track1);

Satisfiability Checking

Z3_solver_check

Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s);

Check if the current set of assertions is satisfiable.

Z3_lbool

Z3_L_TRUE if satisfiable, Z3_L_FALSE if unsatisfiable, Z3_L_UNDEF if unknown

Example:

Z3_lbool result = Z3_solver_check(ctx, solver);

if (result == Z3_L_TRUE) {
    printf("Satisfiable\n");
    Z3_model model = Z3_solver_get_model(ctx, solver);
    // Use model...
    Z3_model_dec_ref(ctx, model);
} else if (result == Z3_L_FALSE) {
    printf("Unsatisfiable\n");
} else {
    printf("Unknown\n");
}

Z3_solver_check_assumptions

Z3_lbool Z3_API Z3_solver_check_assumptions(
    Z3_context c, 
    Z3_solver s,
    unsigned num_assumptions, 
    Z3_ast const assumptions[]
);

Check satisfiability under given assumptions.

Z3_lbool

Satisfiability result

Description: Assumptions are temporary constraints only active for this check call. Example:

Z3_ast assumptions[2] = {p, q};
Z3_lbool result = Z3_solver_check_assumptions(ctx, solver, 2, assumptions);

Models

Z3_solver_get_model

Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s);

Retrieve the model for the last check (if satisfiable).

Z3_model

Model object (must increment reference)

Note: Model must be kept alive with Z3_model_inc_ref.

Unsat Cores

Z3_solver_get_unsat_core

Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s);

Retrieve the unsat core from the last check (if unsatisfiable).

Z3_ast_vector

Subset of asserted constraints that are unsatisfiable

Requirements:

Context must be created with unsat_core enabled
Assertions must be tracked using Z3_solver_assert_and_track

Example:

Z3_config cfg = Z3_mk_config();
Z3_set_param_value(cfg, "unsat_core", "true");
Z3_context ctx = Z3_mk_context(cfg);

Z3_solver solver = Z3_mk_solver(ctx);

Z3_ast t1 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "t1"), Z3_mk_bool_sort(ctx));
Z3_ast t2 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "t2"), Z3_mk_bool_sort(ctx));

Z3_solver_assert_and_track(ctx, solver, constraint1, t1);
Z3_solver_assert_and_track(ctx, solver, constraint2, t2);

if (Z3_solver_check(ctx, solver) == Z3_L_FALSE) {
    Z3_ast_vector core = Z3_solver_get_unsat_core(ctx, solver);
    // Examine core...
    Z3_ast_vector_dec_ref(ctx, core);
}

Backtracking

Z3_solver_push

void Z3_API Z3_solver_push(Z3_context c, Z3_solver s);

Create a backtracking point. Description: Saves the current state. Assertions added after push can be removed with pop.

Z3_solver_pop

void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n);

Backtrack n backtracking points. Example:

Z3_solver_push(ctx, solver);
Z3_solver_assert(ctx, solver, constraint1);
Z3_solver_check(ctx, solver); // Check with constraint1

Z3_solver_push(ctx, solver);
Z3_solver_assert(ctx, solver, constraint2);
Z3_solver_check(ctx, solver); // Check with constraint1 and constraint2

Z3_solver_pop(ctx, solver, 1); // Remove constraint2
Z3_solver_check(ctx, solver); // Check with only constraint1

Z3_solver_pop(ctx, solver, 1); // Remove constraint1

Z3_solver_reset

void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s);

Remove all assertions from the solver.

Solver Information

Z3_solver_get_num_scopes

unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s);

Return the number of backtracking points.

unsigned

Number of scopes

Z3_solver_get_assertions

Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s);

Return the set of asserted formulas.

Z3_ast_vector

Vector of assertions

Z3_solver_get_reason_unknown

Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s);

Return a string describing why the last check returned unknown.

Z3_string

Reason string

Z3_solver_to_string

Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s);

Convert solver state to a string (SMT-LIB format).

Z3_string

String representation

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);
    
    // Create constraints: x + y = 10, x > 0
    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 zero = Z3_mk_int(ctx, 0, int_sort);
    
    Z3_solver_assert(ctx, solver, Z3_mk_eq(ctx, sum, ten));
    Z3_solver_assert(ctx, solver, Z3_mk_gt(ctx, x, zero));
    
    // Check satisfiability
    Z3_lbool result = Z3_solver_check(ctx, solver);
    
    if (result == Z3_L_TRUE) {
        printf("Satisfiable\n");
        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);
    } else if (result == Z3_L_FALSE) {
        printf("Unsatisfiable\n");
    } else {
        printf("Unknown\n");
    }
    
    Z3_solver_dec_ref(ctx, solver);
    Z3_del_context(ctx);
    return 0;
}

Core API

Theory Solvers

Advanced

Overview

Types

Z3_solver

Solver Creation

Z3_mk_solver

Z3_mk_simple_solver

Z3_mk_solver_for_logic

Z3_mk_solver_from_tactic

Reference Counting

Z3_solver_inc_ref

Z3_solver_dec_ref

Assertions

Z3_solver_assert

Z3_solver_assert_and_track

Satisfiability Checking

Z3_solver_check

Z3_solver_check_assumptions

Models

Z3_solver_get_model

Unsat Cores

Z3_solver_get_unsat_core

Backtracking

Z3_solver_push

Z3_solver_pop

Z3_solver_reset

Solver Information

Z3_solver_get_num_scopes

Z3_solver_get_assertions

Z3_solver_get_reason_unknown

Z3_solver_to_string

Complete Example

​Overview

​Types

​Z3_solver

​Solver Creation

​Z3_mk_solver

​Z3_mk_simple_solver

​Z3_mk_solver_for_logic

​Z3_mk_solver_from_tactic

​Reference Counting

​Z3_solver_inc_ref

​Z3_solver_dec_ref

​Assertions

​Z3_solver_assert

​Z3_solver_assert_and_track

​Satisfiability Checking

​Z3_solver_check

​Z3_solver_check_assumptions

​Models

​Z3_solver_get_model

​Unsat Cores

​Z3_solver_get_unsat_core

​Backtracking

​Z3_solver_push

​Z3_solver_pop

​Z3_solver_reset

​Solver Information

​Z3_solver_get_num_scopes

​Z3_solver_get_assertions

​Z3_solver_get_reason_unknown

​Z3_solver_to_string

​Complete Example

Overview

Types

Z3_solver

Solver Creation

Z3_mk_solver

Z3_mk_simple_solver

Z3_mk_solver_for_logic

Z3_mk_solver_from_tactic

Reference Counting

Z3_solver_inc_ref

Z3_solver_dec_ref

Assertions

Z3_solver_assert

Z3_solver_assert_and_track

Satisfiability Checking

Z3_solver_check

Z3_solver_check_assumptions

Models

Z3_solver_get_model

Unsat Cores

Z3_solver_get_unsat_core

Backtracking

Z3_solver_push

Z3_solver_pop

Z3_solver_reset

Solver Information

Z3_solver_get_num_scopes

Z3_solver_get_assertions

Z3_solver_get_reason_unknown

Z3_solver_to_string

Complete Example