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 340 of file z3_fixedpoint.h.

◆ Z3_fixedpoint_predecessor_eh

typedef void(* Z3_fixedpoint_predecessor_eh) (void *state)

Definition at line 341 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 319 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 314 of file z3_fixedpoint.h.

◆ Z3_fixedpoint_unfold_eh

typedef void(* Z3_fixedpoint_unfold_eh) (void *state)

Definition at line 342 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
expr forall(expr const &x, expr const &b)
Definition: z3++.h:1935

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__(), 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().

◆ 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
expr exists(expr const &x, expr const &b)
Definition: z3++.h:1959

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().