RetroSearch Browse

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

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

Z3: fixedpoint Class Reference

Definition at line 3402 of file z3++.h.

◆ fixedpoint() [1/2]

Definition at line 3405 of file z3++.h.

void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)

Increment the reference counter of the given fixedpoint context.

Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)

Create a new fixedpoint context.

Referenced by Fixedpoint::__deepcopy__(), Fixedpoint::__del__(), Fixedpoint::add_cover(), Fixedpoint::add_rule(), Fixedpoint::assert_exprs(), Fixedpoint::get_answer(), Fixedpoint::get_assertions(), Fixedpoint::get_cover_delta(), Fixedpoint::get_ground_sat_answer(), Fixedpoint::get_num_levels(), Fixedpoint::get_rule_names_along_trace(), Fixedpoint::get_rules(), Fixedpoint::get_rules_along_trace(), Fixedpoint::help(), Fixedpoint::param_descrs(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), Fixedpoint::query(), Fixedpoint::query_from_lvl(), Fixedpoint::reason_unknown(), Fixedpoint::register_relation(), Fixedpoint::set(), Fixedpoint::set_predicate_representation(), Fixedpoint::sexpr(), Fixedpoint::statistics(), Fixedpoint::to_string(), and Fixedpoint::update_rule().

◆ fixedpoint() [2/2]

Definition at line 3406 of file z3++.h.

◆ ~fixedpoint()

Definition at line 3407 of file z3++.h.

void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)

Decrement the reference counter of the given fixedpoint context.

◆ add_cover()

Definition at line 3444 of file z3++.h.

Z3_error_code check_error() const

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

◆ add_fact() void add_fact ( func_decl & f, unsigned * args ) inline

Definition at line 3427 of file z3++.h.

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.

◆ add_rule() void add_rule ( expr & rule, symbol const & name ) inline

Definition at line 3426 of file z3++.h.

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::fact(), and Fixedpoint::rule().

◆ assertions()

Definition at line 3447 of file z3++.h.

Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)

Retrieve set of background assertions from fixedpoint context.

System.IntPtr Z3_ast_vector

ast_vector_tpl< expr > expr_vector

Referenced by Solver::to_smt2().

◆ from_file()

Definition at line 3421 of file z3++.h.

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

◆ from_string()

Definition at line 3416 of file z3++.h.

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

◆ get_answer()

Definition at line 3435 of file z3++.h.

Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)

Retrieve a formula that encodes satisfying answers to the query.

◆ get_cover_delta()

Definition at line 3439 of file z3++.h.

3442 return

expr(

ctx

(), r);

Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)

◆ get_num_levels()

Definition at line 3438 of file z3++.h.

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.

◆ get_param_descrs()

Definition at line 3451 of file z3++.h.

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.

◆ help() std::string help ( ) const inline

Definition at line 3450 of file z3++.h.

Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)

Return a string describing all fixedpoint available parameters.

◆ operator Z3_fixedpoint() operator Z3_fixedpoint ( ) const inline ◆ operator=()

Definition at line 3408 of file z3++.h.

3412

object::operator=(o);

◆ query() [1/2]

Definition at line 3428 of file z3++.h.

Z3_lbool

Lifted Boolean type: false, undefined, true.

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

Pose a query against the asserted rules.

check_result to_check_result(Z3_lbool l)

◆ query() [2/2]

Definition at line 3429 of file z3++.h.

3430

array<Z3_func_decl> rs(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.

◆ reason_unknown() std::string reason_unknown ( ) inline

Definition at line 3436 of file z3++.h.

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.

◆ register_relation()

Definition at line 3446 of file z3++.h.

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

◆ rules()

Definition at line 3448 of file z3++.h.

Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)

Retrieve set of rules from fixedpoint context.

◆ set()

Definition at line 3449 of file z3++.h.

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

Set parameters on fixedpoint context.

◆ statistics() stats statistics ( ) const inline

Definition at line 3445 of file z3++.h.

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.

◆ to_string() [1/2] std::string to_string ( ) inline

Definition at line 3452 of file z3++.h.

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.

◆ to_string() [2/2]

Definition at line 3453 of file z3++.h.

3454

array<Z3_ast> qs(queries);

◆ update_rule() void update_rule ( expr & rule, symbol const & name ) inline

Definition at line 3437 of file z3++.h.

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.

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