Fixedpoint API

Overview

The Fixedpoint API provides a context for solving recursive predicate queries using Datalog-style rules. It supports Horn clauses, queries, and least fixedpoint computation.

Types

Z3_fixedpoint

Context for the recursive predicate solver. Used for Datalog queries and Horn clause solving.

Fixedpoint Creation

Z3_mk_fixedpoint

Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c);

Create a fixedpoint context.

Z3_fixedpoint

New fixedpoint instance

Example:

Z3_fixedpoint fp = Z3_mk_fixedpoint(ctx);
Z3_fixedpoint_inc_ref(ctx, fp);
// Use fixedpoint...
Z3_fixedpoint_dec_ref(ctx, fp);

Z3_fixedpoint_inc_ref

void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d);

Increment the reference counter.

Z3_fixedpoint_dec_ref

void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d);

Decrement the reference counter.

Predicate Registration

Z3_fixedpoint_register_relation

void Z3_API Z3_fixedpoint_register_relation(
    Z3_context c,
    Z3_fixedpoint d,
    Z3_func_decl f
);

// Declare predicate: edge(int, int)
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_sort domain[2] = {int_sort, int_sort};
Z3_func_decl edge = Z3_mk_func_decl(
    ctx,
    Z3_mk_string_symbol(ctx, "edge"),
    2,
    domain,
    Z3_mk_bool_sort(ctx)
);

Z3_fixedpoint_register_relation(ctx, fp, edge);

Adding Rules

Z3_fixedpoint_add_rule

void Z3_API Z3_fixedpoint_add_rule(
    Z3_context c,
    Z3_fixedpoint d,
    Z3_ast rule,
    Z3_symbol name
);

Add a Horn clause rule. Description: Rules are Horn clauses of the form:

Facts: P(args)
Rules: (implies (and body...) head)

Example:

// Fact: edge(1, 2)
Z3_ast one = Z3_mk_int(ctx, 1, int_sort);
Z3_ast two = Z3_mk_int(ctx, 2, int_sort);
Z3_ast edge_args[2] = {one, two};
Z3_ast fact = Z3_mk_app(ctx, edge, 2, edge_args);

Z3_fixedpoint_add_rule(ctx, fp, fact, Z3_mk_string_symbol(ctx, "edge_1_2"));

// Rule: path(x,y) :- edge(x,y)
Z3_sort var_sorts[2] = {int_sort, int_sort};
Z3_symbol var_names[2] = {
    Z3_mk_string_symbol(ctx, "x"),
    Z3_mk_string_symbol(ctx, "y")
};

Z3_ast x = Z3_mk_bound(ctx, 0, int_sort);
Z3_ast y = Z3_mk_bound(ctx, 1, int_sort);
Z3_ast edge_xy_args[2] = {x, y};
Z3_ast edge_xy = Z3_mk_app(ctx, edge, 2, edge_xy_args);

Z3_ast path_xy_args[2] = {x, y};
Z3_ast path_xy = Z3_mk_app(ctx, path, 2, path_xy_args);

Z3_ast rule = Z3_mk_implies(ctx, edge_xy, path_xy);
Z3_ast quantified = Z3_mk_forall_const(
    ctx, 0, 2, var_sorts, var_names, rule
);

Z3_fixedpoint_add_rule(ctx, fp, quantified, Z3_mk_string_symbol(ctx, "path_edge"));

Z3_fixedpoint_add_fact

void Z3_API Z3_fixedpoint_add_fact(
    Z3_context c,
    Z3_fixedpoint d,
    Z3_func_decl r,
    unsigned num_args,
    unsigned args[]
);

Add a fact using numeric constants. Description: Convenience function for adding ground facts with finite domain values. Example:

unsigned fact_args[2] = {1, 2};
Z3_fixedpoint_add_fact(ctx, fp, edge, 2, fact_args);

Queries

Z3_fixedpoint_query

Z3_lbool Z3_API Z3_fixedpoint_query(
    Z3_context c,
    Z3_fixedpoint d,
    Z3_ast query
);

Pose a query.

Z3_lbool

Z3_L_TRUE if derivable, Z3_L_FALSE if not derivable, Z3_L_UNDEF if unknown

Example:

// Query: path(1, 3)?
Z3_ast one = Z3_mk_int(ctx, 1, int_sort);
Z3_ast three = Z3_mk_int(ctx, 3, int_sort);
Z3_ast query_args[2] = {one, three};
Z3_ast query = Z3_mk_app(ctx, path, 2, query_args);

Z3_lbool result = Z3_fixedpoint_query(ctx, fp, query);

