RetroSearch Browse

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

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

Z3: probe Class Reference

probe operator<= (probe const &p1, probe const &p2) probe operator<= (probe const &p1, double p2) probe operator<= (double p1, probe const &p2) probe operator>= (probe const &p1, probe const &p2) probe operator>= (probe const &p1, double p2) probe operator>= (double p1, probe const &p2) probe operator< (probe const &p1, probe const &p2) probe operator< (probe const &p1, double p2) probe operator< (double p1, probe const &p2) probe operator> (probe const &p1, probe const &p2) probe operator> (probe const &p1, double p2) probe operator> (double p1, probe const &p2) probe operator== (probe const &p1, probe const &p2) probe operator== (probe const &p1, double p2) probe operator== (double p1, probe const &p2) probe operator&& (probe const &p1, probe const &p2) probe operator|| (probe const &p1, probe const &p2) probe operator! (probe const &p)

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

◆ probe() [1/4] ◆ probe() [2/4] ◆ probe() [3/4] ◆ probe() [4/4] ◆ ~probe()

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

void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)

Decrement the reference counter of the given probe.

◆ apply() double apply ( goal const & g ) const inline

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

double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)

Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0....

Referenced by Tactic::__call__(), and probe::operator()().

◆ operator Z3_probe() operator Z3_probe ( ) const inline ◆ operator()() double operator() ( goal const & g ) const inline

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

3231

{

return apply

(g); }

double apply(goal const &g) const

◆ operator=()

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

3226

object::operator=(s);

3227

m_probe = s.m_probe;

void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)

Increment the reference counter of the given probe.

◆ operator!

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

3284

Z3_probe r =

Z3_probe_not

(p.ctx(), p); p.check_error();

return probe

(p.ctx(), r);

probe(context &c, char const *name)

Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)

Return a probe that evaluates to "true" when p does not evaluate to true.

◆ operator&&

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

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

Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when p1 and p2 evaluates to true.

◆ operator< [1/3]

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

3266

{

return probe

(p2.ctx(), p1) < p2; }

◆ operator< [2/3]

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

3265

{

return

p1 <

probe

(p1.ctx(), p2); }

◆ operator< [3/3]

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

Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...

◆ operator<= [1/3]

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

3256

{

return probe

(p2.ctx(), p1) <= p2; }

◆ operator<= [2/3]

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

3255

{

return

p1 <=

probe

(p1.ctx(), p2); }

◆ operator<= [3/3]

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

Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...

◆ operator== [1/3]

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

3276

{

return probe

(p2.ctx(), p1) == p2; }

◆ operator== [2/3]

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

3275

{

return

p1 ==

probe

(p1.ctx(), p2); }

◆ operator== [3/3]

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

Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...

◆ operator> [1/3]

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

3271

{

return probe

(p2.ctx(), p1) > p2; }

◆ operator> [2/3]

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

3270

{

return

p1 >

probe

(p1.ctx(), p2); }

◆ operator> [3/3]

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

Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...

◆ operator>= [1/3]

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

3261

{

return probe

(p2.ctx(), p1) >= p2; }

◆ operator>= [2/3]

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

3260

{

return

p1 >=

probe

(p1.ctx(), p2); }

◆ operator>= [3/3]

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

Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...

◆ operator||

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

Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when p1 or p2 evaluates to true.

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