cprover
string_constraint.h File Reference

Defines string constraints. More...

Include dependency graph for string_constraint.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  string_constraintt
 

Universally quantified string constraint

More...
 
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_constrainttto_string_not_contains_constraint (const exprt &expr)
 
string_not_contains_constrainttto_string_not_contains_constraint (exprt &expr)
 

Detailed Description

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.

Function Documentation

◆ to_string() [1/2]

std::string to_string ( const string_constraintt expr)
inline

Used for debug printing.

Parameters
[in]nsnamespace for from_expr
[in]identifieridentifier for from_expr
[in]exprconstraint to render
Returns
rendered string

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().

◆ to_string() [2/2]

std::string to_string ( const string_not_contains_constraintt expr)
inline

◆ to_string_not_contains_constraint() [1/2]

const string_not_contains_constraintt& to_string_not_contains_constraint ( const exprt expr)
inline

◆ to_string_not_contains_constraint() [2/2]

string_not_contains_constraintt& to_string_not_contains_constraint ( exprt expr)
inline