Z3
 
Loading...
Searching...
No Matches
object Class Reference

#include <z3++.h>

+ Inheritance diagram for object:

Public Member Functions

 object (context &c)
 
virtual ~object ()=default
 
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

◆ ~object()

virtual ~object ( )
virtualdefault

Member Function Documentation

◆ check_error()

Z3_error_code check_error ( ) const
inline

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

475{ 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 goal::add(), solver::add(), solver::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(), probe::apply(), tactic::apply(), expr::arg(), func_entry::arg(), sort::array_domain(), sort::array_range(), z3::as_array(), expr::as_binary(), fixedpoint::assertions(), optimize::assertions(), solver::assertions(), expr::at(), expr::body(), sort::bv_size(), expr::char_from_bv(), expr::char_to_bv(), expr::char_to_int(), optimize::check(), optimize::check(), solver::check(), solver::check(), solver::check(), z3::cond(), 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(), z3::exists(), z3::exists(), z3::exists(), z3::exists(), z3::exists(), expr::extract(), z3::fail_if(), z3::forall(), z3::forall(), z3::forall(), z3::forall(), z3::forall(), sort::fpa_ebits(), sort::fpa_sbits(), fixedpoint::from_file(), optimize::from_file(), fixedpoint::from_string(), optimize::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(), goal::get_model(), optimize::get_model(), solver::get_model(), fixedpoint::get_num_levels(), expr::get_sort(), expr::get_string(), ast::hash(), optimize::help(), simplifier::help(), tactic::help(), expr::id(), func_decl::id(), sort::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::lambda(), z3::lambda(), z3::lambda(), z3::lambda(), z3::lambda(), 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(), func_decl::name(), sort::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()(), apply_result::operator[](), ast_vector_tpl< T >::operator[](), goal::operator[](), solver::pop(), z3::prefixof(), 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(), z3::select(), z3::select(), fixedpoint::set(), optimize::set(), solver::set(), func_interp::set_else(), optimize::set_initial_value(), solver::set_initial_value(), z3::set_intersect(), z3::set_union(), simplifier::simplifier(), expr::simplify(), expr::simplify(), solver::solver(), solver::solver(), solver::solver(), solver::solver(), fixedpoint::statistics(), optimize::statistics(), solver::statistics(), expr::stoi(), z3::store(), z3::store(), expr::substitute(), expr::substitute(), expr::substitute(), z3::suffixof(), tactic::tactic(), z3::to_real(), solver::trail(), solver::trail(), func_decl::transitive_closure(), expr::ubvtos(), stats::uint_value(), expr::unit(), solver::units(), optimize::unsat_core(), solver::unsat_core(), fixedpoint::update_rule(), optimize::upper(), func_entry::value(), and z3::when().

◆ ctx()

context & ctx ( ) const
inline

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

474{ return *m_ctx; }

Referenced by ArithRef::__add__(), BitVecRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), AstMap::__contains__(), AstRef::__copy__(), AstVector::__copy__(), FuncInterp::__copy__(), Goal::__copy__(), ModelRef::__copy__(), AstMap::__deepcopy__(), AstRef::__deepcopy__(), AstVector::__deepcopy__(), Datatype::__deepcopy__(), FuncEntry::__deepcopy__(), FuncInterp::__deepcopy__(), Goal::__deepcopy__(), ModelRef::__deepcopy__(), ParamDescrsRef::__deepcopy__(), ParamsRef::__deepcopy__(), Statistics::__deepcopy__(), AstMap::__del__(), AstRef::__del__(), AstVector::__del__(), Context::__del__(), FuncEntry::__del__(), FuncInterp::__del__(), Goal::__del__(), ModelRef::__del__(), ParamDescrsRef::__del__(), ParamsRef::__del__(), ScopedConstructor::__del__(), ScopedConstructorList::__del__(), Solver::__del__(), Statistics::__del__(), ArithRef::__div__(), BitVecRef::__div__(), ExprRef::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), AstMap::__getitem__(), AstVector::__getitem__(), ModelRef::__getitem__(), Statistics::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), AstMap::__len__(), AstVector::__len__(), ModelRef::__len__(), Statistics::__len__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), ArithRef::__mul__(), BitVecRef::__mul__(), BoolRef::__mul__(), ExprRef::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), AstMap::__repr__(), ParamDescrsRef::__repr__(), ParamsRef::__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__(), AstMap::__setitem__(), AstVector::__setitem__(), ArithRef::__sub__(), BitVecRef::__sub__(), BitVecRef::__xor__(), DatatypeSortRef::accessor(), func_decl::accessors(), goal::add(), optimize::add(), optimize::add(), optimize::add(), solver::add(), solver::add(), solver::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(), probe::apply(), tactic::apply(), expr::arg(), func_entry::arg(), ExprRef::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(), z3::ashr(), z3::ashr(), z3::ashr(), Solver::assert_and_track(), Goal::assert_exprs(), Solver::assert_exprs(), fixedpoint::assertions(), optimize::assertions(), solver::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(), optimize::check(), optimize::check(), solver::check(), solver::check(), solver::check(), Solver::check(), z3::cond(), 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(), goal::dimacs(), solver::dimacs(), Goal::dimacs(), param_descrs::documentation(), func_decl::domain(), FuncDeclRef::domain(), ArraySortRef::domain_n(), stats::double_value(), func_interp::else_value(), FuncInterp::else_value(), z3::empty(), func_interp::entry(), FuncInterp::entry(), AstMap::erase(), model::eval(), ModelRef::eval(), z3::exists(), z3::exists(), z3::exists(), z3::exists(), z3::exists(), expr::extract(), expr::extract(), z3::fail_if(), fixedpoint::fixedpoint(), z3::foldl(), z3::foldli(), z3::forall(), z3::forall(), z3::forall(), z3::forall(), z3::forall(), sort::fpa_ebits(), sort::fpa_sbits(), fixedpoint::from_file(), optimize::from_file(), solver::from_file(), fixedpoint::from_string(), optimize::from_string(), solver::from_string(), context::function(), context::function(), z3::function(), z3::function(), z3::function(), z3::function(), z3::function(), z3::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(), goal::get_model(), optimize::get_model(), solver::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(), fixedpoint::get_param_descrs(), simplifier::get_param_descrs(), solver::get_param_descrs(), tactic::get_param_descrs(), ModelRef::get_sort(), expr::get_string(), expr::get_u32string(), ModelRef::get_universe(), model::has_interp(), ast::hash(), fixedpoint::help(), optimize::help(), simplifier::help(), tactic::help(), expr::hi(), expr::id(), func_decl::id(), sort::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(), ast::kind(), param_descrs::kind(), symbol::kind(), z3::lambda(), z3::lambda(), z3::lambda(), z3::lambda(), z3::lambda(), z3::last_indexof(), expr::length(), z3::linear_order(), expr::lo(), expr::loop(), expr::loop(), optimize::lower(), z3::lshr(), z3::lshr(), z3::lshr(), z3::map(), z3::mapi(), 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(), model::model(), Solver::model(), func_decl::name(), param_descrs::name(), sort::name(), SortRef::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(), z3::operator!=(), z3::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()(), 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=(), z3::operator==(), z3::operator==(), apply_result::operator[](), ast_vector_tpl< T >::operator[](), goal::operator[](), optimize::optimize(), param_descrs::param_descrs(), params::params(), params::params(), FuncDeclRef::params(), z3::partial_order(), QuantifierRef::pattern(), z3::piecewise_linear_order(), AlgebraicNumRef::poly(), optimize::pop(), solver::pop(), Solver::pop(), Goal::prec(), goal::precision(), z3::prefixof(), solver::proof(), user_propagator_base::propagate(), user_propagator_base::propagate(), optimize::push(), solver::push(), AstVector::push(), Solver::push(), ast_vector_tpl< T >::push_back(), QuantifierRef::qid(), fixedpoint::query(), fixedpoint::query(), func_decl::range(), ArraySortRef::range(), FuncDeclRef::range(), z3::re_diff(), 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(), goal::reset(), solver::reset(), AstMap::reset(), Solver::reset(), ast_vector_tpl< T >::resize(), AstVector::resize(), expr::rotate_left(), expr::rotate_right(), fixedpoint::rules(), expr::sbvtos(), z3::select(), z3::select(), z3::select(), ast_vector_tpl< T >::set(), fixedpoint::set(), optimize::set(), params::set(), params::set(), params::set(), params::set(), params::set(), solver::set(), solver::set(), solver::set(), solver::set(), solver::set(), solver::set(), ParamsRef::set(), Solver::set(), func_interp::set_else(), optimize::set_initial_value(), optimize::set_initial_value(), optimize::set_initial_value(), solver::set_initial_value(), solver::set_initial_value(), solver::set_initial_value(), z3::set_intersect(), z3::set_union(), AstVector::sexpr(), Goal::sexpr(), ModelRef::sexpr(), z3::sext(), z3::sge(), z3::sge(), z3::sge(), z3::sgt(), z3::sgt(), z3::sgt(), z3::shl(), z3::shl(), z3::shl(), expr::simplify(), expr::simplify(), apply_result::size(), ast_vector_tpl< T >::size(), goal::size(), param_descrs::size(), stats::size(), Goal::size(), ParamDescrsRef::size(), QuantifierRef::skolem_id(), z3::sle(), z3::sle(), z3::sle(), z3::slt(), z3::slt(), z3::slt(), z3::smod(), z3::smod(), z3::smod(), solver::solver(), solver::solver(), z3::srem(), z3::srem(), z3::srem(), fixedpoint::statistics(), optimize::statistics(), solver::statistics(), expr::stoi(), z3::store(), z3::store(), z3::store(), z3::store(), z3::store(), symbol::str(), expr::substitute(), expr::substitute(), expr::substitute(), z3::suffixof(), symbol::to_int(), z3::to_real(), solver::to_smt2(), ast::to_string(), ast_vector_tpl< T >::to_string(), fixedpoint::to_string(), fixedpoint::to_string(), model::to_string(), param_descrs::to_string(), solver::trail(), solver::trail(), func_decl::transitive_closure(), AstRef::translate(), AstVector::translate(), Goal::translate(), ModelRef::translate(), z3::tree_order(), expr::ubvtos(), z3::udiv(), z3::udiv(), z3::udiv(), z3::uge(), z3::uge(), z3::uge(), z3::ugt(), z3::ugt(), z3::ugt(), stats::uint_value(), z3::ule(), z3::ule(), z3::ule(), z3::ult(), z3::ult(), z3::ult(), expr::unit(), solver::units(), optimize::unsat_core(), solver::unsat_core(), fixedpoint::update_rule(), optimize::upper(), z3::urem(), z3::urem(), z3::urem(), context::user_propagate_function(), ParamsRef::validate(), func_entry::value(), FuncEntry::value(), QuantifierRef::var_name(), QuantifierRef::var_sort(), z3::when(), z3::zext(), 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

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().