24#include <unordered_set>
68 const std::function<
exprt(
const exprt &)> &get,
71 bool use_counter_example,
73 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
74 ¬_contain_witnesses);
96 const std::vector<exprt> ¤t_constraints);
101 const exprt &formula);
106 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
110 const std::function<
exprt(
const exprt &)> &super_get,
119 const bool left_propagate);
132 std::vector<T> result;
133 if(!index_value.empty())
135 result.resize(index_value.rbegin()->first + 1);
136 for(
auto it = index_value.rbegin(); it != index_value.rend(); ++it)
138 const std::size_t index = it->first;
139 const T &value = it->second;
140 const auto next = std::next(it);
141 const std::size_t leftmost_index_to_pad =
142 next != index_value.rend() ? next->first + 1 : 0;
143 for(std::size_t j = leftmost_index_to_pad; j <= index; j++)
160 loop_bound_(info.refinement_bound),
174 std::size_t count = 0;
175 std::size_t count_current = 0;
178 const exprt &s = i.first;
181 for(
const auto &j : i.second)
183 const auto it = index_set.
current.find(i.first);
185 it != index_set.
current.end() && it->second.find(j) != it->second.end())
195 stream << count <<
" elements in index set (" << count_current
223 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
224 ¬_contain_witnesses)
226 std::vector<exprt> lemmas;
227 for(
const auto &i : index_set.
current)
229 for(
const auto &univ_axiom : axioms.
universal)
231 for(
const auto &j : i.second)
232 lemmas.push_back(
instantiate(univ_axiom, i.first, j));
237 for(
const auto &instance :
238 instantiate(nc_axiom, index_set, not_contain_witnesses))
239 lemmas.push_back(instance);
251 if(
const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr))
254 const auto fun_app = expr_try_dynamic_cast<function_application_exprt>(
257 const auto new_equation =
303 const std::vector<exprt> &equations,
307 const std::string log_message =
308 "WARNING string_refinement.cpp generate_symbol_resolution_from_equations:";
309 auto equalities =
make_range(equations).filter(
311 for(
const exprt &e : equalities)
316 if(lhs.
id() != ID_symbol)
318 stream << log_message <<
"non symbol lhs: " <<
format(lhs)
325 stream << log_message <<
"non equal types lhs: " <<
format(lhs)
326 <<
"\n####################### rhs: " <<
format(rhs)
335 else if(rhs.
id() == ID_function_application)
343 if(rhs.
type().
id() == ID_struct || rhs.
type().
id() == ID_struct_tag)
346 for(
const auto &comp : struct_type.
components())
359 stream << log_message <<
"non struct with char pointer subexpr "
373static std::vector<exprt>
376 std::vector<exprt> result;
378 result.push_back(lhs);
379 else if(lhs.
type().
id() == ID_struct || lhs.
type().
id() == ID_struct_tag)
382 for(
const auto &comp : struct_type.
components())
387 result.end(), strings_in_comp.begin(), strings_in_comp.end());
398static std::vector<exprt>
401 std::vector<exprt> result;
406 result.push_back(*it);
407 it.next_sibling_or_parent();
409 else if(it->id() == ID_symbol)
413 it.next_sibling_or_parent();
444 for(
const auto &comp : struct_type.
components())
450 equal_exprt(lhs_data, rhs_data), symbol_resolve, ns);
464 const std::vector<equal_exprt> &equations,
468 const std::string log_message =
469 "WARNING string_refinement.cpp "
470 "string_identifiers_resolution_from_equations:";
475 std::unordered_set<size_t> required_equations;
476 std::stack<size_t> equations_to_treat;
478 for(std::size_t i = 0; i < equations.size(); ++i)
481 if(eq.
rhs().
id() == ID_function_application)
483 if(required_equations.insert(i).second)
484 equations_to_treat.push(i);
487 for(
const auto &expr : rhs_strings)
488 equation_map.
add(i, expr);
496 for(
const auto &expr : lhs_strings)
497 equation_map.
add(i, expr);
499 if(lhs_strings.empty())
501 stream << log_message <<
"non struct with string subtype "
507 equation_map.
add(i, expr);
512 while(!equations_to_treat.empty())
514 const std::size_t i = equations_to_treat.top();
515 equations_to_treat.pop();
520 if(required_equations.insert(j).second)
521 equations_to_treat.push(j);
527 for(
const std::size_t i : required_equations)
536output_equations(std::ostream &output,
const std::vector<exprt> &equations)
538 for(std::size_t i = 0; i < equations.size(); ++i)
539 output <<
" [" << i <<
"] " <<
format(equations[i]) << std::endl;
614 log.
debug() <<
"dec_solve: Build symbol solver from equations"
630 std::vector<equal_exprt> equalities;
633 if(
auto equal_expr = expr_try_dynamic_cast<equal_exprt>(eq))
634 equalities.push_back(*equal_expr);
642 for(
const auto &pair : string_id_symbol_resolve.
to_vector())
649 log.
debug() <<
"dec_solve: Replacing string ids and simplifying arguments"
650 " in function applications"
654 auto it = expr.depth_begin();
655 while(it != expr.depth_end())
665 it.next_sibling_or_parent();
681 log.
debug() <<
"dec_solve: compute dependency graph and remove function "
682 <<
"applications captured by the dependencies:" <<
messaget::eom;
683 std::vector<exprt> local_equations;
688 const exprt eq_with_char_array_replaced_with_representative_elements =
692 eq_with_char_array_replaced_with_representative_elements,
696 local_equations.push_back(*new_equation);
698 local_equations.push_back(eq);
718 <<
format(pair.second) <<
" : " <<
format(pair.second.type())
723 for(
const auto &eq : local_equations)
736 constraint.replace_expr(symbol_resolve);
738 is_valid_string_constraint(log.error(), ns, constraint),
739 string_refinement_invariantt(
740 "string constraints satisfy their invariant"));
749 replace(symbol_resolve, axiom);
754 std::unordered_map<string_not_contains_constraintt, symbol_exprt>
755 not_contain_witnesses;
758 const auto &witness_type = [&] {
763 not_contain_witnesses.emplace(
781 const auto get = [
this](
const exprt &expr) {
return this->
get(expr); };
787 std::vector<exprt> counter_examples;
796 not_contain_witnesses);
802 log.
debug() <<
"check_SAT: got SAT but the model is not correct"
808 return initial_result;
814 const auto initial_instances =
816 for(
const auto &instance : initial_instances)
829 std::vector<exprt> counter_examples;
838 not_contain_witnesses);
846 <<
"check_SAT: got SAT but the model is not correct, refining..."
862 log.
error() <<
"dec_solve: current index set is empty, "
868 log.
debug() <<
"dec_solve: current index set is empty, "
870 for(
const auto &counter : counter_examples)
875 const auto instances =
877 for(
const auto &instance : instances)
883 log.
debug() <<
"check_SAT: default return "
885 return refined_result;
888 log.
debug() <<
"string_refinementt::dec_solve reached the maximum number"
898 const bool simplify_lemma)
905 exprt simple_lemma = lemma;
925 if(it->id() == ID_array && it->operands().empty())
931 it.next_sibling_or_parent();
957 const std::function<
exprt(
const exprt &)> &super_get,
965 if(size_from_pool.has_value())
967 const exprt size = size_from_pool.value();
969 if(size_val.
id() != ID_constant)
971 stream <<
"(sr::get_valid_array_size) string of unknown size: "
981 auto n_opt = numeric_cast<std::size_t>(size_val);
984 stream <<
"(sr::get_valid_array_size) size is not valid" <<
messaget::eom;
1001 const std::function<
exprt(
const exprt &)> &super_get,
1009 if(!size.has_value())
1014 const size_t n = numeric_cast<std::size_t>(size.value()).value();
1018 stream <<
"(sr::get_valid_array_size) long string (size "
1020 stream <<
"(sr::get_valid_array_size) consider reducing "
1021 "max-nondet-string-length so "
1022 "that no string exceeds "
1024 <<
" in length and "
1025 "make sure all functions returning strings are loaded"
1027 stream <<
"(sr::get_valid_array_size) this can also happen on invalid "
1050 if(arr.
type().
id() != ID_array)
1051 return std::string(
"");
1067 const std::function<
exprt(
const exprt &)> &super_get,
1073 stream <<
"- " <<
format(arr) <<
":\n";
1074 stream << std::string(4,
' ') <<
"- type: " <<
format(arr.
type())
1076 const auto arr_model_opt =
get_array(super_get, ns, stream, arr, array_pool);
1079 stream << std::string(4,
' ') <<
"- char_array: " <<
format(*arr_model_opt)
1081 stream << std::string(4,
' ')
1084 stream << std::string(4,
' ')
1087 const auto concretized_array =
get_array(
1090 stream << std::string(4,
' ')
1091 <<
"- concretized_char_array: " <<
format(*concretized_array)
1095 const auto array_expr =
1096 expr_try_dynamic_cast<array_exprt>(*concretized_array))
1098 stream << std::string(4,
' ') <<
"- as_string: \""
1102 stream << std::string(2,
' ') <<
"- warning: not an array"
1104 return *concretized_array;
1108 stream << std::string(4,
' ') <<
"- incomplete model" <<
messaget::eom;
1118 const std::function<
exprt(
const exprt &)> &super_get,
1119 const std::vector<symbol_exprt> &symbols,
1122 stream <<
"debug_model:" <<
'\n';
1125 const auto arr = pointer_array.second;
1129 stream <<
"- " <<
format(arr) <<
":\n"
1130 <<
" - pointer: " <<
format(pointer_array.first) <<
"\n"
1134 for(
const auto &symbol : symbols)
1136 stream <<
" - " << symbol.get_identifier() <<
": "
1137 <<
format(super_get(symbol)) <<
'\n';
1157 const bool left_propagate)
1175 const exprt default_val = symbol_generator(
"out_of_bound_access",
char_type);
1184 const bool left_propagate)
1197 substituted_true_case ? *substituted_true_case : true_index,
1198 substituted_false_case ? *substituted_false_case : false_index);
1204 const bool left_propagate)
1207 if(
auto array_of = expr_try_dynamic_cast<array_of_exprt>(array))
1208 return array_of->op();
1209 if(
auto array_with = expr_try_dynamic_cast<with_exprt>(array))
1211 *array_with, index_expr.
index(), left_propagate);
1212 if(
auto array_expr = expr_try_dynamic_cast<array_exprt>(array))
1214 *array_expr, index_expr.
index(), symbol_generator);
1215 if(
auto if_expr = expr_try_dynamic_cast<if_exprt>(array))
1217 *if_expr, index_expr.
index(), symbol_generator, left_propagate);
1220 array.
is_nil() || array.
id() == ID_symbol || array.
id() == ID_nondet_symbol,
1222 "in case the array is unknown, it should be a symbol or nil, id: ") +
1233 const bool left_propagate)
1238 if(
const auto index_expr = expr_try_dynamic_cast<index_exprt>(*it))
1245 it.mutate() = *result;
1272 const bool left_propagate)
1291 const std::function<
exprt(
const exprt &)> &get)
1294 const auto lbe = numeric_cast_v<mp_integer>(
1296 const auto ube = numeric_cast_v<mp_integer>(
1310 std::vector<exprt> conjuncts;
1311 conjuncts.reserve(numeric_cast_v<std::size_t>(ube - lbe));
1315 const exprt s0_char =
1318 conjuncts.push_back(
equal_exprt(s0_char, s1_char));
1328template <
typename T>
1332 const T &axiom_in_model,
1333 const exprt &negaxiom,
1334 const exprt &with_concretized_arrays)
1336 stream << std::string(4,
' ') <<
"- axiom:\n" << std::string(6,
' ');
1339 << std::string(4,
' ') <<
"- axiom_in_model:\n"
1340 << std::string(6,
' ');
1341 stream <<
to_string(axiom_in_model) <<
'\n'
1342 << std::string(4,
' ') <<
"- negated_axiom:\n"
1343 << std::string(6,
' ') <<
format(negaxiom) <<
'\n';
1344 stream << std::string(4,
' ') <<
"- negated_axiom_with_concretized_arrays:\n"
1345 << std::string(6,
' ') <<
format(with_concretized_arrays) <<
'\n';
1352 const std::function<
exprt(
const exprt &)> &get,
1355 bool use_counter_example,
1357 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1358 ¬_contain_witnesses)
1360 stream <<
"string_refinementt::check_axioms:" <<
messaget::eom;
1363 auto pairs = symbol_resolve.
to_vector();
1364 for(
const auto &pair : pairs)
1365 stream <<
" - " <<
format(pair.first) <<
" --> " <<
format(pair.second)
1379 std::map<size_t, exprt> violated;
1381 stream <<
"string_refinement::check_axioms: " << axioms.
universal.size()
1383 for(
size_t i = 0; i < axioms.
universal.size(); i++)
1395 stream << std::string(2,
' ') << i <<
".\n";
1396 const exprt with_concretized_arrays =
1399 stream, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
1404 with_concretized_arrays,
1408 stream << std::string(4,
' ')
1411 violated[i] = *witness;
1414 stream << std::string(4,
' ') <<
"- correct" <<
messaget::eom;
1418 std::map<std::size_t, exprt> violated_not_contains;
1420 stream <<
"there are " << axioms.
not_contains.size() <<
" not_contains axioms"
1422 for(std::size_t i = 0; i < axioms.
not_contains.size(); i++)
1428 nc_axiom, univ_var, [&](
const exprt &expr) {
1432 stream << std::string(2,
' ') << i <<
".\n";
1434 stream, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
1440 stream << std::string(4,
' ')
1443 violated_not_contains[i] = *witness;
1447 if(violated.empty() && violated_not_contains.empty())
1450 return {
true, std::vector<exprt>()};
1454 stream << violated.size() <<
" universal string axioms can be violated"
1456 stream << violated_not_contains.size()
1457 <<
" not_contains string axioms can be violated" <<
messaget::eom;
1459 if(use_counter_example)
1461 std::vector<exprt> lemmas;
1463 for(
const auto &v : violated)
1465 const exprt &val = v.second;
1476 lemmas.push_back(counter);
1479 for(
const auto &v : violated_not_contains)
1481 const exprt &val = v.second;
1485 const exprt func_val =
1486 index_exprt(not_contain_witnesses.at(axiom), val);
1489 std::set<std::pair<exprt, exprt>> indices;
1490 indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
1491 const exprt counter =
1493 lemmas.push_back(counter);
1495 return {
false, lemmas};
1498 return {
false, std::vector<exprt>()};
1518 for(
const auto &axiom : axioms.
universal)
1531 const std::vector<exprt> ¤t_constraints)
1533 for(
const auto &axiom : current_constraints)
1545 if(array_expr.
id() == ID_if)
1552 if(array_expr.
type().
id() == ID_array)
1555 accu.push_back(array_expr);
1559 for(
const auto &operand : array_expr.
operands())
1577 const bool is_size_t = numeric_cast<std::size_t>(i).has_value();
1578 if(i.
id() != ID_constant || is_size_t)
1580 std::vector<exprt> sub_arrays;
1582 for(
const auto &sub : sub_arrays)
1583 if(index_set.
cumulative[sub].insert(i).second)
1584 index_set.
current[sub].insert(i);
1607 const exprt &upper_bound,
1612 s.
id() == ID_symbol || s.
id() == ID_nondet_symbol || s.
id() == ID_array ||
1614 if(s.
id() == ID_array)
1616 for(std::size_t j = 0; j < s.
operands().size(); ++j)
1620 if(
auto ite = expr_try_dynamic_cast<if_exprt>(s))
1646 const auto &s = index_expr.array();
1648 it.next_sibling_or_parent();
1672 it.next_sibling_or_parent();
1690 const exprt &formula)
1692 std::list<exprt> to_process;
1693 to_process.push_back(formula);
1695 while(!to_process.empty())
1697 exprt cur = to_process.back();
1698 to_process.pop_back();
1704 s.
type().
id() == ID_array,
1707 if(s.
id() != ID_array)
1713 to_process.push_back(*it);
1739 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1746 const auto &index_set1 = index_set.
cumulative.find(
s1.content());
1747 const auto ¤t_index_set0 = index_set.
current.find(s0.
content());
1748 const auto ¤t_index_set1 = index_set.
current.find(
s1.content());
1753 current_index_set0 != index_set.
current.end() &&
1754 current_index_set1 != index_set.
current.end())
1756 typedef std::pair<exprt, exprt> expr_pairt;
1757 std::set<expr_pairt> index_pairs;
1759 for(
const auto &ic0 : current_index_set0->second)
1760 for(
const auto &i1 : index_set1->second)
1761 index_pairs.insert(expr_pairt(ic0, i1));
1762 for(
const auto &ic1 : current_index_set1->second)
1763 for(
const auto &i0 : index_set0->second)
1764 index_pairs.insert(expr_pairt(i0, ic1));
1766 return ::instantiate_not_contains(axiom, index_pairs, witnesses);
1780 for(
auto &operand : expr.
operands())
1783 if(expr.
id() == ID_array_list)
1793 for(
size_t i = 0; i < expr.
operands().size(); i += 2)
1797 const auto index_value = numeric_cast<std::size_t>(index);
1800 (index_value && *index_value < string_max_length))
1801 ret_expr =
with_exprt(ret_expr, index, value);
1818 const auto super_get = [
this](
const exprt &expr) {
1825 const auto &index_expr = expr_try_dynamic_cast<index_exprt>(ecopy);
1828 std::reference_wrapper<const exprt> current(index_expr->array());
1829 while(current.get().id() == ID_if)
1831 const auto &if_expr = expr_dynamic_cast<if_exprt>(current.get());
1832 const exprt cond =
get(if_expr.cond());
1834 current = std::cref(if_expr.true_case());
1836 current = std::cref(if_expr.false_case());
1841 const auto index =
get(index_expr->index());
1848 const exprt unknown =
1853 if(
const auto index_value = numeric_cast<std::size_t>(index))
1854 return sparse_array->at(*index_value);
1855 return sparse_array->to_if_expression(index);
1858 INVARIANT(array.id() == ID_symbol || array.id() == ID_nondet_symbol,
1859 "Apart from symbols, array valuations can be interpreted as "
1860 "sparse arrays. Array model : " + array.pretty());
1869 const auto from_dependencies =
1871 return *from_dependencies;
1874 const auto arr_model_opt =
1876 return *arr_model_opt;
1879 const auto &length_from_pool =
1882 const exprt length = super_get(length_from_pool.value());
1884 if(
const auto n = numeric_cast<std::size_t>(length))
1911 satcheck_no_simplifiert sat_check(message_handler);
1932 [&](
const exprt &expr)
1934 const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
1936 indices[index_expr->array()].push_back(index_expr->index());
1953 it->id() != ID_plus && it->id() != ID_minus &&
1954 it->id() != ID_unary_minus && *it != var)
1956 if(std::find(it->depth_begin(), it->depth_end(), var) != it->depth_end())
1959 it.next_sibling_or_parent();
1980 if(it->id() == ID_index)
1981 it.next_sibling_or_parent();
2002 for(
const auto &pair : body_indices)
2005 const exprt rep = pair.second.back();
2006 for(
size_t j = 0; j < pair.second.size() - 1; j++)
2008 const exprt i = pair.second[j];
2013 stream <<
"Indices not equal: " <<
to_string(constraint)
2020 if(!is_linear_arithmetic_expr(rep, constraint.
univ_var))
2022 stream <<
"f is not linear: " <<
to_string(constraint)
2029 if(!universal_only_in_index(constraint))
2031 stream <<
"Universal variable outside of index:" <<
to_string(constraint)
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
bitvector_typet index_type()
bitvector_typet char_type()
Array constructor from list of elements.
const array_typet & type() const
Array constructor from single element.
Correspondance between arrays and pointers string representations.
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
optionalt< exprt > get_length_if_exists(const array_string_exprt &s) const
As opposed to get_length(), do not create a new symbol if the length of the array_string_exprt does n...
const std::unordered_map< array_string_exprt, exprt, irep_hash > & created_strings() const
Return a map mapping all array_string_exprt of the array_pool to their length.
const typet & length_type() const
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
A base class for relations, i.e., binary predicates whose two operands have the same type.
decision_proceduret::resultt dec_solve() override
Run the decision procedure to solve the problem.
A constant literal expression.
resultt
Result of running the decision procedure.
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
virtual void set_to(const exprt &expr, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Maps equation to expressions contained in them and conversely expressions to equations that contain t...
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
std::vector< std::size_t > find_equations(const exprt &expr)
std::vector< exprt > find_expressions(const std::size_t i)
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
depth_iteratort depth_end()
depth_iteratort depth_begin()
bool is_false() const
Return whether the expression is a constant representing false.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
The trinary if-then-else operator.
An expression denoting infinity.
Represents arrays by the indexes up to which the value remains the same.
exprt to_if_expression(const exprt &index) const
static optionalt< interval_sparse_arrayt > of_expr(const exprt &expr, const exprt &extra_value)
If the expression is an array_exprt or a with_exprt uses the appropriate constructor,...
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
const irep_idt & id() const
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given...
Extract member of struct or union.
message_handlert & get_message_handler()
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The plus expression Associativity is not specified.
bool equality_propagation
void l_set_to_true(literalt a)
static exprt to_if_expression(const with_exprt &expr, const exprt &index)
Creates an if_expr corresponding to the result of accessing the array at the given index.
optionalt< exprt > make_array_pointer_association(const exprt &return_code, const function_application_exprt &expr)
Associate array to pointer, and array to length.
symbol_generatort fresh_symbol
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
Checks the data invariant for string_constraintt.
exprt univ_within_bounds() const
static array_index_mapt gather_indices(const exprt &expr)
static bool universal_only_in_index(const string_constraintt &constr)
The universally quantified variable is only allowed to occur in index expressions in the body of a st...
static bool is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
std::map< exprt, std::vector< exprt > > array_index_mapt
void output_dot(std::ostream &stream) const
void clean_cache()
Clean the cache used by eval
NODISCARD string_constraintst add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
optionalt< exprt > eval(const array_string_exprt &s, const std::function< exprt(const exprt &)> &get_value) const
Attempt to evaluate the given string from the dependencies and valuation of strings on which it depen...
string_constraint_generatort generator
union_find_replacet symbol_resolve
std::vector< exprt > equations
string_refinementt(const infot &)
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
std::set< exprt > seen_instances
void set_to(const exprt &expr, bool value) override
Record the constraints to ensure that the expression is true when the boolean is true and false other...
string_dependenciest dependencies
index_set_pairt index_sets
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
std::vector< exprt > current_constraints
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
Structure type, corresponds to C style structs.
const componentst & components() const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
Generation of fresh symbols of a given type.
const typet & subtype() const
The type of an expression, extends irept.
const typet & subtype() const
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
std::vector< std::pair< exprt, exprt > > to_vector() const
exprt make_union(const exprt &a, const exprt &b)
Merge the set containing a and the set containing b.
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by the representative element of the set they belong to.
Operator to update elements in structs and arrays.
#define forall_operands(it, expr)
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Magic numbers used throughout the codebase.
const std::size_t MAX_CONCRETE_STRING_SIZE
bool can_cast_expr< function_application_exprt >(const exprt &base)
nonstd::optional< T > optionalt
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
int solver(std::istream &in)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
bool can_cast_expr< equal_exprt >(const exprt &base)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
#define CHARACTER_FOR_UNKNOWN
Module: String solver Author: Diffblue Ltd.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
Defines related function for string constraints.
std::vector< exprt > instantiate_not_contains(const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt > > &index_pairs, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)
optionalt< exprt > add_node(string_dependenciest &dependencies, const exprt &expr, array_poolt &array_pool, symbol_generatort &fresh_symbol)
When a sub-expression of expr is a builtin_function, add a "string_builtin_function" node to the grap...
Keeps track of dependencies between strings.
array_string_exprt & to_array_string_expr(exprt &expr)
static void initial_index_set(index_set_pairt &index_set, const namespacet &ns, const string_constraintt &axiom)
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
static std::string string_of_array(const array_exprt &arr)
convert the content of a string to a more readable representation.
static void update_index_set(index_set_pairt &index_set, const namespacet &ns, const std::vector< exprt > ¤t_constraints)
Add to the index set all the indices that appear in the formulas.
static optionalt< exprt > get_array(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr, const array_poolt &array_pool)
Get a model of an array and put it in a certain form.
static std::vector< exprt > extract_strings_from_lhs(const exprt &lhs, const namespacet &ns)
This is meant to be used on the lhs of an equation with string subtype.
exprt substitute_array_lists(exprt expr, size_t string_max_length)
Replace array-lists by 'with' expressions.
static std::vector< exprt > extract_strings(const exprt &expr, const namespacet &ns)
static std::pair< bool, std::vector< exprt > > check_axioms(const string_axiomst &axioms, string_constraint_generatort &generator, const std::function< exprt(const exprt &)> &get, messaget::mstreamt &stream, const namespacet &ns, bool use_counter_example, const union_find_replacet &symbol_resolve, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > ¬_contain_witnesses)
Check axioms takes the model given by the underlying solver and answers whether it satisfies the stri...
static void add_equations_for_symbol_resolution(union_find_replacet &symbol_solver, const std::vector< exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Add association for each char pointer in the equation.
static void make_char_array_pointer_associations(string_constraint_generatort &generator, exprt &expr)
If expr is an equation whose right-hand-side is a associate_array_to_pointer call,...
static void add_string_equation_to_symbol_resolution(const equal_exprt &eq, union_find_replacet &symbol_resolve, const namespacet &ns)
Given an equation on strings, mark these strings as belonging to the same set in the symbol_resolve s...
static bool validate(const string_refinementt::infot &info)
static void add_to_index_set(index_set_pairt &index_set, const namespacet &ns, const exprt &s, exprt i)
Add i to the index set all the indices that appear in the formula.
exprt simplify_sum(const exprt &f)
static optionalt< exprt > get_valid_array_size(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr, const array_poolt &array_pool)
Get a model of the size of the input string.
union_find_replacet string_identifiers_resolution_from_equations(const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Symbol resolution for expressions of type string typet.
static void display_index_set(messaget::mstreamt &stream, const index_set_pairt &index_set)
Write index set to the given stream, use for debugging.
static std::vector< T > fill_in_map_as_vector(const std::map< std::size_t, T > &index_value)
Convert index-value map to a vector of values.
static exprt negation_of_not_contains_constraint(const string_not_contains_constraintt &constraint, const symbol_exprt &univ_var, const std::function< exprt(const exprt &)> &get)
Negates the constraint to be fed to a solver.
static optionalt< exprt > find_counter_example(const namespacet &ns, const exprt &axiom, const symbol_exprt &var, message_handlert &message_handler)
Creates a solver with axiom as the only formula added and runs it.
static exprt replace_expr_copy(const union_find_replacet &symbol_resolve, exprt expr)
Substitute sub-expressions in equation by representative elements of symbol_resolve whenever possible...
static void substitute_array_access_in_place(exprt &expr, symbol_generatort &symbol_generator, const bool left_propagate)
Auxiliary function for substitute_array_access Performs the same operation but modifies the argument ...
static void get_sub_arrays(const exprt &array_expr, std::vector< exprt > &accu)
An expression representing an array of characters can be in the form of an if expression for instance...
void debug_model(const string_constraint_generatort &generator, messaget::mstreamt &stream, const namespacet &ns, const std::function< exprt(const exprt &)> &super_get, const std::vector< symbol_exprt > &symbols, array_poolt &array_pool)
Display part of the current model by mapping the variables created by the solver to constant expressi...
static std::vector< exprt > instantiate(const string_not_contains_constraintt &axiom, const index_set_pairt &index_set, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
static optionalt< exprt > substitute_array_access(const index_exprt &index_expr, symbol_generatort &symbol_generator, const bool left_propagate)
static void debug_check_axioms_step(messaget::mstreamt &stream, const T &axiom, const T &axiom_in_model, const exprt &negaxiom, const exprt &with_concretized_arrays)
Debugging function which outputs the different steps an axiom goes through to be checked in check axi...
static exprt get_char_array_and_concretize(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr, array_poolt &array_pool)
Debugging function which finds the valuation of the given array in super_get and concretize unknown c...
static std::vector< exprt > generate_instantiations(const index_set_pairt &index_set, const string_axiomst &axioms, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > ¬_contain_witnesses)
Instantiation of all constraints.
String support via creating string constraints and progressively instantiating the universal constrai...
exprt substitute_array_access(exprt expr, symbol_generatort &symbol_generator, const bool left_propagate)
Create an equivalent expression where array accesses and 'with' expressions are replaced by 'if' expr...
union_find_replacet string_identifiers_resolution_from_equations(const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Symbol resolution for expressions of type string typet.
#define string_refinement_invariantt(reason)
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
std::map< exprt, std::set< exprt > > current
std::map< exprt, std::set< exprt > > cumulative
std::vector< string_constraintt > universal
std::vector< string_not_contains_constraintt > not_contains
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< string_not_contains_constraintt > not_contains
std::vector< exprt > existential
std::vector< string_constraintt > universal
Constraints to encode non containement of strings.
string_refinementt constructor arguments