Tactics API

Overview

The Tactics API provides a framework for building custom solvers through composable transformations. Tactics transform goals (sets of formulas) into simpler subgoals.

Types

Z3_tactic

Basic building block for creating custom solvers for specific problem domains.

Z3_probe

Function/predicate used to inspect a goal and collect information for deciding which tactic to use.

Z3_goal

Set of formulas that can be solved or transformed using tactics.

Z3_apply_result

Collection of subgoals resulting from applying a tactic to a goal.

Tactic Creation

Z3_mk_tactic

Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name);

Create a tactic by name.

Z3_tactic

Tactic object

Common Tactics:

"simplify" - Apply simplification rules
"solve-eqs" - Solve for variables
"smt" - Apply SMT solver
"qe" - Quantifier elimination
"sat" - SAT solver
"ctx-solver-simplify" - Contextual simplification
"purify-arith" - Purify arithmetic expressions
"split-clause" - Split clauses

Example:

Z3_tactic simplify = Z3_mk_tactic(ctx, "simplify");
Z3_tactic smt = Z3_mk_tactic(ctx, "smt");

Z3_tactic_inc_ref

void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t);

Increment the reference counter of a tactic.

Z3_tactic_dec_ref

void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic t);

Decrement the reference counter of a tactic.

Tactic Combinators

Z3_tactic_and_then

Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);

Create a tactic that applies t1 followed by t2.

Z3_tactic

Sequential composition tactic

Example:

Z3_tactic t = Z3_tactic_and_then(
    ctx,
    Z3_mk_tactic(ctx, "simplify"),
    Z3_mk_tactic(ctx, "solve-eqs")
);

Z3_tactic_or_else

Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2);

Create a tactic that tries t1, and if it fails, tries t2.

Z3_tactic

Or-else combinator

Z3_tactic_par_or

Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[]);

Create a tactic that applies tactics in parallel, returning the first result.

Z3_tactic

Parallel-or combinator

Z3_tactic_par_and_then

Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);

Create a tactic that applies t1 to the goal and t2 to subgoals in parallel.

Z3_tactic

Parallel composition

Z3_tactic_try_for

Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms);

Create a tactic that applies t with a time limit.

Z3_tactic

Tactic with timeout

Example:

Z3_tactic t = Z3_tactic_try_for(ctx, Z3_mk_tactic(ctx, "smt"), 5000);

Z3_tactic_repeat

Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max);

Create a tactic that repeatedly applies t until fixpoint or max iterations.

Z3_tactic

Repeat combinator

Z3_tactic_when

Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t);

Create a tactic that applies t only when probe p evaluates to true.

Z3_tactic

Conditional tactic

Z3_tactic_cond

Z3_tactic Z3_API Z3_tactic_cond(
    Z3_context c, 
    Z3_probe p, 
    Z3_tactic t1, 
    Z3_tactic t2
);

Create a tactic that applies t1 if probe p is true, otherwise t2.

Z3_tactic

If-then-else tactic

Example:

Z3_probe is_qflia = Z3_mk_probe(ctx, "is-qflia");
Z3_tactic t = Z3_tactic_cond(
    ctx,
    is_qflia,
    Z3_mk_tactic(ctx, "qflia"),
    Z3_mk_tactic(ctx, "smt")
);

Probes

Z3_mk_probe

Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name);

Create a probe by name.

Z3_probe

Probe object

Common Probes:

"is-qflia" - Linear integer arithmetic
"is-qfbv" - Bit-vectors
"is-propositional" - Pure Boolean
"num-consts" - Number of constants
"size" - Goal size
"depth" - Expression depth

Example:

Z3_probe is_propositional = Z3_mk_probe(ctx, "is-propositional");

Z3_probe_inc_ref

void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p);

Increment reference counter of a probe.

Z3_probe_dec_ref

void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p);

Decrement reference counter of a probe.

Goals

Z3_mk_goal

Z3_goal Z3_API Z3_mk_goal(
    Z3_context c,
    bool models,
    bool unsat_cores,
    bool proofs
);

Create a goal (collection of formulas).

Z3_goal

Goal object

Example:

Z3_goal goal = Z3_mk_goal(ctx, true, false, false);

Z3_goal_assert

void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a);

Add a formula to the goal.

Z3_tactic_apply

Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g);

Apply a tactic to a goal.

Z3_apply_result

Result containing subgoals

Z3_apply_result_get_num_subgoals

unsigned Z3_API Z3_apply_result_get_num_subgoals(
    Z3_context c,
    Z3_apply_result r
);

Return the number of subgoals in the result.

unsigned

Number of subgoals

Z3_apply_result_get_subgoal

