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 void(* Z3_fixedpoint_new_lemma_eh) (void *state, Z3_ast lemma, unsigned level) |
Definition at line 340 of file z3_fixedpoint.h.
typedef void(* Z3_fixedpoint_predecessor_eh) (void *state) |
Definition at line 341 of file z3_fixedpoint.h.
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.
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.
typedef void(* Z3_fixedpoint_unfold_eh) (void *state) |
Definition at line 342 of file z3_fixedpoint.h.
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
void Z3_API Z3_fixedpoint_add_constraint | ( | Z3_context | c, |
Z3_fixedpoint | d, | ||
Z3_ast | e, | ||
unsigned | lvl | ||
) |
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().
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.
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().
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:
Referenced by fixedpoint::add_rule(), and Fixedpoint::add_rule().
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().
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_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.
c | - context. |
f | - fixedpoint context. |
s | - path to file containing SMT2 specification. |
Referenced by fixedpoint::from_file(), and Fixedpoint::parse_file().
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.
c | - context. |
f | - fixedpoint context. |
s | - string containing SMT2 specification. |
Referenced by fixedpoint::from_string(), and Fixedpoint::parse_string().
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_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_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_string Z3_API Z3_fixedpoint_get_help | ( | Z3_context | c, |
Z3_fixedpoint | f | ||
) |
Return a string describing all fixedpoint available parameters.
Referenced by fixedpoint::help(), and Fixedpoint::help().
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_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.
Referenced by fixedpoint::get_param_descrs(), and Fixedpoint::param_descrs().
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_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_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().
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().
void Z3_API Z3_fixedpoint_init | ( | Z3_context | c, |
Z3_fixedpoint | d, | ||
void * | state | ||
) |
Initialize the context with a user-defined state.
Z3_lbool Z3_API Z3_fixedpoint_query | ( | Z3_context | c, |
Z3_fixedpoint | d, | ||
Z3_ast | query | ||
) |
Pose a query against the asserted rules.
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_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().
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().
void Z3_API Z3_fixedpoint_set_params | ( | Z3_context | c, |
Z3_fixedpoint | f, | ||
Z3_params | p | ||
) |
Set parameters on fixedpoint context.
Referenced by fixedpoint::set(), and Fixedpoint::set().
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().
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.
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_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.
c | - context. |
f | - fixedpoint context. |
num_queries | - number of additional queries to print. |
queries | - additional queries. |
Referenced by z3::operator<<(), Fixedpoint::sexpr(), fixedpoint::to_string(), and Fixedpoint::to_string().
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_fixedpoint Z3_API Z3_mk_fixedpoint | ( | Z3_context | c | ) |
Create a new fixedpoint context.
Referenced by fixedpoint::fixedpoint().