Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/z3__fixedpoint_8h_source.html below:

Z3: doc/tmp/z3_fixedpoint.h Source File

num_args,

args[]);

num_relations,

relations[]);

num_relations,

num_queries,

,

[],

,

[]);

,

[],

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_add_constraint(Z3_context c, Z3_fixedpoint d, Z3_ast e, unsigned lvl)

void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)

Increment the reference counter of the given fixedpoint context.

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:

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.

void(* Z3_fixedpoint_predecessor_eh)(void *state)

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

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.

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.

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.

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

Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)

Retrieve set of background assertions from fixedpoint context.

const char * Z3_string

Z3 string type. It is just an alias for const char *.

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.

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

Z3_lbool

Lifted Boolean type: false, undefined, true.

void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)

Decrement the reference counter of the given fixedpoint context.

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

Pose a query against the asserted rules.

Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)

Retrieve set of rules from fixedpoint context.

Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)

Create a new fixedpoint context.

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.

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.

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_init(Z3_context c, Z3_fixedpoint d, void *state)

Initialize the context with a user-defined state.

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.

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

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_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.

Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)

Return a string describing all fixedpoint available parameters.

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

Assert a constraint to the fixedpoint context.

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.

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

Set parameters on fixedpoint context.

Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)

Retrieve a formula that encodes satisfying answers to the 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...

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 forw...

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.

void(* Z3_fixedpoint_unfold_eh)(void *state)

System.IntPtr Z3_ast_vector

System.IntPtr Z3_func_decl

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4