Go to the documentation of this file.
26 #include <unordered_set>
67 const std::function<
exprt(
const exprt &)> &get,
70 bool use_counter_example,
72 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
73 ¬_contain_witnesses);
95 const std::vector<exprt> ¤t_constraints);
100 const exprt &formula);
105 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
109 const std::function<
exprt(
const exprt &)> &super_get,
118 const bool left_propagate);
127 template <
typename T>
128 static std::vector<T>
131 std::vector<T> result;
132 if(!index_value.empty())
134 result.resize(index_value.rbegin()->first + 1);
135 for(
auto it = index_value.rbegin(); it != index_value.rend(); ++it)
137 const std::size_t index = it->first;
138 const T &value = it->second;
139 const auto next = std::next(it);
140 const std::size_t leftmost_index_to_pad =
141 next != index_value.rend() ? next->first + 1 : 0;
142 for(std::size_t j = leftmost_index_to_pad; j <= index; j++)
159 loop_bound_(info.refinement_bound),
173 std::size_t count = 0;
174 std::size_t count_current = 0;
177 const exprt &s = i.first;
180 for(
const auto &j : i.second)
182 const auto it = index_set.
current.find(i.first);
184 it != index_set.
current.end() && it->second.find(j) != it->second.end())
194 stream << count <<
" elements in index set (" << count_current
222 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
223 ¬_contain_witnesses)
225 std::vector<exprt> lemmas;
226 for(
const auto &i : index_set.
current)
228 for(
const auto &univ_axiom : axioms.
universal)
230 for(
const auto &j : i.second)
231 lemmas.push_back(
instantiate(univ_axiom, i.first, j));
236 for(
const auto &instance :
237 instantiate(nc_axiom, index_set, not_contain_witnesses))
238 lemmas.push_back(instance);
250 if(
const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr))
253 const auto fun_app = expr_try_dynamic_cast<function_application_exprt>(
256 const auto new_equation =
302 const std::vector<exprt> &equations,
306 const std::string log_message =
307 "WARNING string_refinement.cpp generate_symbol_resolution_from_equations:";
308 auto equalities =
make_range(equations).filter(
310 for(
const exprt &e : equalities)
315 if(lhs.
id() != ID_symbol)
317 stream << log_message <<
"non symbol lhs: " <<
format(lhs)
324 stream << log_message <<
"non equal types lhs: " <<
format(lhs)
325 <<
"\n####################### rhs: " <<
format(rhs)
334 else if(rhs.
id() == ID_function_application)
342 if(rhs.
type().
id() == ID_struct || rhs.
type().
id() == ID_struct_tag)
345 for(
const auto &comp : struct_type.
components())
358 stream << log_message <<
"non struct with char pointer subexpr "
372 static std::vector<exprt>
375 std::vector<exprt> result;
377 result.push_back(lhs);
378 else if(lhs.
type().
id() == ID_struct || lhs.
type().
id() == ID_struct_tag)
381 for(
const auto &comp : struct_type.
components())
386 result.end(), strings_in_comp.begin(), strings_in_comp.end());
397 static std::vector<exprt>
400 std::vector<exprt> result;
405 result.push_back(*it);
406 it.next_sibling_or_parent();
408 else if(it->id() == ID_symbol)
412 it.next_sibling_or_parent();
443 for(
const auto &comp : struct_type.
components())
449 equal_exprt(lhs_data, rhs_data), symbol_resolve, ns);
463 const std::vector<equal_exprt> &equations,
467 const std::string log_message =
468 "WARNING string_refinement.cpp "
469 "string_identifiers_resolution_from_equations:";
474 std::unordered_set<size_t> required_equations;
475 std::stack<size_t> equations_to_treat;
477 for(std::size_t i = 0; i < equations.size(); ++i)
480 if(eq.
rhs().
id() == ID_function_application)
482 if(required_equations.insert(i).second)
483 equations_to_treat.push(i);
486 for(
const auto &expr : rhs_strings)
487 equation_map.
add(i, expr);
495 for(
const auto &expr : lhs_strings)
496 equation_map.
add(i, expr);
498 if(lhs_strings.empty())
500 stream << log_message <<
"non struct with string subtype "
506 equation_map.
add(i, expr);
511 while(!equations_to_treat.empty())
513 const std::size_t i = equations_to_treat.top();
514 equations_to_treat.pop();
519 if(required_equations.insert(j).second)
520 equations_to_treat.push(j);
526 for(
const std::size_t i : required_equations)
535 output_equations(std::ostream &output,
const std::vector<exprt> &equations)
537 for(std::size_t i = 0; i < equations.size(); ++i)
538 output <<
" [" << i <<
"] " <<
format(equations[i]) << std::endl;
613 log.
debug() <<
"dec_solve: Build symbol solver from equations"
629 std::vector<equal_exprt> equalities;
632 if(
auto equal_expr = expr_try_dynamic_cast<equal_exprt>(eq))
633 equalities.push_back(*equal_expr);
641 for(
const auto &pair : string_id_symbol_resolve.
to_vector())
648 log.
debug() <<
"dec_solve: Replacing string ids and simplifying arguments"
649 " in function applications"
653 auto it = expr.depth_begin();
654 while(it != expr.depth_end())
664 it.next_sibling_or_parent();
680 log.
debug() <<
"dec_solve: compute dependency graph and remove function "
681 <<
"applications captured by the dependencies:" <<
messaget::eom;
682 std::vector<exprt> local_equations;
687 const exprt eq_with_char_array_replaced_with_representative_elements =
691 eq_with_char_array_replaced_with_representative_elements,
695 local_equations.push_back(*new_equation);
697 local_equations.push_back(eq);
717 <<
format(pair.second) <<
" : " <<
format(pair.second.type())
722 for(
const auto &eq : local_equations)
735 constraint.replace_expr(symbol_resolve);
737 is_valid_string_constraint(log.error(), ns, constraint),
738 string_refinement_invariantt(
739 "string constraints satisfy their invariant"));
748 replace(symbol_resolve, axiom);
753 std::unordered_map<string_not_contains_constraintt, symbol_exprt>
754 not_contain_witnesses;
757 const auto &witness_type = [&] {
762 not_contain_witnesses.emplace(
780 const auto get = [
this](
const exprt &expr) {
return this->
get(expr); };
786 std::vector<exprt> counter_examples;
795 not_contain_witnesses);
801 log.
debug() <<
"check_SAT: got SAT but the model is not correct"
807 return initial_result;
813 const auto initial_instances =
815 for(
const auto &instance : initial_instances)
828 std::vector<exprt> counter_examples;
837 not_contain_witnesses);
845 <<
"check_SAT: got SAT but the model is not correct, refining..."
861 log.
error() <<
"dec_solve: current index set is empty, "
867 log.
debug() <<
"dec_solve: current index set is empty, "
869 for(
const auto &counter : counter_examples)
874 const auto instances =
876 for(
const auto &instance : instances)
882 log.
debug() <<
"check_SAT: default return "
884 return refined_result;
887 log.
debug() <<
"string_refinementt::dec_solve reached the maximum number"
897 const bool simplify_lemma)
904 exprt simple_lemma = lemma;
924 if(it->id() == ID_array && it->operands().empty())
929 it.next_sibling_or_parent();
955 const std::function<
exprt(
const exprt &)> &super_get,
963 if(size_from_pool.has_value())
965 const exprt size = size_from_pool.value();
967 if(size_val.
id() != ID_constant)
969 stream <<
"(sr::get_valid_array_size) string of unknown size: "
979 auto n_opt = numeric_cast<std::size_t>(size_val);
982 stream <<
"(sr::get_valid_array_size) size is not valid" <<
messaget::eom;
999 const std::function<
exprt(
const exprt &)> &super_get,
1007 if(!size.has_value())
1012 const size_t n = numeric_cast<std::size_t>(size.value()).value();
1016 stream <<
"(sr::get_valid_array_size) long string (size "
1018 stream <<
"(sr::get_valid_array_size) consider reducing "
1019 "max-nondet-string-length so "
1020 "that no string exceeds "
1022 <<
" in length and "
1023 "make sure all functions returning strings are loaded"
1025 stream <<
"(sr::get_valid_array_size) this can also happen on invalid "
1048 if(arr.
type().
id() != ID_array)
1049 return std::string(
"");
1065 const std::function<
exprt(
const exprt &)> &super_get,
1071 stream <<
"- " <<
format(arr) <<
":\n";
1072 stream << std::string(4,
' ') <<
"- type: " <<
format(arr.
type())
1074 const auto arr_model_opt =
get_array(super_get, ns, stream, arr, array_pool);
1077 stream << std::string(4,
' ') <<
"- char_array: " <<
format(*arr_model_opt)
1079 stream << std::string(4,
' ')
1082 stream << std::string(4,
' ')
1085 const auto concretized_array =
get_array(
1088 stream << std::string(4,
' ')
1089 <<
"- concretized_char_array: " <<
format(*concretized_array)
1093 const auto array_expr =
1094 expr_try_dynamic_cast<array_exprt>(*concretized_array))
1096 stream << std::string(4,
' ') <<
"- as_string: \""
1100 stream << std::string(2,
' ') <<
"- warning: not an array"
1102 return *concretized_array;
1106 stream << std::string(4,
' ') <<
"- incomplete model" <<
messaget::eom;
1116 const std::function<
exprt(
const exprt &)> &super_get,
1117 const std::vector<symbol_exprt> &symbols,
1120 stream <<
"debug_model:" <<
'\n';
1123 const auto arr = pointer_array.second;
1127 stream <<
"- " <<
format(arr) <<
":\n"
1128 <<
" - pointer: " <<
format(pointer_array.first) <<
"\n"
1132 for(
const auto &symbol : symbols)
1134 stream <<
" - " << symbol.get_identifier() <<
": "
1135 <<
format(super_get(symbol)) <<
'\n';
1155 const bool left_propagate)
1173 const exprt default_val = symbol_generator(
"out_of_bound_access",
char_type);
1182 const bool left_propagate)
1195 substituted_true_case ? *substituted_true_case : true_index,
1196 substituted_false_case ? *substituted_false_case : false_index);
1202 const bool left_propagate)
1205 if(
auto array_of = expr_try_dynamic_cast<array_of_exprt>(array))
1206 return array_of->op();
1207 if(
auto array_with = expr_try_dynamic_cast<with_exprt>(array))
1209 *array_with, index_expr.
index(), left_propagate);
1210 if(
auto array_expr = expr_try_dynamic_cast<array_exprt>(array))
1212 *array_expr, index_expr.
index(), symbol_generator);
1213 if(
auto if_expr = expr_try_dynamic_cast<if_exprt>(array))
1215 *if_expr, index_expr.
index(), symbol_generator, left_propagate);
1218 array.
is_nil() || array.
id() == ID_symbol || array.
id() == ID_nondet_symbol,
1220 "in case the array is unknown, it should be a symbol or nil, id: ") +
1231 const bool left_propagate)
1236 if(
const auto index_expr = expr_try_dynamic_cast<index_exprt>(*it))
1243 it.mutate() = *result;
1270 const bool left_propagate)
1289 const std::function<
exprt(
const exprt &)> &get)
1292 const auto lbe = numeric_cast_v<mp_integer>(
1294 const auto ube = numeric_cast_v<mp_integer>(
1308 std::vector<exprt> conjuncts;
1309 conjuncts.reserve(numeric_cast_v<std::size_t>(ube - lbe));
1313 const exprt s0_char =
1316 conjuncts.push_back(
equal_exprt(s0_char, s1_char));
1326 template <
typename T>
1330 const T &axiom_in_model,
1331 const exprt &negaxiom,
1332 const exprt &with_concretized_arrays)
1334 stream << std::string(4,
' ') <<
"- axiom:\n" << std::string(6,
' ');
1337 << std::string(4,
' ') <<
"- axiom_in_model:\n"
1338 << std::string(6,
' ');
1339 stream <<
to_string(axiom_in_model) <<
'\n'
1340 << std::string(4,
' ') <<
"- negated_axiom:\n"
1341 << std::string(6,
' ') <<
format(negaxiom) <<
'\n';
1342 stream << std::string(4,
' ') <<
"- negated_axiom_with_concretized_arrays:\n"
1343 << std::string(6,
' ') <<
format(with_concretized_arrays) <<
'\n';
1350 const std::function<
exprt(
const exprt &)> &get,
1353 bool use_counter_example,
1355 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1356 ¬_contain_witnesses)
1358 stream <<
"string_refinementt::check_axioms:" <<
messaget::eom;
1361 auto pairs = symbol_resolve.
to_vector();
1362 for(
const auto &pair : pairs)
1363 stream <<
" - " <<
format(pair.first) <<
" --> " <<
format(pair.second)
1377 std::map<size_t, exprt> violated;
1379 stream <<
"string_refinement::check_axioms: " << axioms.
universal.size()
1381 for(
size_t i = 0; i < axioms.
universal.size(); i++)
1393 stream << std::string(2,
' ') << i <<
".\n";
1394 const exprt with_concretized_arrays =
1397 stream, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
1402 with_concretized_arrays,
1406 stream << std::string(4,
' ')
1409 violated[i] = *witness;
1412 stream << std::string(4,
' ') <<
"- correct" <<
messaget::eom;
1416 std::map<std::size_t, exprt> violated_not_contains;
1418 stream <<
"there are " << axioms.
not_contains.size() <<
" not_contains axioms"
1420 for(std::size_t i = 0; i < axioms.
not_contains.size(); i++)
1426 nc_axiom, univ_var, [&](
const exprt &expr) {
1430 stream << std::string(2,
' ') << i <<
".\n";
1432 stream, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
1438 stream << std::string(4,
' ')
1441 violated_not_contains[i] = *witness;
1445 if(violated.empty() && violated_not_contains.empty())
1448 return {
true, std::vector<exprt>()};
1452 stream << violated.size() <<
" universal string axioms can be violated"
1454 stream << violated_not_contains.size()
1455 <<
" not_contains string axioms can be violated" <<
messaget::eom;
1457 if(use_counter_example)
1459 std::vector<exprt> lemmas;
1461 for(
const auto &v : violated)
1463 const exprt &val = v.second;
1474 lemmas.push_back(counter);
1477 for(
const auto &v : violated_not_contains)
1479 const exprt &val = v.second;
1483 const exprt func_val =
1484 index_exprt(not_contain_witnesses.at(axiom), val);
1487 std::set<std::pair<exprt, exprt>> indices;
1488 indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
1489 const exprt counter =
1491 lemmas.push_back(counter);
1493 return {
false, lemmas};
1496 return {
false, std::vector<exprt>()};
1516 for(
const auto &axiom : axioms.
universal)
1529 const std::vector<exprt> ¤t_constraints)
1531 for(
const auto &axiom : current_constraints)
1543 if(array_expr.
id() == ID_if)
1550 if(array_expr.
type().
id() == ID_array)
1553 accu.push_back(array_expr);
1557 for(
const auto &operand : array_expr.
operands())
1575 const bool is_size_t = numeric_cast<std::size_t>(i).has_value();
1576 if(i.
id() != ID_constant || is_size_t)
1578 std::vector<exprt> sub_arrays;
1580 for(
const auto &sub : sub_arrays)
1581 if(index_set.
cumulative[sub].insert(i).second)
1582 index_set.
current[sub].insert(i);
1605 const exprt &upper_bound,
1610 s.
id() == ID_symbol || s.
id() == ID_nondet_symbol || s.
id() == ID_array ||
1612 if(s.
id() == ID_array)
1614 for(std::size_t j = 0; j < s.
operands().size(); ++j)
1618 if(
auto ite = expr_try_dynamic_cast<if_exprt>(s))
1644 const auto &s = index_expr.array();
1646 it.next_sibling_or_parent();
1670 it.next_sibling_or_parent();
1688 const exprt &formula)
1690 std::list<exprt> to_process;
1691 to_process.push_back(formula);
1693 while(!to_process.empty())
1695 exprt cur = to_process.back();
1696 to_process.pop_back();
1702 s.
type().
id() == ID_array,
1705 if(s.
id() != ID_array)
1711 to_process.push_back(*it);
1737 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1744 const auto &index_set1 = index_set.
cumulative.find(
s1.content());
1745 const auto ¤t_index_set0 = index_set.
current.find(s0.
content());
1746 const auto ¤t_index_set1 = index_set.
current.find(
s1.content());
1751 current_index_set0 != index_set.
current.end() &&
1752 current_index_set1 != index_set.
current.end())
1754 typedef std::pair<exprt, exprt> expr_pairt;
1755 std::set<expr_pairt> index_pairs;
1757 for(
const auto &ic0 : current_index_set0->second)
1758 for(
const auto &i1 : index_set1->second)
1759 index_pairs.insert(expr_pairt(ic0, i1));
1760 for(
const auto &ic1 : current_index_set1->second)
1761 for(
const auto &i0 : index_set0->second)
1762 index_pairs.insert(expr_pairt(i0, ic1));
1778 for(
auto &operand : expr.
operands())
1781 if(expr.
id() == ID_array_list)
1791 for(
size_t i = 0; i < expr.
operands().size(); i += 2)
1795 const auto index_value = numeric_cast<std::size_t>(index);
1798 (index_value && *index_value < string_max_length))
1799 ret_expr =
with_exprt(ret_expr, index, value);
1816 const auto super_get = [
this](
const exprt &expr) {
1823 const auto &index_expr = expr_try_dynamic_cast<index_exprt>(ecopy);
1826 std::reference_wrapper<const exprt> current(index_expr->array());
1827 while(current.get().id() == ID_if)
1829 const auto &if_expr = expr_dynamic_cast<if_exprt>(current.get());
1830 const exprt cond =
get(if_expr.cond());
1832 current = std::cref(if_expr.true_case());
1834 current = std::cref(if_expr.false_case());
1839 const auto index =
get(index_expr->index());
1846 const exprt unknown =
1851 if(
const auto index_value = numeric_cast<std::size_t>(index))
1852 return sparse_array->at(*index_value);
1853 return sparse_array->to_if_expression(index);
1856 INVARIANT(array.id() == ID_symbol || array.id() == ID_nondet_symbol,
1857 "Apart from symbols, array valuations can be interpreted as "
1858 "sparse arrays. Array model : " + array.pretty());
1867 const auto from_dependencies =
1869 return *from_dependencies;
1872 const auto arr_model_opt =
1874 return *arr_model_opt;
1877 const auto &length_from_pool =
1880 const exprt length = super_get(length_from_pool.value());
1882 if(
const auto n = numeric_cast<std::size_t>(length))
1909 satcheck_no_simplifiert sat_check(message_handler);
1930 [&](
const exprt &expr)
1932 const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
1934 indices[index_expr->array()].push_back(index_expr->index());
1951 it->id() != ID_plus && it->id() != ID_minus &&
1952 it->id() != ID_unary_minus && *it != var)
1954 if(std::find(it->depth_begin(), it->depth_end(), var) != it->depth_end())
1957 it.next_sibling_or_parent();
1978 if(it->id() == ID_index)
1979 it.next_sibling_or_parent();
2000 for(
const auto &pair : body_indices)
2003 const exprt rep = pair.second.back();
2004 for(
size_t j = 0; j < pair.second.size() - 1; j++)
2006 const exprt i = pair.second[j];
2011 stream <<
"Indices not equal: " <<
to_string(constraint)
2020 stream <<
"f is not linear: " <<
to_string(constraint)
2029 stream <<
"Universal variable outside of index:" <<
to_string(constraint)
Operator to update elements in structs and arrays.
std::vector< string_constraintt > universal
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
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.
bool equality_propagation
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...
string_constraint_generatort generator
const typet & length_type() const
const typet & subtype() const
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
std::vector< std::pair< exprt, exprt > > to_vector() const
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 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.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
depth_iteratort depth_begin()
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)
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.
The type of an expression, extends irept.
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 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 void display_index_set(messaget::mstreamt &stream, const index_set_pairt &index_set)
Write index set to the given stream, use for debugging.
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.
Correspondance between arrays and pointers string representations.
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
std::vector< exprt > current_constraints
The trinary if-then-else operator.
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
Represents arrays by the indexes up to which the value remains the same.
symbol_generatort fresh_symbol
exprt to_if_expression(const exprt &index) const
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by the representative element of the set they belong to.
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
const std::size_t MAX_CONCRETE_STRING_SIZE
The plus expression Associativity is not specified.
Base class for all expressions.
void l_set_to_true(literalt a)
Collection of constraints of different types: existential formulas, universal formulas,...
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,...
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...
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given...
bool is_true() const
Return whether the expression is a constant representing true.
index_set_pairt index_sets
Expression to hold a symbol (variable)
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,...
bitvector_typet index_type()
Keeps track of dependencies between strings.
Magic numbers used throughout the codebase.
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
bool can_cast_expr< equal_exprt >(const exprt &base)
An expression denoting infinity.
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.
bool is_false() const
Return whether the expression is a constant representing false.
static void initial_index_set(index_set_pairt &index_set, const namespacet &ns, const string_constraintt &axiom)
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
std::map< exprt, std::vector< exprt > > array_index_mapt
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...
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
const array_typet & type() const
Generation of fresh symbols of a given type.
static bool validate(const string_refinementt::infot &info)
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
decision_proceduret::resultt dec_solve() override
Run the decision procedure to solve the problem.
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...
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
void clean_cache()
Clean the cache used by eval
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.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define CHARACTER_FOR_UNKNOWN
const std::string & id2string(const irep_idt &d)
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...
exprt substitute_array_lists(exprt expr, size_t string_max_length)
Replace array-lists by 'with' expressions.
#define forall_operands(it, expr)
static std::string string_of_array(const array_exprt &arr)
convert the content of a string to a more readable representation.
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
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...
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
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
void output_dot(std::ostream &stream) const
Array constructor from single element.
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 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 bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
Checks the data invariant for string_constraintt.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
const irep_idt & id() const
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 ...
Ranges: pair of begin and end iterators, which can be initialized from containers,...
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
String support via creating string constraints and progressively instantiating the universal constrai...
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.
Maps equation to expressions contained in them and conversely expressions to equations that contain t...
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.
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...
array_string_exprt & to_array_string_expr(exprt &expr)
optionalt< exprt > make_array_pointer_association(const exprt &return_code, const function_application_exprt &expr)
Associate array to pointer, and array to length.
nonstd::optional< T > optionalt
union_find_replacet symbol_resolve
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
resultt
Result of running the decision procedure.
exprt make_union(const exprt &a, const exprt &b)
Merge the set containing a and the set containing b.
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
string_dependenciest dependencies
bitvector_typet char_type()
Extract member of struct or union.
Deprecated expression utility functions.
exprt univ_within_bounds() const
message_handlert & get_message_handler()
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.
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
Structure type, corresponds to C style structs.
Forward depth-first search iterators These iterators' copy operations are expensive,...
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 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...
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bool can_cast_expr< function_application_exprt >(const exprt &base)
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
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)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
#define string_refinement_invariantt(reason)
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...
int solver(std::istream &in)
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
bool is_constant() const
Return whether the expression is a constant.
Defines related function for string constraints.
A base class for relations, i.e., binary predicates whose two operands have the same type.
exprt simplify_sum(const exprt &f)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
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.
static optionalt< exprt > substitute_array_access(const index_exprt &index_expr, symbol_generatort &symbol_generator, const bool left_propagate)
std::map< exprt, std::set< exprt > > current
std::vector< exprt > find_expressions(const std::size_t i)
std::vector< exprt > equations
std::vector< string_not_contains_constraintt > not_contains
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
Constraints to encode non containement of strings.
std::map< exprt, std::set< exprt > > cumulative
static bool is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
string_refinementt constructor arguments
static array_index_mapt gather_indices(const exprt &expr)
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...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
A constant literal expression.
depth_iteratort depth_end()
string_refinementt(const infot &)
std::vector< std::size_t > find_equations(const exprt &expr)
Array constructor from list of elements.
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...
ranget< iteratort > make_range(iteratort begin, iteratort end)
std::vector< string_not_contains_constraintt > not_contains
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
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...
std::set< exprt > seen_instances
std::vector< exprt > existential
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
std::vector< string_constraintt > universal