if (result == Z3_L_TRUE) {
    printf("Query is derivable\n");
} else if (result == Z3_L_FALSE) {
    printf("Query is not derivable\n");
} else {
    printf("Unknown\n");
}

Z3_fixedpoint_query_relations

Z3_lbool Z3_API Z3_fixedpoint_query_relations(
    Z3_context c,
    Z3_fixedpoint d,
    unsigned num_relations,
    Z3_func_decl const relations[]
);

Pose multiple queries on relations.

Z3_lbool

Satisfiability result

Results and Answers

Z3_fixedpoint_get_answer

Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d);

Retrieve the answer for the last query.

Z3_ast

Answer expression (derivation or counterexample)

Description: If the query was satisfiable, returns a derivation. If unsatisfiable, may return a certificate.

Z3_fixedpoint_get_reason_unknown

Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(
    Z3_context c,
    Z3_fixedpoint d
);

Return a string describing why the last query returned unknown.

Z3_string

Reason string

Level and Cover Management

Z3_fixedpoint_get_num_levels

unsigned Z3_API Z3_fixedpoint_get_num_levels(
    Z3_context c,
    Z3_fixedpoint d,
    Z3_func_decl pred
);

Return the number of levels in the PDR engine for a predicate.

unsigned

Number of levels

Z3_fixedpoint_get_cover_delta

Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(
    Z3_context c,
    Z3_fixedpoint d,
    int level,
    Z3_func_decl pred
);

Retrieve the cover at a given level.

Z3_ast

Cover expression

Z3_fixedpoint_add_cover

void Z3_API Z3_fixedpoint_add_cover(
    Z3_context c,
    Z3_fixedpoint d,
    int level,
    Z3_func_decl pred,
    Z3_ast property
);

Add a property to the cover at a level.

Backtracking

Z3_fixedpoint_push

void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d);

Create a backtracking point.

Z3_fixedpoint_pop

void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d);

Backtrack one level.

Information

Z3_fixedpoint_to_string

Z3_string Z3_API Z3_fixedpoint_to_string(
    Z3_context c,
    Z3_fixedpoint d,
    unsigned num_queries,
    Z3_ast queries[]
);

Convert fixedpoint state to a string.

Z3_string

String representation (Datalog format)

Z3_fixedpoint_get_rules

Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint d);

Return the set of rules.

Z3_ast_vector

Vector of rules

Z3_fixedpoint_get_assertions

Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint d);

Return the set of background assertions.

Z3_ast_vector

Vector of assertions

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);
    
    Z3_fixedpoint fp = Z3_mk_fixedpoint(ctx);
    Z3_fixedpoint_inc_ref(ctx, fp);
    
    // Declare predicates: edge(int, int), path(int, int)
    Z3_sort int_sort = Z3_mk_int_sort(ctx);
    Z3_sort domain[2] = {int_sort, int_sort};
    
    Z3_func_decl edge = Z3_mk_func_decl(
        ctx,
        Z3_mk_string_symbol(ctx, "edge"),
        2, domain, Z3_mk_bool_sort(ctx)
    );
    
    Z3_func_decl path = Z3_mk_func_decl(
        ctx,
        Z3_mk_string_symbol(ctx, "path"),
        2, domain, Z3_mk_bool_sort(ctx)
    );
    
    Z3_fixedpoint_register_relation(ctx, fp, edge);
    Z3_fixedpoint_register_relation(ctx, fp, path);
    
    // Add facts: edge(1,2), edge(2,3)
    unsigned fact1[2] = {1, 2};
    unsigned fact2[2] = {2, 3};
    Z3_fixedpoint_add_fact(ctx, fp, edge, 2, fact1);
    Z3_fixedpoint_add_fact(ctx, fp, edge, 2, fact2);
    
    // Add rules:
    // path(x,y) :- edge(x,y)
    // path(x,z) :- path(x,y), edge(y,z)
    
    Z3_sort var_sorts[3] = {int_sort, int_sort, int_sort};
    Z3_symbol var_names[3] = {
        Z3_mk_string_symbol(ctx, "x"),
        Z3_mk_string_symbol(ctx, "y"),
        Z3_mk_string_symbol(ctx, "z")
    };
    
    Z3_ast x = Z3_mk_bound(ctx, 0, int_sort);
    Z3_ast y = Z3_mk_bound(ctx, 1, int_sort);
    Z3_ast z = Z3_mk_bound(ctx, 2, int_sort);
    
    // Rule 1: path(x,y) :- edge(x,y)
    Z3_ast edge_xy_args[2] = {x, y};
    Z3_ast edge_xy = Z3_mk_app(ctx, edge, 2, edge_xy_args);
    Z3_ast path_xy_args[2] = {x, y};
    Z3_ast path_xy = Z3_mk_app(ctx, path, 2, path_xy_args);
    Z3_ast rule1 = Z3_mk_implies(ctx, edge_xy, path_xy);
    
    // Rule 2: path(x,z) :- path(x,y) and edge(y,z)
    Z3_ast edge_yz_args[2] = {y, z};
    Z3_ast edge_yz = Z3_mk_app(ctx, edge, 2, edge_yz_args);
    Z3_ast path_xz_args[2] = {x, z};
    Z3_ast path_xz = Z3_mk_app(ctx, path, 2, path_xz_args);
    Z3_ast body_args[2] = {path_xy, edge_yz};
    Z3_ast body = Z3_mk_and(ctx, 2, body_args);
    Z3_ast rule2 = Z3_mk_implies(ctx, body, path_xz);
    
    Z3_fixedpoint_add_rule(ctx, fp, rule1, 0);
    Z3_fixedpoint_add_rule(ctx, fp, rule2, 0);
    
    // Query: path(1, 3)?
    Z3_ast one = Z3_mk_int(ctx, 1, int_sort);
    Z3_ast three = Z3_mk_int(ctx, 3, int_sort);
    Z3_ast query_args[2] = {one, three};
    Z3_ast query = Z3_mk_app(ctx, path, 2, query_args);
    
    Z3_lbool result = Z3_fixedpoint_query(ctx, fp, query);
    
    if (result == Z3_L_TRUE) {
        printf("Path(1,3) is derivable\n");
        Z3_ast answer = Z3_fixedpoint_get_answer(ctx, fp);
        printf("Derivation: %s\n", Z3_ast_to_string(ctx, answer));
    } else {
        printf("Path(1,3) is not derivable\n");
    }
    
    Z3_fixedpoint_dec_ref(ctx, fp);
    Z3_del_context(ctx);
    return 0;
}