Z3_goal Z3_API Z3_apply_result_get_subgoal(
    Z3_context c,
    Z3_apply_result r,
    unsigned i
);

Return the i-th subgoal.

Z3_goal

Subgoal

Complete Example

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

int main() {
    Z3_config cfg = Z3_mk_config();
    Z3_context ctx = Z3_mk_context(cfg);
    Z3_del_config(cfg);
    
    // Create goal
    Z3_goal goal = Z3_mk_goal(ctx, true, false, false);
    Z3_goal_inc_ref(ctx, goal);
    
    // Add formulas
    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);
    
    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_goal_assert(ctx, goal, Z3_mk_eq(ctx, sum, ten));
    
    // Create and apply tactic
    Z3_tactic simplify = Z3_mk_tactic(ctx, "simplify");
    Z3_tactic_inc_ref(ctx, simplify);
    
    Z3_tactic smt = Z3_mk_tactic(ctx, "smt");
    Z3_tactic_inc_ref(ctx, smt);
    
    // Compose: simplify then smt
    Z3_tactic combined = Z3_tactic_and_then(ctx, simplify, smt);
    Z3_tactic_inc_ref(ctx, combined);
    
    // Apply tactic
    Z3_apply_result result = Z3_tactic_apply(ctx, combined, goal);
    Z3_apply_result_inc_ref(ctx, result);
    
    printf("Number of subgoals: %u\n",
           Z3_apply_result_get_num_subgoals(ctx, result));
    
    // Convert to solver
    Z3_solver solver = Z3_mk_solver_from_tactic(ctx, combined);
    Z3_solver_inc_ref(ctx, solver);
    
    Z3_solver_assert(ctx, solver, Z3_mk_eq(ctx, sum, ten));
    
    if (Z3_solver_check(ctx, solver) == Z3_L_TRUE) {
        printf("Satisfiable\n");
    }
    
    // Cleanup
    Z3_solver_dec_ref(ctx, solver);
    Z3_apply_result_dec_ref(ctx, result);
    Z3_tactic_dec_ref(ctx, combined);
    Z3_tactic_dec_ref(ctx, smt);
    Z3_tactic_dec_ref(ctx, simplify);
    Z3_goal_dec_ref(ctx, goal);
    Z3_del_context(ctx);
    
    return 0;
}

Core API

Theory Solvers

Advanced

Overview

Types

Z3_tactic

Z3_probe

Z3_goal

Z3_apply_result

Tactic Creation

Z3_mk_tactic

Z3_tactic_inc_ref

Z3_tactic_dec_ref

Tactic Combinators

Z3_tactic_and_then

Z3_tactic_or_else

Z3_tactic_par_or

Z3_tactic_par_and_then

Z3_tactic_try_for

Z3_tactic_repeat

Z3_tactic_when

Z3_tactic_cond

Probes

Z3_mk_probe

Z3_probe_inc_ref

Z3_probe_dec_ref

Goals

Z3_mk_goal

Z3_goal_assert

Z3_tactic_apply

Z3_apply_result_get_num_subgoals

Z3_apply_result_get_subgoal

Complete Example

​Overview

​Types

​Z3_tactic

​Z3_probe

​Z3_goal

​Z3_apply_result

​Tactic Creation

​Z3_mk_tactic

​Z3_tactic_inc_ref

​Z3_tactic_dec_ref

​Tactic Combinators

​Z3_tactic_and_then

​Z3_tactic_or_else

​Z3_tactic_par_or

​Z3_tactic_par_and_then

​Z3_tactic_try_for

​Z3_tactic_repeat

​Z3_tactic_when

​Z3_tactic_cond

​Probes

​Z3_mk_probe

​Z3_probe_inc_ref

​Z3_probe_dec_ref

​Goals

​Z3_mk_goal

​Z3_goal_assert

​Z3_tactic_apply

​Z3_apply_result_get_num_subgoals

​Z3_apply_result_get_subgoal

​Complete Example

Overview

Types

Z3_tactic

Z3_probe

Z3_goal

Z3_apply_result

Tactic Creation

Z3_mk_tactic

Z3_tactic_inc_ref

Z3_tactic_dec_ref

Tactic Combinators

Z3_tactic_and_then

Z3_tactic_or_else

Z3_tactic_par_or

Z3_tactic_par_and_then

Z3_tactic_try_for

Z3_tactic_repeat

Z3_tactic_when

Z3_tactic_cond

Probes

Z3_mk_probe

Z3_probe_inc_ref

Z3_probe_dec_ref

Goals

Z3_mk_goal

Z3_goal_assert

Z3_tactic_apply

Z3_apply_result_get_num_subgoals

Z3_apply_result_get_subgoal

Complete Example