Definition at line 474 of file z3++.h.
Referenced by ArithRef::__add__(), BitVecRef::__add__(), FPRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), Probe::__call__(), AstMap::__contains__(), AstRef::__copy__(), Goal::__copy__(), AstVector::__copy__(), FuncInterp::__copy__(), ModelRef::__copy__(), Solver::__copy__(), AstRef::__deepcopy__(), Datatype::__deepcopy__(), ParamsRef::__deepcopy__(), ParamDescrsRef::__deepcopy__(), Goal::__deepcopy__(), AstVector::__deepcopy__(), AstMap::__deepcopy__(), FuncEntry::__deepcopy__(), FuncInterp::__deepcopy__(), ModelRef::__deepcopy__(), Statistics::__deepcopy__(), Solver::__deepcopy__(), Fixedpoint::__deepcopy__(), Optimize::__deepcopy__(), ApplyResult::__deepcopy__(), Simplifier::__deepcopy__(), Tactic::__deepcopy__(), Probe::__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__(), Fixedpoint::__del__(), Optimize::__del__(), ApplyResult::__del__(), Simplifier::__del__(), Tactic::__del__(), Probe::__del__(), ParserContext::__del__(), ArithRef::__div__(), BitVecRef::__div__(), FPRef::__div__(), ExprRef::__eq__(), Probe::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), Probe::__ge__(), FPRef::__ge__(), SeqRef::__ge__(), AstVector::__getitem__(), SeqRef::__getitem__(), ModelRef::__getitem__(), Statistics::__getitem__(), ApplyResult::__getitem__(), AstMap::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), Probe::__gt__(), FPRef::__gt__(), SeqRef::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), Probe::__le__(), FPRef::__le__(), SeqRef::__le__(), CharRef::__le__(), AstVector::__len__(), AstMap::__len__(), ModelRef::__len__(), Statistics::__len__(), ApplyResult::__len__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), Probe::__lt__(), FPRef::__lt__(), SeqRef::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), BoolRef::__mul__(), ArithRef::__mul__(), BitVecRef::__mul__(), FPRef::__mul__(), ExprRef::__ne__(), Probe::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), FPRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), FPRef::__rdiv__(), ParamsRef::__repr__(), ParamDescrsRef::__repr__(), AstMap::__repr__(), Statistics::__repr__(), BitVecRef::__rlshift__(), ArithRef::__rmod__(), BitVecRef::__rmod__(), ArithRef::__rmul__(), BitVecRef::__rmul__(), FPRef::__rmul__(), BitVecRef::__ror__(), ArithRef::__rpow__(), BitVecRef::__rrshift__(), BitVecRef::__rshift__(), ArithRef::__rsub__(), BitVecRef::__rsub__(), FPRef::__rsub__(), BitVecRef::__rxor__(), AstVector::__setitem__(), AstMap::__setitem__(), ArithRef::__sub__(), BitVecRef::__sub__(), FPRef::__sub__(), BitVecRef::__xor__(), DatatypeSortRef::accessor(), func_decl::accessors(), solver::add(), optimize::add(), goal::add(), Simplifier::add(), model::add_const_interp(), fixedpoint::add_cover(), Fixedpoint::add_cover(), ParserContext::add_decl(), func_interp::add_entry(), fixedpoint::add_fact(), model::add_func_interp(), fixedpoint::add_rule(), Fixedpoint::add_rule(), optimize::add_soft(), Optimize::add_soft(), ParserContext::add_sort(), expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), tactic::apply(), probe::apply(), Tactic::apply(), AlgebraicNumRef::approx(), 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(), ApplyResult::as_expr(), FPNumRef::as_string(), z3::ashr(), Solver::assert_and_track(), Optimize::assert_and_track(), Goal::assert_exprs(), Solver::assert_exprs(), Fixedpoint::assert_exprs(), Optimize::assert_exprs(), solver::assertions(), optimize::assertions(), fixedpoint::assertions(), Solver::assertions(), Optimize::assertions(), ast::ast(), ast_vector_tpl< T >::ast_vector_tpl(), expr::at(), SeqRef::at(), SeqSortRef::basis(), ReSortRef::basis(), expr::bit2bool(), expr::body(), QuantifierRef::body(), expr::bool_value(), sort::bv_size(), BoolSortRef::cast(), expr::char_from_bv(), expr::char_to_bv(), expr::char_to_int(), solver::check(), optimize::check(), Solver::check(), Optimize::check(), z3::cond(), UserPropagateBase::conflict(), solver::consequences(), Solver::consequences(), DatatypeSortRef::constructor(), sort::constructors(), expr::contains(), goal::convert_model(), Goal::convert_model(), user_propagator_base::ctx(), AstRef::ctx_ref(), UserPropagateBase::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(), Solver::dimacs(), param_descrs::documentation(), ArraySortRef::domain(), 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(), z3::exists(), FPNumRef::exponent(), FPNumRef::exponent_as_bv(), FPNumRef::exponent_as_long(), expr::extract(), z3::fail_if(), fixedpoint::fixedpoint(), z3::foldl(), z3::foldli(), z3::forall(), sort::fpa_ebits(), sort::fpa_sbits(), solver::from_file(), optimize::from_file(), fixedpoint::from_file(), Solver::from_file(), Optimize::from_file(), optimize::from_string(), solver::from_string(), fixedpoint::from_string(), Solver::from_string(), Optimize::from_string(), ParserContext::from_string(), context::function(), z3::function(), Goal::get(), fixedpoint::get_answer(), Fixedpoint::get_answer(), Fixedpoint::get_assertions(), model::get_const_decl(), model::get_const_interp(), fixedpoint::get_cover_delta(), Fixedpoint::get_cover_delta(), expr::get_decimal_string(), ParamDescrsRef::get_documentation(), model::get_func_decl(), model::get_func_interp(), Fixedpoint::get_ground_sat_answer(), 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(), 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(), Fixedpoint::get_rule_names_along_trace(), Fixedpoint::get_rules(), Fixedpoint::get_rules_along_trace(), 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(), Solver::help(), Fixedpoint::help(), Optimize::help(), Simplifier::help(), Tactic::help(), expr::hi(), sort::id(), func_decl::id(), expr::id(), Solver::import_model_converter(), goal::inconsistent(), Goal::inconsistent(), z3::indexof(), Solver::interrupt(), expr::is_algebraic(), goal::is_decided_sat(), goal::is_decided_unsat(), expr::is_digit(), CharRef::is_digit(), stats::is_double(), expr::is_exists(), expr::is_forall(), expr::is_lambda(), 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(), FPNumRef::isInf(), FPNumRef::isNaN(), FPNumRef::isNegative(), FPNumRef::isNormal(), FPNumRef::isPositive(), FPNumRef::isSubnormal(), FPNumRef::isZero(), expr::itos(), stats::key(), AstMap::keys(), Statistics::keys(), symbol::kind(), ast::kind(), SortRef::kind(), param_descrs::kind(), z3::lambda(), z3::last_indexof(), expr::length(), z3::linear_order(), expr::lo(), expr::loop(), optimize::lower(), z3::lshr(), z3::map(), z3::mapi(), optimize::maximize(), Optimize::maximize(), optimize::minimize(), 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(), Optimize::model(), sort::name(), func_decl::name(), SortRef::name(), FuncDeclRef::name(), param_descrs::name(), Solver::next(), QuantifierRef::no_pattern(), solver::non_units(), 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(), RatNumRef::numerator(), optimize::objectives(), Optimize::objectives(), z3::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==(), goal::operator[](), apply_result::operator[](), ast_vector_tpl< T >::operator[](), optimize::optimize(), param_descrs::param_descrs(), Solver::param_descrs(), Fixedpoint::param_descrs(), Optimize::param_descrs(), Simplifier::param_descrs(), Tactic::param_descrs(), params::params(), FuncDeclRef::params(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), z3::partial_order(), QuantifierRef::pattern(), z3::piecewise_linear_order(), AlgebraicNumRef::poly(), optimize::pop(), Optimize::pop(), Solver::pop(), solver::pop(), Goal::prec(), goal::precision(), z3::prefixof(), solver::proof(), Solver::proof(), user_propagator_base::propagate(), solver::push(), optimize::push(), Solver::push(), Optimize::push(), AstVector::push(), ast_vector_tpl< T >::push_back(), QuantifierRef::qid(), fixedpoint::query(), Fixedpoint::query(), Fixedpoint::query_from_lvl(), func_decl::range(), FuncDeclRef::range(), ArraySortRef::range(), z3::re_diff(), z3::re_empty(), z3::re_full(), z3::re_intersect(), fixedpoint::reason_unknown(), solver::reason_unknown(), Solver::reason_unknown(), Fixedpoint::reason_unknown(), Optimize::reason_unknown(), context::recdef(), z3::recfun(), DatatypeSortRef::recognizer(), sort::recognizers(), Context::ref(), fixedpoint::register_relation(), Fixedpoint::register_relation(), expr::repeat(), expr::replace(), solver::reset(), goal::reset(), AstMap::reset(), Solver::reset(), AstVector::resize(), ast_vector_tpl< T >::resize(), Solver::root(), expr::rotate_left(), expr::rotate_right(), fixedpoint::rules(), expr::sbvtos(), z3::select(), params::set(), solver::set(), optimize::set(), fixedpoint::set(), Solver::set(), Fixedpoint::set(), Optimize::set(), ParamsRef::set(), ast_vector_tpl< T >::set(), func_interp::set_else(), solver::set_initial_value(), optimize::set_initial_value(), Solver::set_initial_value(), Optimize::set_initial_value(), z3::set_intersect(), Optimize::set_on_model(), Fixedpoint::set_predicate_representation(), z3::set_union(), Goal::sexpr(), AstVector::sexpr(), ModelRef::sexpr(), Solver::sexpr(), Fixedpoint::sexpr(), Optimize::sexpr(), ApplyResult::sexpr(), z3::sext(), z3::sge(), z3::sgt(), z3::shl(), FPNumRef::sign(), FPNumRef::sign_as_bv(), FPNumRef::significand(), FPNumRef::significand_as_bv(), FPNumRef::significand_as_long(), expr::simplify(), param_descrs::size(), ast_vector_tpl< T >::size(), stats::size(), goal::size(), apply_result::size(), ParamDescrsRef::size(), Goal::size(), QuantifierRef::skolem_id(), z3::sle(), z3::slt(), z3::smod(), solver::solver(), Tactic::solver(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), DatatypeRef::sort(), FiniteDomainRef::sort(), FPRef::sort(), SeqRef::sort(), z3::srem(), solver::statistics(), optimize::statistics(), fixedpoint::statistics(), Solver::statistics(), Fixedpoint::statistics(), Optimize::statistics(), expr::stoi(), z3::store(), symbol::str(), expr::substitute(), z3::suffixof(), CharRef::to_bv(), symbol::to_int(), CharRef::to_int(), z3::to_real(), solver::to_smt2(), 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(), Solver::trail_levels(), func_decl::transitive_closure(), AstVector::translate(), FuncInterp::translate(), AstRef::translate(), Goal::translate(), ModelRef::translate(), Solver::translate(), z3::tree_order(), expr::ubvtos(), z3::udiv(), z3::uge(), z3::ugt(), stats::uint_value(), z3::ule(), z3::ult(), expr::unit(), solver::units(), Solver::units(), solver::unsat_core(), optimize::unsat_core(), Solver::unsat_core(), Optimize::unsat_core(), fixedpoint::update_rule(), Fixedpoint::update_rule(), optimize::upper(), z3::urem(), context::user_propagate_function(), Simplifier::using_params(), 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().
Inheritance diagram for object:
1.9.1