Core API

Theory Solvers

Advanced

Overview

Types

Z3_fixedpoint

Fixedpoint Creation

Z3_mk_fixedpoint

Z3_fixedpoint_inc_ref

Z3_fixedpoint_dec_ref

Predicate Registration

Z3_fixedpoint_register_relation

Adding Rules

Z3_fixedpoint_add_rule

Z3_fixedpoint_add_fact

Queries

Z3_fixedpoint_query

Z3_fixedpoint_query_relations

Results and Answers

Z3_fixedpoint_get_answer

Z3_fixedpoint_get_reason_unknown

Level and Cover Management

Z3_fixedpoint_get_num_levels

Z3_fixedpoint_get_cover_delta

Z3_fixedpoint_add_cover

Backtracking

Z3_fixedpoint_push

Z3_fixedpoint_pop

Information

Z3_fixedpoint_to_string

Z3_fixedpoint_get_rules

Z3_fixedpoint_get_assertions

Complete Example

​Overview

​Types

​Z3_fixedpoint

​Fixedpoint Creation

​Z3_mk_fixedpoint

​Z3_fixedpoint_inc_ref

​Z3_fixedpoint_dec_ref

​Predicate Registration

​Z3_fixedpoint_register_relation

​Adding Rules

​Z3_fixedpoint_add_rule

​Z3_fixedpoint_add_fact

​Queries

​Z3_fixedpoint_query

​Z3_fixedpoint_query_relations

​Results and Answers

​Z3_fixedpoint_get_answer

​Z3_fixedpoint_get_reason_unknown

​Level and Cover Management

​Z3_fixedpoint_get_num_levels

​Z3_fixedpoint_get_cover_delta

​Z3_fixedpoint_add_cover

​Backtracking

​Z3_fixedpoint_push

​Z3_fixedpoint_pop

​Information

​Z3_fixedpoint_to_string

​Z3_fixedpoint_get_rules

​Z3_fixedpoint_get_assertions

​Complete Example

Overview

Types

Z3_fixedpoint

Fixedpoint Creation

Z3_mk_fixedpoint

Z3_fixedpoint_inc_ref

Z3_fixedpoint_dec_ref

Predicate Registration

Z3_fixedpoint_register_relation

Adding Rules

Z3_fixedpoint_add_rule

Z3_fixedpoint_add_fact

Queries

Z3_fixedpoint_query

Z3_fixedpoint_query_relations

Results and Answers

Z3_fixedpoint_get_answer

Z3_fixedpoint_get_reason_unknown

Level and Cover Management

Z3_fixedpoint_get_num_levels

Z3_fixedpoint_get_cover_delta

Z3_fixedpoint_add_cover

Backtracking

Z3_fixedpoint_push

Z3_fixedpoint_pop

Information

Z3_fixedpoint_to_string

Z3_fixedpoint_get_rules

Z3_fixedpoint_get_assertions

Complete Example