cprover
|
#include "simplify_expr.h"
#include <cassert>
#include <algorithm>
#include "c_types.h"
#include "rational.h"
#include "simplify_expr_class.h"
#include "mp_arith.h"
#include "arith_tools.h"
#include "replace_expr.h"
#include "std_types.h"
#include "expr_util.h"
#include "std_expr.h"
#include "fixedbv.h"
#include "pointer_offset_size.h"
#include "rational_tools.h"
#include "config.h"
#include "base_type.h"
#include "namespace.h"
#include "threeval.h"
#include "pointer_predicates.h"
#include "prefix.h"
#include "byte_operators.h"
#include "bv_arithmetic.h"
#include "endianness_map.h"
#include "simplify_utils.h"
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 2384 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(), add_padding(), constant_propagator_domaint::ai_simplify(), build_full_lhs_rec(), build_goto_trace(), c_offsetof(), c_sizeof(), 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_sett::get_value_set(), value_set_fit::get_value_set(), value_set_fivrnst::get_value_set(), value_set_fivrt::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(), size_of_expr(), c_sizeoft::sizeof_rec(), symex_slice_by_tracet::slice_by_trace(), symex_slice_by_tracet::slice_SSA_steps(), goto_symext::symex_malloc(), 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 2389 of file simplify_expr.cpp.
References simplify_exprt::simplify().
Referenced by linkingt::adjust_object_type_rec(), ai_domain_baset::ai_simplify_lhs(), path_symex_statet::array_index_as_string(), path_symex_statet::array_theory(), constant_propagator_domaint::assign(), acceleration_utilst::assign_array(), path_symext::assign_rec(), constant_propagator_domaint::assign_rec(), interval_domaint::assume(), boolbvt::bv_get_unbounded_array(), custom_bitvector_analysist::check(), goto_program2codet::cleanup_code_ifthenelse(), boolbvt::convert_index(), path_searcht::drop_state(), path_symex_statet::expand_structs_and_arrays(), flatten_byte_extract(), 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(), list_calls_and_arguments(), taint_analysist::operator()(), path_symex_statet::read(), dereferencet::read_object(), cpp_typecheckt::reinterpret_typecast(), constant_propagator_ait::replace(), cpp_typecheckt::standard_conversion_pointer(), symex_bmct::symex_step(), constant_propagator_domaint::transform(), 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().