RetroSearch Browse

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

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

◆ simplifier() [1/3] ◆ simplifier() [2/3] ◆ simplifier() [3/3] ◆ ~simplifier()

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

void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g)

Decrement the reference counter of the given simplifier.

◆ get_param_descrs()

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

Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t)

Return the parameter description set for the given simplifier object.

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

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

Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t)

Return a string containing a description of parameters accepted by the given simplifier.

◆ operator Z3_simplifier() operator Z3_simplifier ( ) const inline

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

3180

{

return

m_simplifier; }

◆ operator=()

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

3184

object::operator=(s);

3185

m_simplifier = s.m_simplifier;

void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t)

Increment the reference counter of the given simplifier.

◆ operator&

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

friend void check_context(object const &a, object const &b)

simplifier(context &c, char const *name)

Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2)

Return a simplifier that applies t1 to a given goal and t2 to every subgoal produced by t1.

◆ with

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

Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p)

Return a simplifier that applies t using the given set of parameters.

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