Skip to main content

​
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.
​
return
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
);
Register a relation (predicate) for use in rules. Example: 
// 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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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.
​
return
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;
}

Build docs developers (and LLMs) love

Get started for freeTalk to us