Definition at line 4390 of file z3++.h.
4391 return c ? *c : s->
ctx();
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(), user_propagator_base::add(), Simplifier::add(), Fixedpoint::add_cover(), ParserContext::add_decl(), Fixedpoint::add_rule(), Optimize::add_soft(), ParserContext::add_sort(), Tactic::apply(), AlgebraicNumRef::approx(), ExprRef::arg(), FuncEntry::arg_value(), FuncInterp::arity(), Goal::as_expr(), ApplyResult::as_expr(), FPNumRef::as_string(), Solver::assert_and_track(), Optimize::assert_and_track(), Goal::assert_exprs(), Solver::assert_exprs(), Fixedpoint::assert_exprs(), Optimize::assert_exprs(), Solver::assertions(), Optimize::assertions(), SeqRef::at(), SeqSortRef::basis(), ReSortRef::basis(), QuantifierRef::body(), BoolSortRef::cast(), Solver::check(), Optimize::check(), user_propagator_base::conflict(), UserPropagateBase::conflict(), Solver::consequences(), DatatypeSortRef::constructor(), Goal::convert_model(), AstRef::ctx_ref(), UserPropagateBase::ctx_ref(), ExprRef::decl(), ModelRef::decls(), ArrayRef::default(), RatNumRef::denominator(), Goal::depth(), Goal::dimacs(), Solver::dimacs(), ArraySortRef::domain(), FuncDeclRef::domain(), ArraySortRef::domain_n(), FuncInterp::else_value(), FuncInterp::entry(), AstMap::erase(), ModelRef::eval(), FPNumRef::exponent(), FPNumRef::exponent_as_bv(), FPNumRef::exponent_as_long(), Solver::from_file(), Optimize::from_file(), Solver::from_string(), Optimize::from_string(), ParserContext::from_string(), Goal::get(), Fixedpoint::get_answer(), Fixedpoint::get_assertions(), Fixedpoint::get_cover_delta(), ParamDescrsRef::get_documentation(), Fixedpoint::get_ground_sat_answer(), ModelRef::get_interp(), Statistics::get_key_value(), ParamDescrsRef::get_kind(), ParamDescrsRef::get_name(), Fixedpoint::get_num_levels(), Fixedpoint::get_rule_names_along_trace(), Fixedpoint::get_rules(), Fixedpoint::get_rules_along_trace(), ModelRef::get_sort(), ModelRef::get_universe(), Solver::help(), Fixedpoint::help(), Optimize::help(), Simplifier::help(), Tactic::help(), Solver::import_model_converter(), Goal::inconsistent(), Solver::interrupt(), CharRef::is_digit(), FPNumRef::isInf(), FPNumRef::isNaN(), FPNumRef::isNegative(), FPNumRef::isNormal(), FPNumRef::isPositive(), FPNumRef::isSubnormal(), FPNumRef::isZero(), AstMap::keys(), Statistics::keys(), SortRef::kind(), Optimize::maximize(), Optimize::minimize(), Solver::model(), Optimize::model(), SortRef::name(), FuncDeclRef::name(), Solver::next(), user_propagator_base::next_split(), QuantifierRef::no_pattern(), Solver::non_units(), FuncEntry::num_args(), FuncInterp::num_entries(), Solver::num_scopes(), ModelRef::num_sorts(), RatNumRef::numerator(), Optimize::objectives(), Solver::param_descrs(), Fixedpoint::param_descrs(), Optimize::param_descrs(), Simplifier::param_descrs(), Tactic::param_descrs(), FuncDeclRef::params(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), QuantifierRef::pattern(), AlgebraicNumRef::poly(), Optimize::pop(), Solver::pop(), Goal::prec(), Solver::proof(), user_propagator_base::propagate(), Solver::push(), Optimize::push(), AstVector::push(), QuantifierRef::qid(), Fixedpoint::query(), Fixedpoint::query_from_lvl(), FuncDeclRef::range(), ArraySortRef::range(), Solver::reason_unknown(), Fixedpoint::reason_unknown(), Optimize::reason_unknown(), DatatypeSortRef::recognizer(), Context::ref(), user_propagator_base::register_created(), user_propagator_base::register_decide(), user_propagator_base::register_eq(), user_propagator_base::register_final(), user_propagator_base::register_fixed(), Fixedpoint::register_relation(), AstMap::reset(), Solver::reset(), AstVector::resize(), Solver::root(), Solver::set(), Fixedpoint::set(), Optimize::set(), ParamsRef::set(), Solver::set_initial_value(), Optimize::set_initial_value(), Optimize::set_on_model(), Fixedpoint::set_predicate_representation(), Goal::sexpr(), AstVector::sexpr(), ModelRef::sexpr(), Solver::sexpr(), Fixedpoint::sexpr(), Optimize::sexpr(), ApplyResult::sexpr(), FPNumRef::sign(), FPNumRef::sign_as_bv(), FPNumRef::significand(), FPNumRef::significand_as_bv(), FPNumRef::significand_as_long(), ParamDescrsRef::size(), Goal::size(), QuantifierRef::skolem_id(), Tactic::solver(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), DatatypeRef::sort(), FiniteDomainRef::sort(), FPRef::sort(), SeqRef::sort(), Solver::statistics(), Fixedpoint::statistics(), Optimize::statistics(), CharRef::to_bv(), CharRef::to_int(), Solver::to_smt2(), Fixedpoint::to_string(), Solver::trail(), Solver::trail_levels(), AstVector::translate(), FuncInterp::translate(), AstRef::translate(), Goal::translate(), ModelRef::translate(), Solver::translate(), Solver::units(), Solver::unsat_core(), Optimize::unsat_core(), Fixedpoint::update_rule(), user_propagator_base::user_propagator_base(), Simplifier::using_params(), ParamsRef::validate(), FuncEntry::value(), QuantifierRef::var_name(), and QuantifierRef::var_sort().
1.9.1