cprover
|
Defines string constraints. More...
#include "bv_refinement.h"
#include "string_refinement_invariant.h"
#include <util/format_expr.h>
#include <util/format_type.h>
#include <util/refined_string_type.h>
#include <util/string_expr.h>
#include <util/union_find_replace.h>
Go to the source code of this file.
Classes | |
class | string_constraintt |
Universally quantified string constraintMore... | |
class | string_not_contains_constraintt |
Constraints to encode non containement of strings. More... | |
Functions | |
std::string | to_string (const string_constraintt &expr) |
Used for debug printing. More... | |
std::string | to_string (const string_not_contains_constraintt &expr) |
Used for debug printing. More... | |
const string_not_contains_constraintt & | to_string_not_contains_constraint (const exprt &expr) |
string_not_contains_constraintt & | to_string_not_contains_constraint (exprt &expr) |
Defines string constraints.
These are formulas talking about strings. We implemented two forms of constraints: string_constraintt
are formulas of the form \(\forall univ\_var \in [lb,ub[. prem => body\), and not_contains_constraintt of the form: \(\forall x \in [lb,ub[. p(x) => \exists y \in [lb,ub[. s1[x+y] \ne s2[y]\).
Definition in file string_constraint.h.
|
inline |
Used for debug printing.
[in] | ns | namespace for from_expr |
[in] | identifier | identifier for from_expr |
[in] | expr | constraint to render |
Definition at line 117 of file string_constraint.h.
References string_constraintt::body, format(), string_constraintt::lower_bound, string_constraintt::univ_var, and string_constraintt::upper_bound.
Referenced by bv_pointerst::add_addr(), add_to_xml(), ansi_c_internal_additions(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), approximate_nondet_rec(), architecture_string(), bv_refinementt::approximationt::as_string(), as_string(), assign_parameter_names(), value_set_fit::assign_rec(), value_set_fivrnst::assign_rec(), value_set_fivrt::assign_rec(), value_sett::assign_rec(), banner_string(), symex_coveraget::build_cobertura(), build_function_environment(), goto_symext::build_symex_nondet(), string_abstractiont::build_unknown(), cpp_typecheckt::class_template_identifier(), goto_program2codet::cleanup_expr(), partial_order_concurrencyt::clock(), smt2_convt::collect_bindings(), convert(), java_bytecode_convert_classt::convert(), java_bytecode_convert_methodt::convert(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), convert_assert(), boolbvt::convert_case(), convert_character_literal(), boolbvt::convert_cond(), convert_decl(), convert_default(), boolbvt::convert_equality(), smt2_convt::convert_identifier(), boolbvt::convert_index(), convert_input(), java_bytecode_convert_methodt::convert_instructions(), symex_target_equationt::convert_io(), smt2_convt::convert_literal(), convert_output(), cpp_typecheckt::convert_parameter(), expr2ct::convert_rec(), java_bytecode_convert_methodt::convert_ret(), convert_return(), goto_convertt::convert_switch(), boolbvt::convert_verilog_case_equality(), cpp_internal_additions(), debug_check_axioms_step(), bv_refinementt::dec_solve(), linkingt::detailed_conflict_report_rec(), value_set_fit::do_end_function(), value_set_fivrnst::do_end_function(), value_set_fivrt::do_end_function(), java_bytecode_convert_methodt::do_exception_handling(), value_set_fit::do_function_call(), value_set_fivrnst::do_function_call(), value_set_fivrt::do_function_call(), value_sett::do_function_call(), bmct::do_language_agnostic_bmc(), do_prefix(), as_modet::doit(), aigt::dot_label(), xmlt::escape_attribute(), messaget::eval_verbosity(), find_closing_delimiter(), smt2_convt::find_symbols(), smt2_convt::find_symbols_rec(), call_grapht::format_callsites(), format_number_range(), acceleration_utilst::fresh_symbol(), generate_function_bodiest::generate_parameter_names(), new_scopet::get_anon_id(), document_propertiest::get_code(), smt2_parsert::get_fresh_id(), get_new_name(), get_temporary_file(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), value_sett::get_value_set_rec(), goto_program_coverage_recordt::goto_program_coverage_recordt(), cover_location_instrumentert::instrument(), cover_branch_instrumentert::instrument(), instrumentert::instrument_minimum_interference_inserter(), introduce_temporaries(), string_constraintt::is_valid_string_constraint(), java_build_arguments(), java_bytecode_initialize_parameter_names(), json(), aigt::label(), label_properties(), goto_symext::loop_bound_exceeded(), goto_programt::loop_id(), linker_script_merget::ls_data2instructions(), goto_symext::make_auto_object(), boolbvt::make_bv_expr(), cpp_scopest::new_block_scope(), memory_model_baset::nondet_bool_symbol(), configt::object_bits_info(), graphml_witnesst::operator()(), bmc_all_propertiest::operator()(), full_slicert::operator()(), bmc_covert::operator()(), dump_ct::operator()(), shared_bufferst::operator()(), grapht< abstract_eventt >::output_dot(), goto_difft::output_functions(), goto_inlinet::goto_inline_logt::output_inline_log_json(), dep_graph_domaint::output_json(), ai_baset::output_json(), goto_unwindt::unwind_logt::output_log_json(), ai_baset::output_xml(), pad(), pad_bit_field(), goto_symext::parameter_assignments(), goto_symext::phi_function(), pointer_logict::pointer_expr(), irept::pretty(), ui_message_handlert::print(), event_grapht::critical_cyclet::print(), event_grapht::critical_cyclet::print_detail(), event_grapht::critical_cyclet::print_output(), instrumentert::print_outputs(), cnft::process_clause(), qbf_skizzo_coret::prop_solve(), satcheck_zcoret::prop_solve(), satcheck_picosatt::prop_solve(), satcheck_lingelingt::prop_solve(), satcheck_zchaff_baset::prop_solve(), qbf_squolem_coret::prop_solve(), qbf_squolemt::prop_solve(), qbf_bdd_coret::prop_solve(), java_bytecode_parsert::rbytecode(), smt2_dect::read_result(), linkingt::rename(), partial_order_concurrencyt::rw_clock_id(), configt::set(), irept::set(), configt::ansi_ct::set_arch_spec_mips(), xmlt::set_attribute(), show_locations(), show_loop_ids(), show_loop_ids_json(), bmct::show_program(), smallest_unused_suffix(), stack_depth(), goto_symext::symex_allocate(), goto_symext::symex_cpp_new(), goto_symext::symex_gcc_builtin_va_arg_next(), Parser::SyntaxError(), java_bytecode_convert_methodt::tmp_variable(), smt2_convt::type2id(), type2name_symbol(), language_filest::typecheck(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_function_body(), cpp_typecheckt::typecheck_template_parameters(), shared_bufferst::unique(), goto_unwindt::unwind(), java_bytecode_convert_methodt::variable(), write_graphml(), and yyansi_cparse().
|
inline |
Used for debug printing.
[in] | ns | namespace for from_expr |
[in] | identifier | identifier for from_expr |
[in] | expr | constraint to render |
Definition at line 189 of file string_constraint.h.
References string_not_contains_constraintt::exists_lower_bound(), string_not_contains_constraintt::exists_upper_bound(), format(), string_not_contains_constraintt::premise(), string_not_contains_constraintt::s0(), string_not_contains_constraintt::s1(), string_not_contains_constraintt::univ_lower_bound(), and string_not_contains_constraintt::univ_upper_bound().
|
inline |
Definition at line 202 of file string_constraint.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), PRECONDITION, and string_refinement_invariantt.
|
inline |
Definition at line 213 of file string_constraint.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), PRECONDITION, and string_refinement_invariantt.