Z3
 
Loading...
Searching...
No Matches
Public Member Functions | Protected Attributes | Friends
object Class Reference

#include <z3++.h>

+ Inheritance diagram for object:

Public Member Functions

 object (context &c)
 
contextctx () const
 
Z3_error_code check_error () const
 

Protected Attributes

contextm_ctx
 

Friends

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

Detailed Description

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

Constructor & Destructor Documentation

◆ object()

object ( context c)
inline

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

472:m_ctx(&c) {}
context * m_ctx
Definition z3++.h:470

Member Function Documentation

◆ check_error()

Z3_error_code check_error ( ) const
inline

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

474{ return m_ctx->check_error(); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition z3++.h:192

Referenced by solver::add(), solver::add(), goal::add(), model::add_const_interp(), fixedpoint::add_cover(), func_interp::add_entry(), fixedpoint::add_fact(), model::add_func_interp(), fixedpoint::add_rule(), expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), tactic::apply(), probe::apply(), expr::arg(), func_entry::arg(), sort::array_domain(), sort::array_range(), z3::as_array(), expr::as_binary(), solver::assertions(), optimize::assertions(), fixedpoint::assertions(), expr::at(), expr::body(), sort::bv_size(), expr::char_from_bv(), expr::char_to_bv(), expr::char_to_int(), solver::check(), optimize::check(), optimize::check(), solver::check(), solver::check(), solver::consequences(), expr::contains(), goal::convert_model(), solver::cube(), expr::decl(), expr::denominator(), param_descrs::documentation(), func_decl::domain(), stats::double_value(), func_interp::else_value(), z3::empty(), func_interp::entry(), model::eval(), expr::extract(), z3::fail_if(), sort::fpa_ebits(), sort::fpa_sbits(), optimize::from_file(), fixedpoint::from_file(), optimize::from_string(), fixedpoint::from_string(), fixedpoint::get_answer(), model::get_const_decl(), model::get_const_interp(), fixedpoint::get_cover_delta(), model::get_func_decl(), model::get_func_interp(), solver::get_model(), goal::get_model(), optimize::get_model(), fixedpoint::get_num_levels(), expr::get_sort(), expr::get_string(), ast::hash(), tactic::help(), simplifier::help(), optimize::help(), sort::id(), func_decl::id(), expr::id(), z3::indexof(), expr::is_digit(), stats::is_double(), expr::is_numeral(), expr::is_numeral(), expr::is_numeral(), expr::is_numeral_i(), expr::is_numeral_i64(), expr::is_numeral_u(), expr::is_numeral_u64(), stats::is_uint(), expr::is_well_sorted(), expr::itos(), stats::key(), ast::kind(), z3::last_indexof(), expr::length(), expr::loop(), expr::loop(), optimize::lower(), expr::mk_from_ieee_bv(), expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), tactic::mk_solver(), expr::mk_to_ieee_bv(), sort::name(), func_decl::name(), solver::non_units(), expr::nth(), expr::num_args(), func_entry::num_args(), func_interp::num_entries(), expr::numerator(), optimize::objectives(), func_decl::operator()(), func_decl::operator()(), goal::operator[](), apply_result::operator[](), ast_vector_tpl< T >::operator[](), solver::pop(), probe::probe(), probe::probe(), solver::proof(), solver::push(), ast_vector_tpl< T >::push_back(), fixedpoint::query(), fixedpoint::query(), func_decl::range(), z3::re_empty(), z3::re_full(), solver::reason_unknown(), expr::replace(), solver::reset(), ast_vector_tpl< T >::resize(), fixedpoint::rules(), expr::sbvtos(), solver::set(), optimize::set(), fixedpoint::set(), func_interp::set_else(), simplifier::simplifier(), expr::simplify(), expr::simplify(), solver::solver(), solver::solver(), solver::solver(), solver::solver(), solver::statistics(), optimize::statistics(), fixedpoint::statistics(), expr::stoi(), expr::substitute(), expr::substitute(), expr::substitute(), tactic::tactic(), solver::trail(), solver::trail(), func_decl::transitive_closure(), expr::ubvtos(), stats::uint_value(), expr::unit(), solver::units(), solver::unsat_core(), optimize::unsat_core(), fixedpoint::update_rule(), optimize::upper(), and func_entry::value().

