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

Public Member Functions

 apply_result (context &c, Z3_apply_result s)
 
 apply_result (apply_result const &s)
 
 ~apply_result ()
 
 operator Z3_apply_result () const
 
apply_resultoperator= (apply_result const &s)
 
unsigned size () const
 
goal operator[] (int i) const
 
model convert_model (model const &m, unsigned i=0) const
 
expr as_expr () const
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
Z3_error_code check_error () const
 

Friends

std::ostream & operator<< (std::ostream &out, apply_result const &r)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

◆ apply_result() [1/2]

apply_result ( context c,
Z3_apply_result  s 
)
inline

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

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

◆ apply_result() [2/2]

apply_result ( apply_result const &  s)
inline

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

2095 :object(s) { init(s.m_apply_result); }
object(context &c)
Definition: z3++.h:371

◆ ~apply_result()

~apply_result ( )
inline

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

2096 { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
context & ctx() const
Definition: z3++.h:373
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.

Member Function Documentation

◆ as_expr()

expr as_expr ( ) const
inline

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

2113  {
2114  unsigned n = size();
2115  if (n == 0)
2116  return ctx().bool_val(true);
2117  else if (n == 1)
2118  return operator[](0).as_expr();
2119  else {
2120  array<Z3_ast> args(n);
2121  for (unsigned i = 0; i < n; i++)
2122  args[i] = operator[](i).as_expr();
2123  return expr(ctx(), Z3_mk_or(ctx(), n, args.ptr()));
2124  }
2125  }
expr as_expr() const
Definition: z3++.h:2070
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
context & ctx() const
Definition: z3++.h:373
goal operator[](int i) const
Definition: z3++.h:2106
unsigned size() const
Definition: z3++.h:2105
expr bool_val(bool b)
Definition: z3++.h:2559

◆ convert_model()

model convert_model ( model const &  m,
unsigned  i = 0 
) const
inline

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

2107  {
2108  check_context(*this, m);
2109  Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
2110  check_error();
2111  return model(ctx(), new_m);
2112  }
Z3_error_code check_error() const
Definition: z3++.h:374
Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m)
Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original go...
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377

◆ operator Z3_apply_result()

operator Z3_apply_result ( ) const
inline

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

2097 { return m_apply_result; }

◆ operator=()

apply_result& operator= ( apply_result const &  s)
inline

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

2098  {
2099  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
2100  Z3_apply_result_dec_ref(ctx(), m_apply_result);
2101  m_ctx = s.m_ctx;
2102  m_apply_result = s.m_apply_result;
2103  return *this;
2104  }
context & ctx() const
Definition: z3++.h:373
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
context * m_ctx
Definition: z3++.h:369

◆ operator[]()

goal operator[] ( int  i) const
inline

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

Referenced by apply_result::as_expr().

2106 { assert(0 <= i); Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:374
context & ctx() const
Definition: z3++.h:373
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.

◆ size()

unsigned size ( ) const
inline

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

Referenced by apply_result::as_expr().

2105 { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
context & ctx() const
Definition: z3++.h:373
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.

Friends And Related Function Documentation

◆ operator<<

std::ostream& operator<< ( std::ostream &  out,
apply_result const &  r 
)
friend

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

2128 { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.