cprover
|
Go to the source code of this file.
Functions | |
bool | simplify (exprt &expr, const namespacet &ns) |
exprt | simplify_expr (const exprt &src, const namespacet &ns) |
bool simplify | ( | exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 2435 of file simplify_expr.cpp.
References simplify_exprt::simplify().
Referenced by disjunctive_polynomial_accelerationt::accelerate(), partial_order_concurrencyt::add_constraint(), goto_checkt::add_guarded_claim(), string_refinementt::add_lemma(), add_padding_gcc(), add_to_index_set(), build_full_lhs_rec(), build_goto_trace(), goto_convertt::clean_expr(), goto_program2codet::cleanup_code_ifthenelse(), goto_program2codet::cleanup_expr(), symex_slice_by_tracet::compute_ts_back(), goto_convertt::convert(), goto_program2codet::convert_do_while(), goto_program2codet::convert_goto_break_continue(), goto_program2codet::convert_goto_goto(), goto_program2codet::convert_goto_if(), goto_program2codet::convert_goto_while(), cpp_typecheckt::convert_initializer(), goto_program_dereferencet::dereference_failure(), acceleration_utilst::do_assumptions(), goto_symext::do_simplify(), c_typecheck_baset::do_special_functions(), linkingt::duplicate_object_symbol(), get_string_argument(), goto_convertt::get_string_constant(), value_set_fit::get_value_set(), value_set_fivrnst::get_value_set(), value_set_fivrt::get_value_set(), value_sett::get_value_set(), value_sett::get_value_set_rec(), cpp_typecheckt::implicit_conversion_sequence(), symex_slice_by_tracet::implied_guards(), symex_slice_by_tracet::implies_false(), c_typecheck_baset::make_constant(), c_typecheck_baset::make_constant_index(), printf_formattert::make_type(), member_offset_expr(), acceleration_utilst::precondition(), polynomial_acceleratort::precondition(), memory_model_tsot::program_order(), constant_propagator_domaint::replace_constants_and_simplify(), size_of_expr(), symex_slice_by_tracet::slice_by_trace(), symex_slice_by_tracet::slice_SSA_steps(), goto_symext::symex_allocate(), invariant_set_domaint::transform(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), cpp_typecheckt::typecheck_template_args(), cpp_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_vector_type(), unpack_rec(), and unsigned_from_ns().
exprt simplify_expr | ( | const exprt & | src, |
const namespacet & | ns | ||
) |
Definition at line 2440 of file simplify_expr.cpp.
References simplify_exprt::simplify().
Referenced by add_string_equation_to_symbol_resolution(), linkingt::adjust_object_type_rec(), ai_domain_baset::ai_simplify_lhs(), acceleration_utilst::assign_array(), interval_domaint::assume(), boolbvt::bv_get_unbounded_array(), custom_bitvector_analysist::check(), check_axioms(), goto_program2codet::cleanup_code_ifthenelse(), smt2_solvert::command(), convert_decl(), boolbvt::convert_index(), interpretert::evaluate(), flatten_byte_extract(), flatten_byte_update(), generate_symbol_resolution_from_equations(), get_array(), get_char_array_and_concretize(), rw_range_sett::get_objects_byte_extract(), rw_range_sett::get_objects_index(), rw_range_sett::get_objects_shift(), c_typecastt::implicit_typecast_followed(), instantiate_quantifier(), string_constraintt::is_valid_string_constraint(), list_calls_and_arguments(), taint_analysist::operator()(), dereferencet::read_object(), cpp_typecheckt::reinterpret_typecast(), cpp_typecheckt::standard_conversion_pointer(), symex_bmct::symex_step(), string_constraint_generatort::to_integer_or_default(), custom_bitvector_domaint::transform(), remove_const_function_pointerst::try_resolve_expression(), remove_const_function_pointerst::try_resolve_function_call(), c_typecheck_baset::typecheck_expr_rel(), and c_typecheck_baset::typecheck_expr_trinary().