Z3 |

z3_fixedpoint.h File Reference

Go to the source code of this file.

## Fixedpoint facilities
typedef void | Z3_fixedpoint_reduce_assign_callback_fptr(void *, Z3_func_decl, unsigned, Z3_ast const [], unsigned, Z3_ast const [])
| The following utilities allows adding user-defined domains. More...
typedef void | Z3_fixedpoint_reduce_app_callback_fptr(void *, Z3_func_decl, unsigned, Z3_ast const [], Z3_ast *)
typedef void(* | Z3_fixedpoint_new_lemma_eh) (void *state, Z3_ast lemma, unsigned level)
typedef void(* | Z3_fixedpoint_predecessor_eh) (void *state)
typedef void(* | Z3_fixedpoint_unfold_eh) (void *state)
Z3_fixedpoint Z3_API | Z3_mk_fixedpoint (Z3_context c)
| Create a new fixedpoint context. More...
void Z3_API | Z3_fixedpoint_inc_ref (Z3_context c, Z3_fixedpoint d)
| Increment the reference counter of the given fixedpoint context. More...
void Z3_API | Z3_fixedpoint_dec_ref (Z3_context c, Z3_fixedpoint d)
| Decrement the reference counter of the given fixedpoint context. More...
void Z3_API | Z3_fixedpoint_add_rule (Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)
| Add a universal Horn clause as a named rule. The `horn_rule` should be of the form: More...
void Z3_API | Z3_fixedpoint_add_fact (Z3_context c, Z3_fixedpoint d, Z3_func_decl r, unsigned num_args, unsigned args[])
| Add a Database fact. More...
void Z3_API | Z3_fixedpoint_assert (Z3_context c, Z3_fixedpoint d, Z3_ast axiom)
| Assert a constraint to the fixedpoint context. More...
Z3_lbool Z3_API | Z3_fixedpoint_query (Z3_context c, Z3_fixedpoint d, Z3_ast query)
| Pose a query against the asserted rules. More...
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 against the asserted rules. More...
Z3_ast Z3_API | Z3_fixedpoint_get_answer (Z3_context c, Z3_fixedpoint d)
| Retrieve a formula that encodes satisfying answers to the query. More...
Z3_string Z3_API | Z3_fixedpoint_get_reason_unknown (Z3_context c, Z3_fixedpoint d)
| Retrieve a string that describes the last status returned by Z3_fixedpoint_query. More...
void Z3_API | Z3_fixedpoint_update_rule (Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name)
| Update a named rule. A rule with the same name must have been previously created. More...
unsigned Z3_API | Z3_fixedpoint_get_num_levels (Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)
| Query the PDR engine for the maximal levels properties are known about predicate. More...
Z3_ast Z3_API | Z3_fixedpoint_get_cover_delta (Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
void Z3_API | Z3_fixedpoint_add_cover (Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
| Add property about the predicate `pred`. Add a property of predicate `pred` at `level`. It gets pushed forward when possible. More...
Z3_stats Z3_API | Z3_fixedpoint_get_statistics (Z3_context c, Z3_fixedpoint d)
| Retrieve statistics information from the last call to Z3_fixedpoint_query. More...
void Z3_API | Z3_fixedpoint_register_relation (Z3_context c, Z3_fixedpoint d, Z3_func_decl f)
| Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics. For example, the relation is empty if it does not occur in a head or a fact. More...
void Z3_API | Z3_fixedpoint_set_predicate_representation (Z3_context c, Z3_fixedpoint d, Z3_func_decl f, unsigned num_relations, Z3_symbol const relation_kinds[])
| Configure the predicate representation. More...
Z3_ast_vector Z3_API | Z3_fixedpoint_get_rules (Z3_context c, Z3_fixedpoint f)
| Retrieve set of rules from fixedpoint context. More...
Z3_ast_vector Z3_API | Z3_fixedpoint_get_assertions (Z3_context c, Z3_fixedpoint f)
| Retrieve set of background assertions from fixedpoint context. More...
void Z3_API | Z3_fixedpoint_set_params (Z3_context c, Z3_fixedpoint f, Z3_params p)
| Set parameters on fixedpoint context. More...
Z3_string Z3_API | Z3_fixedpoint_get_help (Z3_context c, Z3_fixedpoint f)
| Return a string describing all fixedpoint available parameters. More...
Z3_param_descrs Z3_API | Z3_fixedpoint_get_param_descrs (Z3_context c, Z3_fixedpoint f)
| Return the parameter description set for the given fixedpoint object. More...
Z3_string Z3_API | Z3_fixedpoint_to_string (Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])
| Print the current rules and background axioms as a string. More...
Z3_ast_vector Z3_API | Z3_fixedpoint_from_string (Z3_context c, Z3_fixedpoint f, Z3_string s)
| Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the string. More...
Z3_ast_vector Z3_API | Z3_fixedpoint_from_file (Z3_context c, Z3_fixedpoint f, Z3_string s)
| Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file. More...
void Z3_API | Z3_fixedpoint_init (Z3_context c, Z3_fixedpoint d, void *state)
| Initialize the context with a user-defined state. More...
void Z3_API | Z3_fixedpoint_set_reduce_assign_callback (Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr cb)
| Register a callback to destructive updates. More...
void Z3_API | Z3_fixedpoint_set_reduce_app_callback (Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_app_callback_fptr cb)
| Register a callback for building terms based on the relational operators. More...
void Z3_API | Z3_fixedpoint_add_callback (Z3_context ctx, Z3_fixedpoint f, void *state, Z3_fixedpoint_new_lemma_eh new_lemma_eh, Z3_fixedpoint_predecessor_eh predecessor_eh, Z3_fixedpoint_unfold_eh unfold_eh)
| set export callback for lemmas More...
void Z3_API | Z3_fixedpoint_add_constraint (Z3_context c, Z3_fixedpoint d, Z3_ast e, unsigned lvl)

## Typedef Documentation

## ◆ Z3_fixedpoint_new_lemma_eh

typedef void(* Z3_fixedpoint_new_lemma_eh) (void *state, Z3_ast lemma, unsigned level)

Definition at line 339 of file z3_fixedpoint.h.

## ◆ Z3_fixedpoint_predecessor_eh

typedef void(* Z3_fixedpoint_predecessor_eh) (void *state)

Definition at line 340 of file z3_fixedpoint.h.

## ◆ Z3_fixedpoint_reduce_app_callback_fptr

typedef void Z3_fixedpoint_reduce_app_callback_fptr(void *, Z3_func_decl, unsigned, Z3_ast const[], Z3_ast *)

Definition at line 318 of file z3_fixedpoint.h.

## ◆ Z3_fixedpoint_reduce_assign_callback_fptr

typedef void Z3_fixedpoint_reduce_assign_callback_fptr(void *, Z3_func_decl, unsigned, Z3_ast const[], unsigned, Z3_ast const[])

The following utilities allows adding user-defined domains.

Definition at line 313 of file z3_fixedpoint.h.

## ◆ Z3_fixedpoint_unfold_eh

typedef void(* Z3_fixedpoint_unfold_eh) (void *state)

Definition at line 341 of file z3_fixedpoint.h.

## Function Documentation

## ◆ Z3_fixedpoint_add_callback()

void Z3_API Z3_fixedpoint_add_callback | ( | Z3_context | ctx,
|  | Z3_fixedpoint | f,
|  | void * | state,
|  | Z3_fixedpoint_new_lemma_eh | new_lemma_eh,
|  | Z3_fixedpoint_predecessor_eh | predecessor_eh,
|  | Z3_fixedpoint_unfold_eh | unfold_eh
| ) |  |

set export callback for lemmas

## ◆ Z3_fixedpoint_add_constraint()

void Z3_API Z3_fixedpoint_add_constraint | ( | Z3_context | c,
|  | Z3_fixedpoint | d,
|  | Z3_ast | e,
|  | unsigned | lvl
| ) |  |

## ◆ 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 property about the predicate `pred`. Add a property of predicate `pred` at `level`. It gets pushed forward when possible.

Note: level = -1 is treated as the fixedpoint. So passing -1 for the `level` means that the property is true of the fixed-point unfolding with respect to `pred`.

Note: this functionality is PDR specific.

Referenced by fixedpoint::add_cover(), and Fixedpoint::add_cover().

## ◆ 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 Database fact.

Parameters

  c | - context
  d | - fixed point context
  r | - relation signature for the row.
  num_args | - number of columns for the given row.
  args | - array of the row elements.

The number of arguments `num_args` should be equal to the number of sorts in the domain of `r`. Each sort in the domain should be an integral (bit-vector, Boolean or or finite domain sort).

The call has the same effect as adding a rule where `r` is applied to the arguments.

Referenced by fixedpoint::add_fact().

## ◆ 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 universal Horn clause as a named rule. The `horn_rule` should be of the form:

horn_rule ::= (forall (bound-vars) horn_rule)
| (=> atoms horn_rule)
| atom
z3::forall
expr forall(expr const &x, expr const &b)
Definition: z3++.h:2189

Referenced by fixedpoint::add_rule(), and Fixedpoint::add_rule().

## ◆ Z3_fixedpoint_assert()

void Z3_API Z3_fixedpoint_assert | ( | Z3_context | c,
|  | Z3_fixedpoint | d,
|  | Z3_ast | axiom
| ) |  |

Assert a constraint to the fixedpoint context.

The constraints are used as background axioms when the fixedpoint engine uses the PDR mode. They are ignored for standard Datalog mode.

Referenced by Fixedpoint::assert_exprs().

## ◆ Z3_fixedpoint_dec_ref()

void Z3_API Z3_fixedpoint_dec_ref | ( | Z3_context | c,
|  | Z3_fixedpoint | d
| ) |  |

Decrement the reference counter of the given fixedpoint context.

Referenced by Fixedpoint::__del__(), fixedpoint::operator=(), and fixedpoint::~fixedpoint().

## ◆ Z3_fixedpoint_from_file()

Z3_ast_vector Z3_API Z3_fixedpoint_from_file | ( | Z3_context | c,
|  | Z3_fixedpoint | f,
|  | Z3_string | s
| ) |  |

Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file.

Parameters

  c | - context.
  f | - fixedpoint context.
  s | - path to file containing SMT2 specification.

See also
  Z3_fixedpoint_from_string
  Z3_fixedpoint_to_string

Referenced by fixedpoint::from_file(), and Fixedpoint::parse_file().

## ◆ Z3_fixedpoint_from_string()

Z3_ast_vector Z3_API Z3_fixedpoint_from_string | ( | Z3_context | c,
|  | Z3_fixedpoint | f,
|  | Z3_string | s
| ) |  |

Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the string.

Parameters

  c | - context.
  f | - fixedpoint context.
  s | - string containing SMT2 specification.

See also
  Z3_fixedpoint_from_file
  Z3_fixedpoint_to_string

Referenced by fixedpoint::from_string(), and Fixedpoint::parse_string().

## ◆ Z3_fixedpoint_get_answer()

Z3_ast Z3_API Z3_fixedpoint_get_answer | ( | Z3_context | c,
|  | Z3_fixedpoint | d
| ) |  |

Retrieve a formula that encodes satisfying answers to the query.

When used in Datalog mode, the returned answer is a disjunction of conjuncts. Each conjunct encodes values of the bound variables of the query that are satisfied. In PDR mode, the returned answer is a single conjunction.

When used in Datalog mode the previous call to Z3_fixedpoint_query must have returned `Z3_L_TRUE`. When used with the PDR engine, the previous call must have been either `Z3_L_TRUE` or `Z3_L_FALSE`.

Referenced by fixedpoint::get_answer(), and Fixedpoint::get_answer().

## ◆ Z3_fixedpoint_get_assertions()

Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions | ( | Z3_context | c,
|  | Z3_fixedpoint | f
| ) |  |

Retrieve set of background assertions from fixedpoint context.

Referenced by fixedpoint::assertions(), and Fixedpoint::get_assertions().

## ◆ 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 current cover of `pred` up to `level` unfoldings. Return just the delta that is known at `level`. To obtain the full set of properties of `pred` one should query at `level+1` , `level+2` etc, and include `level=-1`.

Note: this functionality is PDR specific.

Referenced by fixedpoint::get_cover_delta(), and Fixedpoint::get_cover_delta().

## ◆ Z3_fixedpoint_get_help()

Z3_string Z3_API Z3_fixedpoint_get_help | ( | Z3_context | c,
|  | Z3_fixedpoint | f
| ) |  |

Return a string describing all fixedpoint available parameters.

See also
  Z3_fixedpoint_get_param_descrs
  Z3_fixedpoint_set_params

Referenced by fixedpoint::help(), and Fixedpoint::help().

## ◆ Z3_fixedpoint_get_num_levels()

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

Query the PDR engine for the maximal levels properties are known about predicate.

This call retrieves the maximal number of relevant unfoldings of `pred` with respect to the current exploration state. Note: this functionality is PDR specific.

Referenced by fixedpoint::get_num_levels(), and Fixedpoint::get_num_levels().

## ◆ Z3_fixedpoint_get_param_descrs()

Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs | ( | Z3_context | c,
|  | Z3_fixedpoint | f
| ) |  |

Return the parameter description set for the given fixedpoint object.

See also
  Z3_fixedpoint_get_help
  Z3_fixedpoint_set_params

Referenced by fixedpoint::get_param_descrs(), and Fixedpoint::param_descrs().

## ◆ Z3_fixedpoint_get_reason_unknown()

Z3_string Z3_API Z3_fixedpoint_get_reason_unknown | ( | Z3_context | c,
|  | Z3_fixedpoint | d
| ) |  |

Retrieve a string that describes the last status returned by Z3_fixedpoint_query.

Use this method when Z3_fixedpoint_query returns `Z3_L_UNDEF`.

Referenced by fixedpoint::reason_unknown(), and Fixedpoint::reason_unknown().

## ◆ Z3_fixedpoint_get_rules()

Z3_ast_vector Z3_API Z3_fixedpoint_get_rules | ( | Z3_context | c,
|  | Z3_fixedpoint | f
| ) |  |

Retrieve set of rules from fixedpoint context.

Referenced by Fixedpoint::get_rules(), and fixedpoint::rules().

## ◆ Z3_fixedpoint_get_statistics()

Z3_stats Z3_API Z3_fixedpoint_get_statistics | ( | Z3_context | c,
|  | Z3_fixedpoint | d
| ) |  |

Retrieve statistics information from the last call to Z3_fixedpoint_query.

Referenced by fixedpoint::statistics(), and Fixedpoint::statistics().

## ◆ Z3_fixedpoint_inc_ref()

void Z3_API Z3_fixedpoint_inc_ref | ( | Z3_context | c,
|  | Z3_fixedpoint | d
| ) |  |

Increment the reference counter of the given fixedpoint context.

Referenced by fixedpoint::fixedpoint(), and fixedpoint::operator=().

## ◆ Z3_fixedpoint_init()

void Z3_API Z3_fixedpoint_init | ( | Z3_context | c,
|  | Z3_fixedpoint | d,
|  | void * | state
| ) |  |

Initialize the context with a user-defined state.

## ◆ Z3_fixedpoint_query()

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

Pose a query against the asserted rules.

query ::= (exists (bound-vars) query)
| literals
z3::exists
expr exists(expr const &x, expr const &b)
Definition: z3++.h:2213

query returns

- `Z3_L_FALSE` if the query is unsatisfiable.
- `Z3_L_TRUE` if the query is satisfiable. Obtain the answer by calling Z3_fixedpoint_get_answer.
- `Z3_L_UNDEF` if the query was interrupted, timed out or otherwise failed.

Referenced by fixedpoint::query(), and Fixedpoint::query().

## ◆ 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 against the asserted rules.

The queries are encoded as relations (function declarations).

query returns

- `Z3_L_FALSE` if the query is unsatisfiable.
- `Z3_L_TRUE` if the query is satisfiable. Obtain the answer by calling Z3_fixedpoint_get_answer.
- `Z3_L_UNDEF` if the query was interrupted, timed out or otherwise failed.

Referenced by fixedpoint::query(), and Fixedpoint::query().

## ◆ Z3_fixedpoint_register_relation()

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

Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics. For example, the relation is empty if it does not occur in a head or a fact.

Referenced by fixedpoint::register_relation(), and Fixedpoint::register_relation().

## ◆ Z3_fixedpoint_set_params()

void Z3_API Z3_fixedpoint_set_params | ( | Z3_context | c,
|  | Z3_fixedpoint | f,
|  | Z3_params | p
| ) |  |

Set parameters on fixedpoint context.

See also
  Z3_fixedpoint_get_help
  Z3_fixedpoint_get_param_descrs

Referenced by fixedpoint::set(), and Fixedpoint::set().

## ◆ Z3_fixedpoint_set_predicate_representation()

void Z3_API Z3_fixedpoint_set_predicate_representation | ( | Z3_context | c,
|  | Z3_fixedpoint | d,
|  | Z3_func_decl | f,
|  | unsigned | num_relations,
|  | Z3_symbol const | relation_kinds[]
| ) |  |

Configure the predicate representation.

It sets the predicate to use a set of domains given by the list of symbols. The domains given by the list of symbols must belong to a set of built-in domains.

Referenced by Fixedpoint::set_predicate_representation().

## ◆ Z3_fixedpoint_set_reduce_app_callback()

void Z3_API Z3_fixedpoint_set_reduce_app_callback | ( | Z3_context | c,
|  | Z3_fixedpoint | d,
|  | Z3_fixedpoint_reduce_app_callback_fptr | cb
| ) |  |

Register a callback for building terms based on the relational operators.

## ◆ Z3_fixedpoint_set_reduce_assign_callback()

void Z3_API Z3_fixedpoint_set_reduce_assign_callback | ( | Z3_context | c,
|  | Z3_fixedpoint | d,
|  | Z3_fixedpoint_reduce_assign_callback_fptr | cb
| ) |  |

Register a callback to destructive updates.

Registers are identified with terms encoded as fresh constants,

## ◆ Z3_fixedpoint_to_string()

Z3_string Z3_API Z3_fixedpoint_to_string | ( | Z3_context | c,
|  | Z3_fixedpoint | f,
|  | unsigned | num_queries,
|  | Z3_ast | queries[]
| ) |  |

Print the current rules and background axioms as a string.

Parameters

  c | - context.
  f | - fixedpoint context.
  num_queries | - number of additional queries to print.
  queries | - additional queries.

See also
  Z3_fixedpoint_from_file
  Z3_fixedpoint_from_string

Referenced by z3::operator<<(), Fixedpoint::sexpr(), fixedpoint::to_string(), and Fixedpoint::to_string().

## ◆ Z3_fixedpoint_update_rule()

void Z3_API Z3_fixedpoint_update_rule | ( | Z3_context | c,
|  | Z3_fixedpoint | d,
|  | Z3_ast | a,
|  | Z3_symbol | name
| ) |  |

Update a named rule. A rule with the same name must have been previously created.

Referenced by fixedpoint::update_rule(), and Fixedpoint::update_rule().

## ◆ Z3_mk_fixedpoint()

Z3_fixedpoint Z3_API Z3_mk_fixedpoint | ( | Z3_context | c | ) |

Create a new fixedpoint context.

Remarks
  User must use Z3_fixedpoint_inc_ref and Z3_fixedpoint_dec_ref to manage fixedpoint objects. Even if the context was created using Z3_mk_context instead of Z3_mk_context_rc.

Referenced by fixedpoint::fixedpoint().