Skip to main content

​
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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).
​
return
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.
​
return
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.
​
return
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.
​
return
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;
}

Build docs developers (and LLMs) love

Get started for freeTalk to us