Z3
 
Loading...
Searching...
No Matches
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_resultoperator= (apply_result const &s)
 
unsigned size () const
 
goal operator[] (int i) const
 
- Public Member Functions inherited from object
 object (context &c)
 
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 2939 of file z3++.h.

Constructor & Destructor Documentation

◆ apply_result() [1/2]

apply_result ( context c,
Z3_apply_result  s 
)
inline

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

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

◆ apply_result() [2/2]

apply_result ( apply_result const &  s)
inline

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

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

◆ ~apply_result()

~apply_result ( )
inline

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

2948{ Z3_apply_result_dec_ref(ctx(), m_apply_result); }
context & ctx() const
Definition: z3++.h:451
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 2949 of file z3++.h.

2949{ return m_apply_result; }

◆ operator=()

apply_result & operator= ( apply_result const &  s)
inline

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

2950 {
2951 Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
2952 Z3_apply_result_dec_ref(ctx(), m_apply_result);
2953 object::operator=(s);
2954 m_apply_result = s.m_apply_result;
2955 return *this;
2956 }
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 2958 of file z3++.h.

2958{ 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:452
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 2957 of file z3++.h.

2957{ return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
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 2961 of file z3++.h.

2961{ 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.