Z3
Public Member Functions | Friends
probe Class Reference
+ Inheritance diagram for probe:

Public Member Functions

 probe (context &c, char const *name)
 
 probe (context &c, double val)
 
 probe (context &c, Z3_probe s)
 
 probe (probe const &s)
 
 ~probe ()
 
 operator Z3_probe () const
 
probeoperator= (probe const &s)
 
double apply (goal const &g) const
 
double operator() (goal const &g) const
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void check_error () const
 

Friends

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)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

§ probe() [1/4]

probe ( context c,
char const *  name 
)
inline

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

1935 :object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
object(context &c)
Definition: z3++.h:330
void check_error() const
Definition: z3++.h:333

§ probe() [2/4]

probe ( context c,
double  val 
)
inline

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

1936 :object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
object(context &c)
Definition: z3++.h:330
void check_error() const
Definition: z3++.h:333

§ probe() [3/4]

probe ( context c,
Z3_probe  s 
)
inline

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

1937 :object(c) { init(s); }
object(context &c)
Definition: z3++.h:330

§ probe() [4/4]

probe ( probe const &  s)
inline

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

1938 :object(s) { init(s.m_probe); }
object(context &c)
Definition: z3++.h:330

§ ~probe()

~probe ( )
inline

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

1939 { Z3_probe_dec_ref(ctx(), m_probe); }
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
context & ctx() const
Definition: z3++.h:332

Member Function Documentation

§ apply()

double apply ( goal const &  g) const
inline

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

Referenced by Tactic::__call__().

1948 { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
context & ctx() const
Definition: z3++.h:332
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...
void check_error() const
Definition: z3++.h:333

§ operator Z3_probe()

operator Z3_probe ( ) const
inline

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

1940 { return m_probe; }

§ operator()()

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

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

1949 { return apply(g); }
double apply(goal const &g) const
Definition: z3++.h:1948

§ operator=()

probe& operator= ( probe const &  s)
inline

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

1941  {
1942  Z3_probe_inc_ref(s.ctx(), s.m_probe);
1943  Z3_probe_dec_ref(ctx(), m_probe);
1944  m_ctx = s.m_ctx;
1945  m_probe = s.m_probe;
1946  return *this;
1947  }
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
context & ctx() const
Definition: z3++.h:332
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
context * m_ctx
Definition: z3++.h:328

Friends And Related Function Documentation

§ operator &&

probe operator&& ( probe const &  p1,
probe const &  p2 
)
friend

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

1995  {
1996  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1997  }
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.
probe(context &c, char const *name)
Definition: z3++.h:1935
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator!

probe operator! ( probe const &  p)
friend

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

2001  {
2002  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
2003  }
probe(context &c, char const *name)
Definition: z3++.h:1935
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< [1/3]

probe operator< ( probe const &  p1,
probe const &  p2 
)
friend

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

1980  {
1981  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1982  }
probe(context &c, char const *name)
Definition: z3++.h:1935
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...
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator< [2/3]

probe operator< ( probe const &  p1,
double  p2 
)
friend

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

1983 { return p1 < probe(p1.ctx(), p2); }
probe(context &c, char const *name)
Definition: z3++.h:1935

§ operator< [3/3]

probe operator< ( double  p1,
probe const &  p2 
)
friend

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

1984 { return probe(p2.ctx(), p1) < p2; }
probe(context &c, char const *name)
Definition: z3++.h:1935

§ operator<= [1/3]

probe operator<= ( probe const &  p1,
probe const &  p2 
)
friend

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

1970  {
1971  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1972  }
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...
probe(context &c, char const *name)
Definition: z3++.h:1935
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator<= [2/3]

probe operator<= ( probe const &  p1,
double  p2 
)
friend

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

1973 { return p1 <= probe(p1.ctx(), p2); }
probe(context &c, char const *name)
Definition: z3++.h:1935

§ operator<= [3/3]

probe operator<= ( double  p1,
probe const &  p2 
)
friend

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

1974 { return probe(p2.ctx(), p1) <= p2; }
probe(context &c, char const *name)
Definition: z3++.h:1935

§ operator== [1/3]

probe operator== ( probe const &  p1,
probe const &  p2 
)
friend

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

1990  {
1991  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1992  }
probe(context &c, char const *name)
Definition: z3++.h:1935
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
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== [2/3]

probe operator== ( probe const &  p1,
double  p2 
)
friend

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

1993 { return p1 == probe(p1.ctx(), p2); }
probe(context &c, char const *name)
Definition: z3++.h:1935

§ operator== [3/3]

probe operator== ( double  p1,
probe const &  p2 
)
friend

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

1994 { return probe(p2.ctx(), p1) == p2; }
probe(context &c, char const *name)
Definition: z3++.h:1935

§ operator> [1/3]

probe operator> ( probe const &  p1,
probe const &  p2 
)
friend

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

1985  {
1986  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1987  }
probe(context &c, char const *name)
Definition: z3++.h:1935
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
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> [2/3]

probe operator> ( probe const &  p1,
double  p2 
)
friend

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

1988 { return p1 > probe(p1.ctx(), p2); }
probe(context &c, char const *name)
Definition: z3++.h:1935

§ operator> [3/3]

probe operator> ( double  p1,
probe const &  p2 
)
friend

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

1989 { return probe(p2.ctx(), p1) > p2; }
probe(context &c, char const *name)
Definition: z3++.h:1935

§ operator>= [1/3]

probe operator>= ( probe const &  p1,
probe const &  p2 
)
friend

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

1975  {
1976  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1977  }
probe(context &c, char const *name)
Definition: z3++.h:1935
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...
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator>= [2/3]

probe operator>= ( probe const &  p1,
double  p2 
)
friend

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

1978 { return p1 >= probe(p1.ctx(), p2); }
probe(context &c, char const *name)
Definition: z3++.h:1935

§ operator>= [3/3]

probe operator>= ( double  p1,
probe const &  p2 
)
friend

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

1979 { return probe(p2.ctx(), p1) >= p2; }
probe(context &c, char const *name)
Definition: z3++.h:1935

§ operator||

probe operator|| ( probe const &  p1,
probe const &  p2 
)
friend

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

1998  {
1999  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2000  }
probe(context &c, char const *name)
Definition: z3++.h:1935
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.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336