◆ ctx()

context & ctx ( ) const
inline

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

473{ return *m_ctx; }

Referenced by ArithRef::__add__(), BitVecRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), AstMap::__contains__(), AstRef::__copy__(), Goal::__copy__(), AstVector::__copy__(), FuncInterp::__copy__(), ModelRef::__copy__(), AstRef::__deepcopy__(), Datatype::__deepcopy__(), ParamsRef::__deepcopy__(), ParamDescrsRef::__deepcopy__(), Goal::__deepcopy__(), AstVector::__deepcopy__(), AstMap::__deepcopy__(), FuncEntry::__deepcopy__(), FuncInterp::__deepcopy__(), ModelRef::__deepcopy__(), Statistics::__deepcopy__(), Context::__del__(), AstRef::__del__(), ScopedConstructor::__del__(), ScopedConstructorList::__del__(), ParamsRef::__del__(), ParamDescrsRef::__del__(), Goal::__del__(), AstVector::__del__(), AstMap::__del__(), FuncEntry::__del__(), FuncInterp::__del__(), ModelRef::__del__(), Statistics::__del__(), Solver::__del__(), ArithRef::__div__(), BitVecRef::__div__(), ExprRef::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), AstVector::__getitem__(), ModelRef::__getitem__(), Statistics::__getitem__(), AstMap::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), AstVector::__len__(), AstMap::__len__(), ModelRef::__len__(), Statistics::__len__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), BoolRef::__mul__(), ArithRef::__mul__(), BitVecRef::__mul__(), ExprRef::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), ParamsRef::__repr__(), ParamDescrsRef::__repr__(), AstMap::__repr__(), Statistics::__repr__(), BitVecRef::__rlshift__(), ArithRef::__rmod__(), BitVecRef::__rmod__(), ArithRef::__rmul__(), BitVecRef::__rmul__(), BitVecRef::__ror__(), ArithRef::__rpow__(), BitVecRef::__rrshift__(), BitVecRef::__rshift__(), ArithRef::__rsub__(), BitVecRef::__rsub__(), BitVecRef::__rxor__(), AstVector::__setitem__(), AstMap::__setitem__(), ArithRef::__sub__(), BitVecRef::__sub__(), BitVecRef::__xor__(), DatatypeSortRef::accessor(), func_decl::accessors(), solver::add(), optimize::add(), solver::add(), optimize::add(), solver::add(), optimize::add(), goal::add(), model::add_const_interp(), fixedpoint::add_cover(), func_interp::add_entry(), fixedpoint::add_fact(), model::add_func_interp(), fixedpoint::add_rule(), optimize::add_soft(), optimize::add_soft(), expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), tactic::apply(), probe::apply(), ExprRef::arg(), expr::arg(), func_entry::arg(), FuncEntry::arg_value(), expr::args(), func_decl::arity(), FuncInterp::arity(), sort::array_domain(), sort::array_range(), z3::as_array(), expr::as_binary(), goal::as_expr(), Goal::as_expr(), Solver::assert_and_track(), Goal::assert_exprs(), Solver::assert_exprs(), solver::assertions(), optimize::assertions(), fixedpoint::assertions(), ast::ast(), ast::ast(), ast_vector_tpl< T >::ast_vector_tpl(), ast_vector_tpl< T >::ast_vector_tpl(), expr::at(), expr::bit2bool(), expr::body(), QuantifierRef::body(), expr::bool_value(), sort::bv_size(), expr::char_from_bv(), expr::char_to_bv(), expr::char_to_int(), solver::check(), optimize::check(), optimize::check(), solver::check(), Solver::check(), solver::check(), solver::consequences(), sort::constructors(), expr::contains(), goal::convert_model(), Goal::convert_model(), user_propagator_base::ctx(), AstRef::ctx_ref(), solver::cube(), expr::decl(), ExprRef::decl(), func_decl::decl_kind(), ModelRef::decls(), ArrayRef::default(), expr::denominator(), RatNumRef::denominator(), goal::depth(), Goal::depth(), solver::dimacs(), goal::dimacs(), Goal::dimacs(), param_descrs::documentation(), FuncDeclRef::domain(), func_decl::domain(), ArraySortRef::domain_n(), stats::double_value(), func_interp::else_value(), FuncInterp::else_value(), z3::empty(), FuncInterp::entry(), func_interp::entry(), AstMap::erase(), model::eval(), ModelRef::eval(), expr::extract(), expr::extract(), z3::fail_if(), fixedpoint::fixedpoint(), sort::fpa_ebits(), sort::fpa_sbits(), solver::from_file(), optimize::from_file(), fixedpoint::from_file(), optimize::from_string(), solver::from_string(), fixedpoint::from_string(), z3::function(), z3::function(), z3::function(), z3::function(), z3::function(), context::function(), z3::function(), context::function(), z3::function(), z3::function(), z3::function(), Goal::get(), fixedpoint::get_answer(), model::get_const_decl(), model::get_const_interp(), fixedpoint::get_cover_delta(), expr::get_decimal_string(), ParamDescrsRef::get_documentation(), model::get_func_decl(), model::get_func_interp(), ModelRef::get_interp(), Statistics::get_key_value(), ParamDescrsRef::get_kind(), solver::get_model(), goal::get_model(), optimize::get_model(), ParamDescrsRef::get_name(), fixedpoint::get_num_levels(), expr::get_numeral_int(), expr::get_numeral_int64(), expr::get_numeral_uint(), expr::get_numeral_uint64(), solver::get_param_descrs(), tactic::get_param_descrs(), simplifier::get_param_descrs(), fixedpoint::get_param_descrs(), ModelRef::get_sort(), expr::get_string(), expr::get_u32string(), ModelRef::get_universe(), model::has_interp(), ast::hash(), tactic::help(), simplifier::help(), optimize::help(), fixedpoint::help(), expr::hi(), sort::id(), func_decl::id(), expr::id(), goal::inconsistent(), Goal::inconsistent(), z3::indexof(), expr::is_algebraic(), goal::is_decided_sat(), goal::is_decided_unsat(), expr::is_digit(), stats::is_double(), expr::is_exists(), expr::is_forall(), expr::is_lambda(), expr::is_numeral(), expr::is_numeral(), expr::is_numeral(), expr::is_numeral_i(), expr::is_numeral_i64(), expr::is_numeral_u(), expr::is_numeral_u64(), expr::is_string_value(), stats::is_uint(), expr::is_well_sorted(), expr::itos(), stats::key(), AstMap::keys(), Statistics::keys(), symbol::kind(), ast::kind(), param_descrs::kind(), z3::last_indexof(), expr::length(), expr::lo(), expr::loop(), expr::loop(), optimize::lower(), optimize::maximize(), optimize::minimize(), expr::mk_from_ieee_bv(), expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), tactic::mk_solver(), expr::mk_to_ieee_bv(), Solver::model(), sort::name(), func_decl::name(), SortRef::name(), param_descrs::name(), QuantifierRef::no_pattern(), solver::non_units(), expr::nth(), expr::num_args(), func_entry::num_args(), FuncEntry::num_args(), model::num_consts(), func_interp::num_entries(), FuncInterp::num_entries(), goal::num_exprs(), model::num_funcs(), func_decl::num_parameters(), Solver::num_scopes(), ModelRef::num_sorts(), expr::numerator(), optimize::objectives(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), z3::operator<<(), apply_result::operator=(), ast::operator=(), ast_vector_tpl< T >::operator=(), fixedpoint::operator=(), func_entry::operator=(), func_interp::operator=(), goal::operator=(), model::operator=(), optimize::operator=(), param_descrs::operator=(), params::operator=(), probe::operator=(), simplifier::operator=(), solver::operator=(), stats::operator=(), tactic::operator=(), goal::operator[](), apply_result::operator[](), ast_vector_tpl< T >::operator[](), param_descrs::param_descrs(), params::params(), params::params(), FuncDeclRef::params(), QuantifierRef::pattern(), AlgebraicNumRef::poly(), optimize::pop(), Solver::pop(), solver::pop(), Goal::prec(), goal::precision(), solver::proof(), solver::push(), optimize::push(), Solver::push(), AstVector::push(), ast_vector_tpl< T >::push_back(), fixedpoint::query(), fixedpoint::query(), func_decl::range(), FuncDeclRef::range(), ArraySortRef::range(), z3::re_empty(), z3::re_full(), z3::re_intersect(), fixedpoint::reason_unknown(), solver::reason_unknown(), context::recdef(), z3::recfun(), z3::recfun(), z3::recfun(), z3::recfun(), DatatypeSortRef::recognizer(), sort::recognizers(), Context::ref(), fixedpoint::register_relation(), expr::repeat(), expr::replace(), solver::reset(), goal::reset(), AstMap::reset(), Solver::reset(), AstVector::resize(), ast_vector_tpl< T >::resize(), expr::rotate_left(), expr::rotate_right(), fixedpoint::rules(), expr::sbvtos(), params::set(), solver::set(), params::set(), solver::set(), params::set(), solver::set(), params::set(), solver::set(), params::set(), solver::set(), solver::set(), optimize::set(), fixedpoint::set(), Solver::set(), ParamsRef::set(), ast_vector_tpl< T >::set(), func_interp::set_else(), Goal::sexpr(), AstVector::sexpr(), ModelRef::sexpr(), expr::simplify(), expr::simplify(), param_descrs::size(), ast_vector_tpl< T >::size(), stats::size(), goal::size(), apply_result::size(), ParamDescrsRef::size(), Goal::size(), solver::solver(), solver::statistics(), optimize::statistics(), fixedpoint::statistics(), expr::stoi(), symbol::str(), expr::substitute(), expr::substitute(), expr::substitute(), symbol::to_int(), solver::to_smt2(), fixedpoint::to_string(), param_descrs::to_string(), ast::to_string(), ast_vector_tpl< T >::to_string(), model::to_string(), fixedpoint::to_string(), solver::trail(), solver::trail(), func_decl::transitive_closure(), AstVector::translate(), AstRef::translate(), Goal::translate(), ModelRef::translate(), expr::ubvtos(), stats::uint_value(), expr::unit(), solver::units(), solver::unsat_core(), optimize::unsat_core(), fixedpoint::update_rule(), optimize::upper(), context::user_propagate_function(), ParamsRef::validate(), func_entry::value(), FuncEntry::value(), QuantifierRef::var_name(), QuantifierRef::var_sort(), apply_result::~apply_result(), ast_vector_tpl< T >::~ast_vector_tpl(), fixedpoint::~fixedpoint(), func_entry::~func_entry(), func_interp::~func_interp(), goal::~goal(), model::~model(), optimize::~optimize(), param_descrs::~param_descrs(), params::~params(), probe::~probe(), simplifier::~simplifier(), solver::~solver(), stats::~stats(), and tactic::~tactic().

Friends And Related Symbol Documentation

◆ check_context

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

Field Documentation

◆ m_ctx

context* m_ctx
protected

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

Referenced by object::check_error(), object::ctx(), expr::get_sort(), sort::sort_kind(), and ast::~ast().