Z3 |

Public Member Functions | Friends
apply_result Class Reference

`#include <z3++.h>`

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_result & | operator= (apply_result const &s)
unsigned | size () const
goal | operator[] (int i) const
Public Member Functions inherited from object
| object (context &c)
context & | ctx () 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
context * | m_ctx

## Detailed Description

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

## Constructor & Destructor Documentation

## ◆ apply_result() [1/2]

apply_result | ( | context & | c,
|  | Z3_apply_result | s
| ) |  |
| inline

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

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

## ◆ apply_result() [2/2]

apply_result | ( | apply_result const & | s | ) |
| inline

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

2835:object(s) { init(s.m_apply_result); }

## ◆ ~apply_result()

~apply_result | ( |  | ) |
| inline

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

2836{ Z3_apply_result_dec_ref(ctx(), m_apply_result); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
Z3_apply_result_dec_ref
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

## ◆ operator Z3_apply_result()

operator Z3_apply_result | ( |  | ) | const
| inline

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

2837{ return m_apply_result; }

## ◆ operator=()

apply_result & operator= | ( | apply_result const & | s | ) |
| inline

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

2838 {
2839 Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
2840 Z3_apply_result_dec_ref(ctx(), m_apply_result);
2841 object::operator=(s);
2842 m_apply_result = s.m_apply_result;
2843 return *this;
2844 }
Z3_apply_result_inc_ref
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.

## ◆ operator[]()

goal operator[] | ( | int | i | ) | const
| inline

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

2846{ assert(0 <= i); Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
Z3_apply_result_get_subgoal
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 2845 of file z3++.h.

2845{ return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
Z3_apply_result_get_num_subgoals
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.

Referenced by ParamDescrsRef::__len__(), Goal::__len__(), BitVecNumRef::as_signed_long(), and BitVecSortRef::subsort().

## Friends And Related Function Documentation

## ◆ operator<<

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

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

2849{ out << Z3_apply_result_to_string(r.ctx(), r); return out; }
Z3_apply_result_to_string
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.