cprover
string_refinement.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String support via creating string constraints and progressively
4  instantiating the universal constraints as needed.
5  The procedure is described in the PASS paper at HVC'13:
6  "PASS: String Solving with Parameterized Array and Interval Automaton"
7  by Guodong Li and Indradeep Ghosh.
8 
9 Author: Alberto Griggio, alberto.griggio@gmail.com
10 
11 \*******************************************************************/
12 
19 
21 
22 #include <iomanip>
23 #include <numeric>
24 #include <stack>
25 #include <util/expr_iterator.h>
26 #include <util/expr_util.h>
27 #include <util/simplify_expr.h>
28 #include <solvers/sat/satcheck.h>
30 #include <unordered_set>
31 #include <util/magic.h>
32 
33 static bool is_valid_string_constraint(
34  messaget::mstreamt &stream,
35  const namespacet &ns,
36  const string_constraintt &constraint);
37 
39  const namespacet &ns,
40  const exprt &axiom,
41  const symbol_exprt &var);
42 
59 static std::pair<bool, std::vector<exprt>> check_axioms(
60  const string_axiomst &axioms,
62  const std::function<exprt(const exprt &)> &get,
63  messaget::mstreamt &stream,
64  const namespacet &ns,
65  bool use_counter_example,
66  const union_find_replacet &symbol_resolve);
67 
68 static void initial_index_set(
69  index_set_pairt &index_set,
70  const namespacet &ns,
71  const string_constraintt &axiom);
72 
73 static void initial_index_set(
74  index_set_pairt &index_set,
75  const namespacet &ns,
76  const string_not_contains_constraintt &axiom);
77 
78 static void initial_index_set(
79  index_set_pairt &index_set,
80  const namespacet &ns,
81  const string_axiomst &axioms);
82 
83 exprt simplify_sum(const exprt &f);
84 
85 static void update_index_set(
86  index_set_pairt &index_set,
87  const namespacet &ns,
88  const std::vector<exprt> &current_constraints);
89 
90 static void update_index_set(
91  index_set_pairt &index_set,
92  const namespacet &ns,
93  const exprt &formula);
94 
105 static exprt instantiate(
106  messaget::mstreamt &stream,
107  const string_constraintt &axiom,
108  const exprt &str,
109  const exprt &val);
110 
111 static std::vector<exprt> instantiate(
112  const string_not_contains_constraintt &axiom,
113  const index_set_pairt &index_set,
114  const string_constraint_generatort &generator);
115 
117  const std::function<exprt(const exprt &)> &super_get,
118  const namespacet &ns,
119  messaget::mstreamt &stream,
120  const array_string_exprt &arr);
121 
123  const index_exprt &index_expr,
124  const std::function<symbol_exprt(const irep_idt &, const typet &)>
125  &symbol_generator,
126  const bool left_propagate);
127 
135 template <typename T>
136 static std::vector<T> fill_in_map_as_vector(
137  const std::map<std::size_t, T> &index_value)
138 {
139  std::vector<T> result;
140  if(!index_value.empty())
141  {
142  result.resize(index_value.rbegin()->first+1);
143  for(auto it=index_value.rbegin(); it!=index_value.rend(); ++it)
144  {
145  const std::size_t index=it->first;
146  const T &value = it->second;
147  const auto next=std::next(it);
148  const std::size_t leftmost_index_to_pad=
149  next!=index_value.rend()
150  ? next->first+1
151  : 0;
152  for(std::size_t j=leftmost_index_to_pad; j<=index; j++)
153  result[j]=value;
154  }
155  }
156  return result;
157 }
158 
159 static bool validate(const string_refinementt::infot &info)
160 {
161  PRECONDITION(info.ns);
162  PRECONDITION(info.prop);
163  return true;
164 }
165 
167  : supert(info),
168  config_(info),
169  loop_bound_(info.refinement_bound),
170  generator(*info.ns)
171 {
172 }
173 
175  string_refinementt(info, validate(info)) { }
176 
178 static void display_index_set(
179  messaget::mstreamt &stream,
180  const index_set_pairt &index_set)
181 {
182  const auto eom=messaget::eom;
183  std::size_t count=0;
184  std::size_t count_current=0;
185  for(const auto &i : index_set.cumulative)
186  {
187  const exprt &s=i.first;
188  stream << "IS(" << format(s) << ")=={" << eom;
189 
190  for(const auto &j : i.second)
191  {
192  const auto it=index_set.current.find(i.first);
193  if(it!=index_set.current.end() && it->second.find(j)!=it->second.end())
194  {
195  count_current++;
196  stream << "**";
197  }
198  stream << " " << format(j) << ";" << eom;
199  count++;
200  }
201  stream << "}" << eom;
202  }
203  stream << count << " elements in index set (" << count_current
204  << " newly added)" << eom;
205 }
206 
220 // NOLINTNEXTLINE
228 static std::vector<exprt> generate_instantiations(
229  messaget::mstreamt &stream,
230  const string_constraint_generatort &generator,
231  const index_set_pairt &index_set,
232  const string_axiomst &axioms)
233 {
234  std::vector<exprt> lemmas;
235  for(const auto &i : index_set.current)
236  {
237  for(const auto &univ_axiom : axioms.universal)
238  {
239  for(const auto &j : i.second)
240  lemmas.push_back(instantiate(stream, univ_axiom, i.first, j));
241  }
242  }
243  for(const auto &nc_axiom : axioms.not_contains)
244  {
245  for(const auto &instance :
246  instantiate(nc_axiom, index_set, generator))
247  lemmas.push_back(instance);
248  }
249  return lemmas;
250 }
251 
255  string_constraint_generatort &generator,
256  std::vector<equal_exprt> &equations)
257 {
258  for(equal_exprt &eq : equations)
259  {
260  if(
261  const auto fun_app =
262  expr_try_dynamic_cast<function_application_exprt>(eq.rhs()))
263  {
264  if(const auto result = generator.make_array_pointer_association(*fun_app))
265  eq.rhs() = *result;
266  }
267  }
268 }
269 
271  const union_find_replacet &symbol_resolve,
272  std::vector<equal_exprt> &equations)
273 {
274  for(equal_exprt &eq : equations)
275  symbol_resolve.replace_expr(eq);
276 }
277 
282 void string_refinementt::set_to(const exprt &expr, bool value)
283 {
284  PRECONDITION(expr.type().id()==ID_bool);
286 
287  if(expr.id() == ID_equal && value)
288  {
289  const equal_exprt &eq_expr = to_equal_expr(expr);
290  equations.push_back(eq_expr);
291  }
292  else
293  {
294  INVARIANT(
295  !has_char_array_subexpr(expr, ns), "char array only appear in equations");
296  supert::set_to(expr, value);
297  }
298 }
299 
307  const std::vector<equal_exprt> &equations,
308  const namespacet &ns,
309  messaget::mstreamt &stream)
310 {
311  const auto eom = messaget::eom;
312  const std::string log_message =
313  "WARNING string_refinement.cpp generate_symbol_resolution_from_equations:";
315  for(const equal_exprt &eq : equations)
316  {
317  const exprt &lhs = eq.lhs();
318  const exprt &rhs = eq.rhs();
319  if(lhs.id()!=ID_symbol)
320  {
321  stream << log_message << "non symbol lhs: " << format(lhs)
322  << " with rhs: " << format(rhs) << eom;
323  continue;
324  }
325 
326  if(lhs.type()!=rhs.type())
327  {
328  stream << log_message << "non equal types lhs: " << format(lhs)
329  << "\n####################### rhs: " << format(rhs) << eom;
330  continue;
331  }
332 
333  if(is_char_pointer_type(rhs.type()))
334  {
335  solver.make_union(lhs, rhs);
336  }
337  else if(rhs.id() == ID_function_application)
338  {
339  // function applications can be ignored because they will be replaced
340  // in the convert_function_application step of dec_solve
341  }
342  else if(
343  lhs.type().id() != ID_pointer && has_char_pointer_subtype(lhs.type(), ns))
344  {
345  if(rhs.type().id() == ID_struct)
346  {
347  const struct_typet &struct_type = to_struct_type(rhs.type());
348  for(const auto &comp : struct_type.components())
349  {
350  if(is_char_pointer_type(comp.type()))
351  {
352  const member_exprt lhs_data(lhs, comp.get_name(), comp.type());
353  const exprt rhs_data = simplify_expr(
354  member_exprt(rhs, comp.get_name(), comp.type()), ns);
355  solver.make_union(lhs_data, rhs_data);
356  }
357  }
358  }
359  else
360  {
361  stream << log_message << "non struct with char pointer subexpr "
362  << format(rhs) << "\n * of type " << format(rhs.type()) << eom;
363  }
364  }
365  }
366  return solver;
367 }
368 
374 static std::vector<exprt> extract_strings_from_lhs(const exprt &lhs)
375 {
376  std::vector<exprt> result;
377  if(lhs.type() == string_typet())
378  result.push_back(lhs);
379  else if(lhs.type().id() == ID_struct)
380  {
381  const struct_typet &struct_type = to_struct_type(lhs.type());
382  for(const auto &comp : struct_type.components())
383  {
384  const std::vector<exprt> strings_in_comp = extract_strings_from_lhs(
385  member_exprt(lhs, comp.get_name(), comp.type()));
386  result.insert(
387  result.end(), strings_in_comp.begin(), strings_in_comp.end());
388  }
389  }
390  return result;
391 }
392 
397 static std::vector<exprt> extract_strings(const exprt &expr)
398 {
399  std::vector<exprt> result;
400  for(auto it = expr.depth_begin(); it != expr.depth_end();)
401  {
402  if(it->type() == string_typet() && it->id() != ID_if)
403  {
404  result.push_back(*it);
405  it.next_sibling_or_parent();
406  }
407  else if(it->id() == ID_symbol)
408  {
409  for(const exprt &e : extract_strings_from_lhs(*it))
410  result.push_back(e);
411  it.next_sibling_or_parent();
412  }
413  else
414  ++it;
415  }
416  return result;
417 }
418 
426  const equal_exprt &eq,
427  union_find_replacet &symbol_resolve,
428  const namespacet &ns)
429 {
430  if(eq.rhs().type() == string_typet())
431  {
432  symbol_resolve.make_union(eq.lhs(), eq.rhs());
433  }
434  else if(has_subtype(eq.lhs().type(), ID_string, ns))
435  {
436  if(eq.rhs().type().id() == ID_struct)
437  {
438  const struct_typet &struct_type = to_struct_type(eq.rhs().type());
439  for(const auto &comp : struct_type.components())
440  {
441  const member_exprt lhs_data(eq.lhs(), comp.get_name(), comp.type());
442  const exprt rhs_data = simplify_expr(
443  member_exprt(eq.rhs(), comp.get_name(), comp.type()), ns);
445  equal_exprt(lhs_data, rhs_data), symbol_resolve, ns);
446  }
447  }
448  }
449 }
450 
459  std::vector<equal_exprt> &equations,
460  const namespacet &ns,
461  messaget::mstreamt &stream)
462 {
463  const auto eom = messaget::eom;
464  const std::string log_message =
465  "WARNING string_refinement.cpp "
466  "string_identifiers_resolution_from_equations:";
467 
468  equation_symbol_mappingt equation_map;
469 
470  // Indexes of equations that need to be added to the result
471  std::unordered_set<size_t> required_equations;
472  std::stack<size_t> equations_to_treat;
473 
474  for(std::size_t i = 0; i < equations.size(); ++i)
475  {
476  const equal_exprt &eq = equations[i];
477  if(eq.rhs().id() == ID_function_application)
478  {
479  if(required_equations.insert(i).second)
480  equations_to_treat.push(i);
481 
482  std::vector<exprt> rhs_strings = extract_strings(eq.rhs());
483  for(const auto &expr : rhs_strings)
484  equation_map.add(i, expr);
485  }
486  else if(
487  eq.lhs().type().id() != ID_pointer &&
488  has_subtype(eq.lhs().type(), ID_string, ns))
489  {
490  std::vector<exprt> lhs_strings = extract_strings_from_lhs(eq.lhs());
491 
492  for(const auto &expr : lhs_strings)
493  equation_map.add(i, expr);
494 
495  if(lhs_strings.empty())
496  {
497  stream << log_message << "non struct with string subtype "
498  << format(eq.lhs()) << "\n * of type "
499  << format(eq.lhs().type()) << eom;
500  }
501 
502  for(const exprt &expr : extract_strings(eq.rhs()))
503  equation_map.add(i, expr);
504  }
505  }
506 
507  // transitively add all equations which depend on the equations to treat
508  while(!equations_to_treat.empty())
509  {
510  const std::size_t i = equations_to_treat.top();
511  equations_to_treat.pop();
512  for(const exprt &string : equation_map.find_expressions(i))
513  {
514  for(const std::size_t j : equation_map.find_equations(string))
515  {
516  if(required_equations.insert(j).second)
517  equations_to_treat.push(j);
518  }
519  }
520  }
521 
522  union_find_replacet result;
523  for(const std::size_t i : required_equations)
524  add_string_equation_to_symbol_resolution(equations[i], result, ns);
525 
526  return result;
527 }
528 
529 #ifdef DEBUG
530 static void output_equations(
532  std::ostream &output,
533  const std::vector<equal_exprt> &equations)
534 {
535  for(std::size_t i = 0; i < equations.size(); ++i)
536  output << " [" << i << "] " << format(equations[i].lhs())
537  << " == " << format(equations[i].rhs()) << std::endl;
538 }
539 #endif
540 
551 // NOLINTNEXTLINE
554 // NOLINTNEXTLINE
559 // NOLINTNEXTLINE
606 {
607 #ifdef DEBUG
608  debug() << "dec_solve: Initial set of equations" << eom;
609  output_equations(debug(), equations);
610 #endif
611 
612  debug() << "dec_solve: Build symbol solver from equations" << eom;
613  // This is used by get, that's why we use a class member here
616 #ifdef DEBUG
617  debug() << "symbol resolve:" << eom;
618  for(const auto &pair : symbol_resolve.to_vector())
619  debug() << format(pair.first) << " --> " << format(pair.second) << eom;
620 #endif
621 
622  const union_find_replacet string_id_symbol_resolve =
624 #ifdef DEBUG
625  debug() << "symbol resolve string:" << eom;
626  for(const auto &pair : string_id_symbol_resolve.to_vector())
627  {
628  debug() << format(pair.first) << " --> " << format(pair.second) << eom;
629  }
630 #endif
631 
632  debug() << "dec_solve: Replacing char pointer symbols" << eom;
634 
635  debug() << "dec_solve: Replacing string ids in function applications" << eom;
636  for(equal_exprt &eq : equations)
637  {
639  string_id_symbol_resolve.replace_expr(eq.rhs());
640  }
641 
642  // Generator is also used by get, so we have to use it as a class member
643  // but we make sure it is cleared at each `dec_solve` call.
646 
647 #ifdef DEBUG
648  output_equations(debug(), equations);
649 #endif
650 
651  debug() << "dec_solve: compute dependency graph and remove function "
652  << "applications captured by the dependencies:" << eom;
653  std::vector<exprt> local_equations;
654  for(const equal_exprt &eq : equations)
655  {
657  local_equations.push_back(eq);
658  }
659  equations.clear();
660 
661 #ifdef DEBUG
663 #endif
664 
665  debug() << "dec_solve: add constraints" << eom;
667 
668 #ifdef DEBUG
669  output_equations(debug(), equations);
670 #endif
671 
672 #ifdef DEBUG
673  debug() << "dec_solve: arrays_of_pointers:" << eom;
674  for(auto pair : generator.array_pool.get_arrays_of_pointers())
675  {
676  debug() << " * " << format(pair.first) << "\t--> " << format(pair.second)
677  << " : " << format(pair.second.type()) << eom;
678  }
679 #endif
680 
681  for(const auto &eq : local_equations)
682  {
683 #ifdef DEBUG
684  debug() << "dec_solve: set_to " << format(eq) << eom;
685 #endif
686  supert::set_to(eq, true);
687  }
688 
689  const auto constraints = generator.get_constraints();
690  std::transform(
691  constraints.begin(),
692  constraints.end(),
693  std::back_inserter(axioms.universal),
694  [&](string_constraintt constraint) {
695  constraint.replace_expr(symbol_resolve);
697  is_valid_string_constraint(error(), ns, constraint),
699  "string constraints satisfy their invariant"));
700  return constraint;
701  });
702 
703  const auto not_contains_constraints =
705  std::transform(
706  not_contains_constraints.begin(),
707  not_contains_constraints.end(),
708  std::back_inserter(axioms.not_contains),
711  return axiom;
712  });
713 
714  for(const auto &nc_axiom : axioms.not_contains)
715  {
716  const auto &witness_type = [&] {
717  const auto &rtype = to_array_type(nc_axiom.s0().type());
718  const typet &index_type = rtype.size().type();
720  }();
721  generator.witness[nc_axiom] =
722  generator.fresh_symbol("not_contains_witness", witness_type);
723  }
724 
725  for(const exprt &lemma : generator.get_lemmas())
726  add_lemma(lemma);
727 
728  // Initial try without index set
729  const auto get = [this](const exprt &expr) { return this->get(expr); };
732  if(res==resultt::D_SATISFIABLE)
733  {
734  bool satisfied;
735  std::vector<exprt> counter_examples;
736  std::tie(satisfied, counter_examples) = check_axioms(
737  axioms,
738  generator,
739  get,
740  debug(),
741  ns,
744  if(satisfied)
745  {
746  debug() << "check_SAT: the model is correct" << eom;
747  return resultt::D_SATISFIABLE;
748  }
749  debug() << "check_SAT: got SAT but the model is not correct" << eom;
750  }
751  else
752  {
753  debug() << "check_SAT: got UNSAT or ERROR" << eom;
754  return res;
755  }
756 
759  current_constraints.clear();
760  for(const auto &instance :
762  debug(),
763  generator,
764  index_sets,
765  axioms))
766  add_lemma(instance);
767 
768  while((loop_bound_--)>0)
769  {
772 
773  if(res==resultt::D_SATISFIABLE)
774  {
775  bool satisfied;
776  std::vector<exprt> counter_examples;
777  std::tie(satisfied, counter_examples) = check_axioms(
778  axioms,
779  generator,
780  get,
781  debug(),
782  ns,
785  if(satisfied)
786  {
787  debug() << "check_SAT: the model is correct" << eom;
788  return resultt::D_SATISFIABLE;
789  }
790 
791  debug() << "check_SAT: got SAT but the model is not correct, refining..."
792  << eom;
793 
794  // Since the model is not correct although we got SAT, we need to refine
795  // the property we are checking by adding more indices to the index set,
796  // and instantiating universal formulas with this indices.
797  // We will then relaunch the solver with these added lemmas.
798  index_sets.current.clear();
800 
802 
803  if(index_sets.current.empty())
804  {
805  if(axioms.not_contains.empty())
806  {
807  error() << "dec_solve: current index set is empty, "
808  << "this should not happen" << eom;
809  return resultt::D_ERROR;
810  }
811  else
812  {
813  debug() << "dec_solve: current index set is empty, "
814  << "adding counter examples" << eom;
815  for(const auto &counter : counter_examples)
816  add_lemma(counter);
817  }
818  }
819  current_constraints.clear();
820  for(const auto &instance :
822  debug(),
823  generator,
824  index_sets,
825  axioms))
826  add_lemma(instance);
827  }
828  else
829  {
830  debug() << "check_SAT: default return " << static_cast<int>(res) << eom;
831  return res;
832  }
833  }
834  debug() << "string_refinementt::dec_solve reached the maximum number"
835  << "of steps allowed" << eom;
836  return resultt::D_ERROR;
837 }
838 
844  const exprt &lemma,
845  const bool simplify_lemma)
846 {
847  if(!seen_instances.insert(lemma).second)
848  return;
849 
850  current_constraints.push_back(lemma);
851 
852  exprt simple_lemma=lemma;
853  if(simplify_lemma)
854  simplify(simple_lemma, ns);
855 
856  if(simple_lemma.is_true())
857  {
858 #if 0
859  debug() << "string_refinementt::add_lemma : tautology" << eom;
860 #endif
861  return;
862  }
863 
864  symbol_resolve.replace_expr(simple_lemma);
865 
866  // Replace empty arrays with array_of expression because the solver cannot
867  // handle empty arrays.
868  for(auto it = simple_lemma.depth_begin(); it != simple_lemma.depth_end();)
869  {
870  if(it->id() == ID_array && it->operands().empty())
871  {
872  it.mutate() = array_of_exprt(
873  from_integer(CHARACTER_FOR_UNKNOWN, it->type().subtype()),
874  to_array_type(it->type()));
875  it.next_sibling_or_parent();
876  }
877  else
878  ++it;
879  }
880 
881  debug() << "adding lemma " << format(simple_lemma) << eom;
882 
883  prop.l_set_to_true(convert(simple_lemma));
884 }
885 
895  const std::function<exprt(const exprt &)> &super_get,
896  const namespacet &ns,
897  messaget::mstreamt &stream,
898  const array_string_exprt &arr)
899 {
900  const auto eom = messaget::eom;
901  const exprt &size = arr.length();
902  exprt arr_val = simplify_expr(super_get(arr), ns);
903  exprt size_val=super_get(size);
904  size_val=simplify_expr(size_val, ns);
905  const typet char_type = arr.type().subtype();
906  const typet &index_type=size.type();
907  const array_typet empty_ret_type(char_type, from_integer(0, index_type));
908  const array_of_exprt empty_ret(from_integer(0, char_type), empty_ret_type);
909 
910  if(size_val.id()!=ID_constant)
911  {
912  stream << "(sr::get_array) string of unknown size: " << format(size_val)
913  << eom;
914  return {};
915  }
916 
917  auto n_opt = numeric_cast<std::size_t>(size_val);
918  if(!n_opt)
919  {
920  stream << "(sr::get_array) size is not valid" << eom;
921  return {};
922  }
923  std::size_t n = *n_opt;
924 
926  {
927  stream << "(sr::get_array) long string (size " << format(arr.length())
928  << " = " << n << ") " << format(arr) << eom;
929  stream << "(sr::get_array) consider reducing string-max-input-length so "
930  "that no string exceeds "
932  << " in length and "
933  "make sure all functions returning strings are loaded"
934  << eom;
935  stream << "(sr::get_array) this can also happen on invalid object access"
936  << eom;
937  return nil_exprt();
938  }
939 
940  if(
941  const auto &array = interval_sparse_arrayt::of_expr(
943  return array->concretize(n, index_type);
944  return {};
945 }
946 
951 static std::string string_of_array(const array_exprt &arr)
952 {
953  if(arr.type().id()!=ID_array)
954  return std::string("");
955 
956  exprt size_expr=to_array_type(arr.type()).size();
957  auto n = numeric_cast_v<std::size_t>(size_expr);
958  return utf16_constant_array_to_java(arr, n);
959 }
960 
969  const std::function<exprt(const exprt &)> &super_get,
970  const namespacet &ns,
971  messaget::mstreamt &stream,
972  const array_string_exprt &arr)
973 {
974  const auto &eom = messaget::eom;
975  stream << "- " << format(arr) << ":\n";
976  stream << std::string(4, ' ') << "- type: " << format(arr.type()) << eom;
977  const auto arr_model_opt =
978  get_array(super_get, ns, stream, arr);
979  if(arr_model_opt)
980  {
981  stream << std::string(4, ' ') << "- char_array: " << format(*arr_model_opt)
982  << '\n';
983  stream << std::string(4, ' ') << "- type : " << format(arr_model_opt->type())
984  << eom;
985  const exprt simple = simplify_expr(*arr_model_opt, ns);
986  stream << std::string(4, ' ') << "- simplified_char_array: " << format(simple)
987  << eom;
988  if(
989  const auto concretized_array = get_array(
990  super_get, ns, stream, to_array_string_expr(simple)))
991  {
992  stream << std::string(4, ' ')
993  << "- concretized_char_array: " << format(*concretized_array)
994  << eom;
995 
996  if(
997  const auto array_expr =
998  expr_try_dynamic_cast<array_exprt>(*concretized_array))
999  {
1000  stream << std::string(4, ' ') << "- as_string: \""
1001  << string_of_array(*array_expr) << "\"\n";
1002  }
1003  else
1004  stream << std::string(2, ' ') << "- warning: not an array" << eom;
1005  return *concretized_array;
1006  }
1007  return simple;
1008  }
1009  stream << std::string(4, ' ') << "- incomplete model" << eom;
1010  return arr;
1011 }
1012 
1016  const string_constraint_generatort &generator,
1017  messaget::mstreamt &stream,
1018  const namespacet &ns,
1019  const std::function<exprt(const exprt &)> &super_get,
1020  const std::vector<symbol_exprt> &boolean_symbols,
1021  const std::vector<symbol_exprt> &index_symbols)
1022 {
1023  stream << "debug_model:" << '\n';
1024  for(const auto &pointer_array : generator.array_pool.get_arrays_of_pointers())
1025  {
1026  const auto arr = pointer_array.second;
1027  const exprt model = get_char_array_and_concretize(
1028  super_get, ns, stream, arr);
1029 
1030  stream << "- " << format(arr) << ":\n"
1031  << " - pointer: " << format(pointer_array.first) << "\n"
1032  << " - model: " << format(model) << messaget::eom;
1033  }
1034 
1035  for(const auto &symbol : boolean_symbols)
1036  {
1037  stream << " - " << symbol.get_identifier() << ": "
1038  << format(super_get(symbol)) << '\n';
1039  }
1040 
1041  for(const auto &symbol : index_symbols)
1042  {
1043  stream << " - " << symbol.get_identifier() << ": "
1044  << format(super_get(symbol)) << '\n';
1045  }
1046  stream << messaget::eom;
1047 }
1048 
1062  const with_exprt &expr,
1063  const exprt &index,
1064  const bool left_propagate)
1065 {
1066  return left_propagate ? interval_sparse_arrayt(expr).to_if_expression(index)
1067  : sparse_arrayt::to_if_expression(expr, index);
1068 }
1069 
1077  const array_exprt &array_expr,
1078  const exprt &index,
1079  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1080  &symbol_generator)
1081 {
1082  const typet &char_type = array_expr.type().subtype();
1083  const exprt default_val = symbol_generator("out_of_bound_access", char_type);
1084  const interval_sparse_arrayt sparse_array(array_expr, default_val);
1085  return sparse_array.to_if_expression(index);
1086 }
1087 
1089  const if_exprt &if_expr,
1090  const exprt &index,
1091  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1092  &symbol_generator,
1093  const bool left_propagate)
1094 {
1095  // Substitute recursively in branches of conditional expressions
1096  const exprt true_case = substitute_array_access(
1097  index_exprt(if_expr.true_case(), index), symbol_generator, left_propagate);
1098  const exprt false_case = substitute_array_access(
1099  index_exprt(if_expr.false_case(), index), symbol_generator, left_propagate);
1100 
1101  return if_exprt(if_expr.cond(), true_case, false_case);
1102 }
1103 
1105  const index_exprt &index_expr,
1106  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1107  &symbol_generator,
1108  const bool left_propagate)
1109 {
1110  const exprt &array = index_expr.array();
1111  if(auto array_of = expr_try_dynamic_cast<array_of_exprt>(array))
1112  return array_of->op();
1113  if(auto array_with = expr_try_dynamic_cast<with_exprt>(array))
1114  return substitute_array_access(
1115  *array_with, index_expr.index(), left_propagate);
1116  if(auto array_expr = expr_try_dynamic_cast<array_exprt>(array))
1117  return substitute_array_access(
1118  *array_expr, index_expr.index(), symbol_generator);
1119  if(auto if_expr = expr_try_dynamic_cast<if_exprt>(array))
1120  return substitute_array_access(
1121  *if_expr, index_expr.index(), symbol_generator, left_propagate);
1122 
1123  INVARIANT(
1124  array.is_nil() || array.id() == ID_symbol,
1125  std::string(
1126  "in case the array is unknown, it should be a symbol or nil, id: ")
1127  + id2string(array.id()));
1128  return index_expr;
1129 }
1130 
1135  exprt &expr,
1136  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1137  &symbol_generator,
1138  const bool left_propagate)
1139 {
1140  if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
1141  {
1142  expr =
1143  substitute_array_access(*index_expr, symbol_generator, left_propagate);
1144  }
1145 
1146  for(auto &op : expr.operands())
1147  substitute_array_access_in_place(op, symbol_generator, left_propagate);
1148 }
1149 
1171  exprt expr,
1172  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1173  &symbol_generator,
1174  const bool left_propagate)
1175 {
1176  substitute_array_access_in_place(expr, symbol_generator, left_propagate);
1177  return expr;
1178 }
1179 
1191  const string_not_contains_constraintt &constraint,
1192  const symbol_exprt &univ_var,
1193  const std::function<exprt(const exprt &)> &get)
1194 {
1195  // If the for all is vacuously true, the negation is false.
1196  const auto lbe =
1197  numeric_cast_v<mp_integer>(get(constraint.exists_lower_bound()));
1198  const auto ube =
1199  numeric_cast_v<mp_integer>(get(constraint.exists_upper_bound()));
1200  const auto univ_bounds = and_exprt(
1201  binary_relation_exprt(get(constraint.univ_lower_bound()), ID_le, univ_var),
1202  binary_relation_exprt(get(constraint.univ_upper_bound()), ID_gt, univ_var));
1203 
1204  // The negated existential becomes an universal, and this is the unrolling of
1205  // that universal quantifier.
1206  std::vector<exprt> conjuncts;
1207  conjuncts.reserve(numeric_cast_v<std::size_t>(ube - lbe));
1208  for(mp_integer i=lbe; i<ube; ++i)
1209  {
1210  const constant_exprt i_expr = from_integer(i, univ_var.type());
1211  const exprt s0_char =
1212  get(index_exprt(constraint.s0(), plus_exprt(univ_var, i_expr)));
1213  const exprt s1_char = get(index_exprt(constraint.s1(), i_expr));
1214  conjuncts.push_back(equal_exprt(s0_char, s1_char));
1215  }
1216  const exprt equal_strings = conjunction(conjuncts);
1217  return and_exprt(univ_bounds, get(constraint.premise()), equal_strings);
1218 }
1219 
1224 template <typename T>
1226  messaget::mstreamt &stream,
1227  const T &axiom,
1228  const T &axiom_in_model,
1229  const exprt &negaxiom,
1230  const exprt &with_concretized_arrays)
1231 {
1232  stream << std::string(4, ' ') << "- axiom:\n" << std::string(6, ' ');
1233  stream << to_string(axiom);
1234  stream << '\n' << std::string(4, ' ') << "- axiom_in_model:\n"
1235  << std::string(6, ' ');
1236  stream << to_string(axiom_in_model) << '\n'
1237  << std::string(4, ' ') << "- negated_axiom:\n"
1238  << std::string(6, ' ') << format(negaxiom) << '\n';
1239  stream << std::string(4, ' ') << "- negated_axiom_with_concretized_arrays:\n"
1240  << std::string(6, ' ') << format(with_concretized_arrays) << '\n';
1241 }
1242 
1245 static std::pair<bool, std::vector<exprt>> check_axioms(
1246  const string_axiomst &axioms,
1247  string_constraint_generatort &generator,
1248  const std::function<exprt(const exprt &)> &get,
1249  messaget::mstreamt &stream,
1250  const namespacet &ns,
1251  bool use_counter_example,
1252  const union_find_replacet &symbol_resolve)
1253 {
1254  const auto eom=messaget::eom;
1255  // clang-format off
1256  const auto gen_symbol = [&](const irep_idt &id, const typet &type)
1257  {
1258  return generator.fresh_symbol(id, type);
1259  };
1260  // clang-format on
1261 
1262  stream << "string_refinementt::check_axioms:" << eom;
1263 
1264  stream << "symbol_resolve:" << eom;
1265  auto pairs = symbol_resolve.to_vector();
1266  for(const auto &pair : pairs)
1267  stream << " - " << format(pair.first) << " --> " << format(pair.second)
1268  << eom;
1269 
1270 #ifdef DEBUG
1271  debug_model(
1272  generator,
1273  stream,
1274  ns,
1275  get,
1276  generator.get_boolean_symbols(),
1277  generator.get_index_symbols());
1278 #endif
1279 
1280  // Maps from indexes of violated universal axiom to a witness of violation
1281  std::map<size_t, exprt> violated;
1282 
1283  stream << "string_refinement::check_axioms: " << axioms.universal.size()
1284  << " universal axioms:" << eom;
1285  for(size_t i=0; i<axioms.universal.size(); i++)
1286  {
1287  const string_constraintt &axiom=axioms.universal[i];
1288  const string_constraintt axiom_in_model(
1289  axiom.univ_var,
1290  get(axiom.lower_bound),
1291  get(axiom.upper_bound),
1292  get(axiom.body));
1293 
1294  exprt negaxiom = axiom_in_model.negation();
1295  negaxiom = simplify_expr(negaxiom, ns);
1296 
1297  stream << std::string(2, ' ') << i << ".\n";
1298  const exprt with_concretized_arrays =
1299  substitute_array_access(negaxiom, gen_symbol, true);
1301  stream, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
1302 
1303  if(
1304  const auto &witness =
1305  find_counter_example(ns, with_concretized_arrays, axiom.univ_var))
1306  {
1307  stream << std::string(4, ' ') << "- violated_for: "
1308  << format(axiom.univ_var) << "=" << format(*witness) << eom;
1309  violated[i]=*witness;
1310  }
1311  else
1312  stream << std::string(4, ' ') << "- correct" << eom;
1313  }
1314 
1315  // Maps from indexes of violated not_contains axiom to a witness of violation
1316  std::map<std::size_t, exprt> violated_not_contains;
1317 
1318  stream << "there are " << axioms.not_contains.size()
1319  << " not_contains axioms" << eom;
1320  for(std::size_t i = 0; i < axioms.not_contains.size(); i++)
1321  {
1322  const string_not_contains_constraintt &nc_axiom=axioms.not_contains[i];
1323  const symbol_exprt univ_var = generator.fresh_univ_index(
1324  "not_contains_univ_var", nc_axiom.s0().length().type());
1325  const exprt negated_axiom = negation_of_not_contains_constraint(
1326  nc_axiom, univ_var, [&](const exprt &expr) {
1327  return simplify_expr(get(expr), ns); });
1328 
1329  stream << std::string(2, ' ') << i << ".\n";
1331  stream, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
1332 
1333  if(
1334  const auto witness =
1335  find_counter_example(ns, negated_axiom, univ_var))
1336  {
1337  stream << std::string(4, ' ') << "- violated_for: "
1338  << univ_var.get_identifier() << "=" << format(*witness) << eom;
1339  violated_not_contains[i]=*witness;
1340  }
1341  }
1342 
1343  if(violated.empty() && violated_not_contains.empty())
1344  {
1345  stream << "no violated property" << eom;
1346  return { true, std::vector<exprt>() };
1347  }
1348  else
1349  {
1350  stream << violated.size()
1351  << " universal string axioms can be violated" << eom;
1352  stream << violated_not_contains.size()
1353  << " not_contains string axioms can be violated" << eom;
1354 
1355  if(use_counter_example)
1356  {
1357  std::vector<exprt> lemmas;
1358 
1359  for(const auto &v : violated)
1360  {
1361  const exprt &val=v.second;
1362  const string_constraintt &axiom=axioms.universal[v.first];
1363 
1364  exprt instance(axiom.body);
1365  replace_expr(axiom.univ_var, val, instance);
1366  // We are not sure the index set contains only positive numbers
1367  and_exprt bounds(
1368  axiom.univ_within_bounds(),
1369  binary_relation_exprt(from_integer(0, val.type()), ID_le, val));
1370  replace_expr(axiom.univ_var, val, bounds);
1371  const implies_exprt counter(bounds, instance);
1372  lemmas.push_back(counter);
1373  }
1374 
1375  for(const auto &v : violated_not_contains)
1376  {
1377  const exprt &val=v.second;
1378  const string_not_contains_constraintt &axiom=
1379  axioms.not_contains[v.first];
1380 
1381  const exprt func_val=generator.get_witness_of(axiom, val);
1382  const exprt comp_val=simplify_sum(plus_exprt(val, func_val));
1383 
1384  std::set<std::pair<exprt, exprt>> indices;
1385  indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
1386  const exprt counter=::instantiate_not_contains(
1387  axiom, indices, generator)[0];
1388  lemmas.push_back(counter);
1389  }
1390  return { false, lemmas };
1391  }
1392  }
1393  return { false, std::vector<exprt>() };
1394 }
1395 
1400 static std::map<exprt, int> map_representation_of_sum(const exprt &f)
1401 {
1402  // number of time the leaf should be added (can be negative)
1403  std::map<exprt, int> elems;
1404 
1405  std::list<std::pair<exprt, bool> > to_process;
1406  to_process.emplace_back(f, true);
1407 
1408  while(!to_process.empty())
1409  {
1410  exprt cur=to_process.back().first;
1411  bool positive=to_process.back().second;
1412  to_process.pop_back();
1413  if(cur.id()==ID_plus)
1414  {
1415  for(const auto &op : cur.operands())
1416  to_process.emplace_back(op, positive);
1417  }
1418  else if(cur.id()==ID_minus)
1419  {
1420  to_process.emplace_back(cur.op1(), !positive);
1421  to_process.emplace_back(cur.op0(), positive);
1422  }
1423  else if(cur.id()==ID_unary_minus)
1424  {
1425  to_process.emplace_back(cur.op0(), !positive);
1426  }
1427  else
1428  {
1429  if(positive)
1430  elems[cur]=elems[cur]+1;
1431  else
1432  elems[cur]=elems[cur]-1;
1433  }
1434  }
1435  return elems;
1436 }
1437 
1445  std::map<exprt, int> &m,
1446  const typet &type,
1447  bool negated=false)
1448 {
1449  exprt sum=nil_exprt();
1450  mp_integer constants=0;
1451  typet index_type;
1452  if(m.empty())
1453  return from_integer(0, type);
1454  else
1455  index_type=m.begin()->first.type();
1456 
1457  for(const auto &term : m)
1458  {
1459  // We should group constants together...
1460  const exprt &t=term.first;
1461  int second=negated?(-term.second):term.second;
1462  if(t.id()==ID_constant)
1463  {
1464  std::string value(to_constant_expr(t).get_value().c_str());
1465  constants+=binary2integer(value, true)*second;
1466  }
1467  else
1468  {
1469  switch(second)
1470  {
1471  case -1:
1472  if(sum.is_nil())
1473  sum=unary_minus_exprt(t);
1474  else
1475  sum=minus_exprt(sum, t);
1476  break;
1477 
1478  case 1:
1479  if(sum.is_nil())
1480  sum=t;
1481  else
1482  sum=plus_exprt(sum, t);
1483  break;
1484 
1485  default:
1486  if(second>1)
1487  {
1488  if(sum.is_nil())
1489  sum=t;
1490  else
1491  plus_exprt(sum, t);
1492  for(int i=1; i<second; i++)
1493  sum=plus_exprt(sum, t);
1494  }
1495  else if(second<-1)
1496  {
1497  if(sum.is_nil())
1498  sum=unary_minus_exprt(t);
1499  else
1500  sum=minus_exprt(sum, t);
1501  for(int i=-1; i>second; i--)
1502  sum=minus_exprt(sum, t);
1503  }
1504  }
1505  }
1506  }
1507 
1508  exprt index_const=from_integer(constants, index_type);
1509  if(sum.is_not_nil())
1510  return plus_exprt(sum, index_const);
1511  else
1512  return index_const;
1513 }
1514 
1518 {
1519  std::map<exprt, int> map=map_representation_of_sum(f);
1520  return sum_over_map(map, f.type());
1521 }
1522 
1534  messaget::mstreamt &stream,
1535  const exprt &qvar,
1536  const exprt &val,
1537  const exprt &f)
1538 {
1539  exprt positive, negative;
1540  // number of time the element should be added (can be negative)
1541  // qvar has to be equal to val - f(0) if it appears positively in f
1542  // (i.e. if f(qvar)=f(0) + qvar) and f(0) - val if it appears negatively
1543  // in f. So we start by computing val - f(0).
1544  std::map<exprt, int> elems=map_representation_of_sum(minus_exprt(val, f));
1545 
1546  // true if qvar appears negatively in f (positively in elems):
1547  bool neg=false;
1548 
1549  auto it=elems.find(qvar);
1550  INVARIANT(
1551  it!=elems.end(),
1552  string_refinement_invariantt("a function must have an occurrence of qvar"));
1553  if(it->second==1 || it->second==-1)
1554  {
1555  neg=(it->second==1);
1556  }
1557  else
1558  {
1559  INVARIANT(
1560  it->second == 0,
1562  "a proper function must have exactly one "
1563  "occurrences after reduction, or it cancelled out, and it does not"
1564  " have one"));
1565  stream << "in string_refinementt::compute_inverse_function:"
1566  << " warning: occurrences of qvar cancelled out " << messaget::eom;
1567  }
1568 
1569  elems.erase(it);
1570  return sum_over_map(elems, f.type(), neg);
1571 }
1572 
1574 {
1575 private:
1576  const exprt &qvar_;
1577 
1578 public:
1579  bool found;
1580 
1581  explicit find_qvar_visitort(const exprt &qvar): qvar_(qvar), found(false) {}
1582 
1583  void operator()(const exprt &expr) override
1584  {
1585  if(expr==qvar_)
1586  found=true;
1587  }
1588 };
1589 
1594 static bool find_qvar(const exprt &index, const symbol_exprt &qvar)
1595 {
1596  find_qvar_visitort v2(qvar);
1597  index.visit(v2);
1598  return v2.found;
1599 }
1600 
1606 static void initial_index_set(
1607  index_set_pairt &index_set,
1608  const namespacet &ns,
1609  const string_axiomst &axioms)
1610 {
1611  for(const auto &axiom : axioms.universal)
1612  initial_index_set(index_set, ns, axiom);
1613  for(const auto &axiom : axioms.not_contains)
1614  initial_index_set(index_set, ns, axiom);
1615 }
1616 
1621 static void update_index_set(
1622  index_set_pairt &index_set,
1623  const namespacet &ns,
1624  const std::vector<exprt> &current_constraints)
1625 {
1626  for(const auto &axiom : current_constraints)
1627  update_index_set(index_set, ns, axiom);
1628 }
1629 
1636 static void get_sub_arrays(const exprt &array_expr, std::vector<exprt> &accu)
1637 {
1638  if(array_expr.id()==ID_if)
1639  {
1640  get_sub_arrays(to_if_expr(array_expr).true_case(), accu);
1641  get_sub_arrays(to_if_expr(array_expr).false_case(), accu);
1642  }
1643  else
1644  {
1645  if(array_expr.type().id() == ID_array)
1646  {
1647  // TODO: check_that it does not contain any sub_array
1648  accu.push_back(array_expr);
1649  }
1650  else
1651  {
1652  for(const auto &operand : array_expr.operands())
1653  get_sub_arrays(operand, accu);
1654  }
1655  }
1656 }
1657 
1663 static void add_to_index_set(
1664  index_set_pairt &index_set,
1665  const namespacet &ns,
1666  const exprt &s,
1667  exprt i)
1668 {
1669  simplify(i, ns);
1670  const bool is_size_t = numeric_cast<std::size_t>(i).has_value();
1671  if(i.id()!=ID_constant || is_size_t)
1672  {
1673  std::vector<exprt> sub_arrays;
1674  get_sub_arrays(s, sub_arrays);
1675  for(const auto &sub : sub_arrays)
1676  if(index_set.cumulative[sub].insert(i).second)
1677  index_set.current[sub].insert(i);
1678  }
1679 }
1680 
1696 static void initial_index_set(
1697  index_set_pairt &index_set,
1698  const namespacet &ns,
1699  const exprt &qvar,
1700  const exprt &upper_bound,
1701  const exprt &s,
1702  const exprt &i)
1703 {
1704  PRECONDITION(s.id() == ID_symbol || s.id() == ID_array || s.id() == ID_if);
1705  if(s.id() == ID_array)
1706  {
1707  for(std::size_t j = 0; j < s.operands().size(); ++j)
1708  add_to_index_set(index_set, ns, s, from_integer(j, i.type()));
1709  return;
1710  }
1711  if(auto ite = expr_try_dynamic_cast<if_exprt>(s))
1712  {
1713  initial_index_set(index_set, ns, qvar, upper_bound, ite->true_case(), i);
1714  initial_index_set(index_set, ns, qvar, upper_bound, ite->false_case(), i);
1715  return;
1716  }
1717  const minus_exprt u_minus_1(upper_bound, from_integer(1, upper_bound.type()));
1718  exprt i_copy = i;
1719  replace_expr(qvar, u_minus_1, i_copy);
1720  add_to_index_set(index_set, ns, s, i_copy);
1721 }
1722 
1723 static void initial_index_set(
1724  index_set_pairt &index_set,
1725  const namespacet &ns,
1726  const string_constraintt &axiom)
1727 {
1728  const symbol_exprt &qvar = axiom.univ_var;
1729  const auto &bound = axiom.upper_bound;
1730  auto it = axiom.body.depth_begin();
1731  const auto end = axiom.body.depth_end();
1732  while(it != end)
1733  {
1734  if(it->id() == ID_index && is_char_type(it->type()))
1735  {
1736  const auto &index_expr = to_index_expr(*it);
1737  const auto &s = index_expr.array();
1738  initial_index_set(index_set, ns, qvar, bound, s, index_expr.index());
1739  it.next_sibling_or_parent();
1740  }
1741  else
1742  ++it;
1743  }
1744 }
1745 
1746 static void initial_index_set(
1747  index_set_pairt &index_set,
1748  const namespacet &ns,
1749  const string_not_contains_constraintt &axiom)
1750 {
1751  auto it=axiom.premise().depth_begin();
1752  const auto end=axiom.premise().depth_end();
1753  while(it!=end)
1754  {
1755  if(it->id() == ID_index && is_char_type(it->type()))
1756  {
1757  const exprt &s=it->op0();
1758  const exprt &i=it->op1();
1759 
1760  // cur is of the form s[i] and no quantified variable appears in i
1761  add_to_index_set(index_set, ns, s, i);
1762 
1763  it.next_sibling_or_parent();
1764  }
1765  else
1766  ++it;
1767  }
1768 
1769  const minus_exprt kminus1(
1770  axiom.exists_upper_bound(),
1771  from_integer(1, axiom.exists_upper_bound().type()));
1772  add_to_index_set(index_set, ns, axiom.s1().content(), kminus1);
1773 }
1774 
1779 static void update_index_set(
1780  index_set_pairt &index_set,
1781  const namespacet &ns,
1782  const exprt &formula)
1783 {
1784  std::list<exprt> to_process;
1785  to_process.push_back(formula);
1786 
1787  while(!to_process.empty())
1788  {
1789  exprt cur=to_process.back();
1790  to_process.pop_back();
1791  if(cur.id() == ID_index && is_char_type(cur.type()))
1792  {
1793  const exprt &s=cur.op0();
1794  const exprt &i=cur.op1();
1796  s.type().id()==ID_array,
1797  string_refinement_invariantt("index expressions must index on arrays"));
1798  exprt simplified=simplify_sum(i);
1799  if(s.id() != ID_array) // do not update index set of constant arrays
1800  add_to_index_set(index_set, ns, s, simplified);
1801  }
1802  else
1803  {
1804  forall_operands(it, cur)
1805  to_process.push_back(*it);
1806  }
1807  }
1808 }
1809 
1817 static std::unordered_set<exprt, irep_hash>
1818 find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
1819 {
1820  decltype(find_indexes(expr, str, qvar)) result;
1821  auto index_str_containing_qvar = [&](const exprt &e) {
1822  if(auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
1823  {
1824  const auto &arr = index_expr->array();
1825  const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
1826  return str_it != arr.depth_end() && find_qvar(index_expr->index(), qvar);
1827  }
1828  return false;
1829  };
1830 
1831  std::for_each(expr.depth_begin(), expr.depth_end(), [&](const exprt &e) {
1832  if(index_str_containing_qvar(e))
1833  result.insert(to_index_expr(e).index());
1834  });
1835  return result;
1836 }
1837 
1851  messaget::mstreamt &stream,
1852  const string_constraintt &axiom,
1853  const exprt &str,
1854  const exprt &val)
1855 {
1856  const auto indexes = find_indexes(axiom.body, str, axiom.univ_var);
1857  INVARIANT(
1858  str.id() == ID_array || indexes.size() <= 1,
1859  "non constant array should always be accessed at the same index");
1860  exprt::operandst conjuncts;
1861  for(const auto &index : indexes)
1862  {
1863  const exprt univ_var_value =
1864  compute_inverse_function(stream, axiom.univ_var, val, index);
1865  implies_exprt instance(
1866  and_exprt(
1867  binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound),
1868  binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound)),
1869  axiom.body);
1870  replace_expr(axiom.univ_var, univ_var_value, instance);
1871  conjuncts.push_back(instance);
1872  }
1873  return conjunction(conjuncts);
1874 }
1875 
1894 static std::vector<exprt> instantiate(
1895  const string_not_contains_constraintt &axiom,
1896  const index_set_pairt &index_set,
1897  const string_constraint_generatort &generator)
1898 {
1899  const array_string_exprt &s0 = axiom.s0();
1900  const array_string_exprt &s1 = axiom.s1();
1901 
1902  const auto &index_set0=index_set.cumulative.find(s0.content());
1903  const auto &index_set1=index_set.cumulative.find(s1.content());
1904  const auto &current_index_set0=index_set.current.find(s0.content());
1905  const auto &current_index_set1=index_set.current.find(s1.content());
1906 
1907  if(index_set0!=index_set.cumulative.end() &&
1908  index_set1!=index_set.cumulative.end() &&
1909  current_index_set0!=index_set.current.end() &&
1910  current_index_set1!=index_set.current.end())
1911  {
1912  typedef std::pair<exprt, exprt> expr_pairt;
1913  std::set<expr_pairt> index_pairs;
1914 
1915  for(const auto &ic0 : current_index_set0->second)
1916  for(const auto &i1 : index_set1->second)
1917  index_pairs.insert(expr_pairt(ic0, i1));
1918  for(const auto &ic1 : current_index_set1->second)
1919  for(const auto &i0 : index_set0->second)
1920  index_pairs.insert(expr_pairt(i0, ic1));
1921 
1922  return ::instantiate_not_contains(axiom, index_pairs, generator);
1923  }
1924  return { };
1925 }
1926 
1934 exprt substitute_array_lists(exprt expr, size_t string_max_length)
1935 {
1936  for(auto &operand : expr.operands())
1937  operand = substitute_array_lists(operand, string_max_length);
1938 
1939  if(expr.id() == ID_array_list)
1940  {
1942  expr.operands().size()>=2,
1943  string_refinement_invariantt("array-lists must have at least two "
1944  "operands"));
1945  const typet &char_type = expr.operands()[1].type();
1947  exprt ret_expr=array_of_exprt(from_integer(0, char_type), arr_type);
1948 
1949  for(size_t i=0; i<expr.operands().size(); i+=2)
1950  {
1951  const exprt &index=expr.operands()[i];
1952  const exprt &value=expr.operands()[i+1];
1953  const auto index_value = numeric_cast<std::size_t>(index);
1954  if(!index.is_constant() ||
1955  (index_value && *index_value<string_max_length))
1956  ret_expr=with_exprt(ret_expr, index, value);
1957  }
1958  return ret_expr;
1959  }
1960 
1961  return expr;
1962 }
1963 
1972 {
1973  const auto super_get = [this](const exprt &expr) {
1974  return supert::get(expr);
1975  };
1976  exprt ecopy(expr);
1977  (void)symbol_resolve.replace_expr(ecopy);
1978 
1979  // Special treatment for index expressions
1980  const auto &index_expr = expr_try_dynamic_cast<index_exprt>(ecopy);
1981  if(index_expr && is_char_type(index_expr->type()))
1982  {
1983  std::reference_wrapper<const exprt> current(index_expr->array());
1984  while(current.get().id() == ID_if)
1985  {
1986  const auto &if_expr = expr_dynamic_cast<if_exprt>(current.get());
1987  const exprt cond = get(if_expr.cond());
1988  if(cond.is_true())
1989  current = std::cref(if_expr.true_case());
1990  else if(cond.is_false())
1991  current = std::cref(if_expr.false_case());
1992  else
1993  UNREACHABLE;
1994  }
1995  const auto array = supert::get(current.get());
1996  const auto index = get(index_expr->index());
1997  const exprt unknown =
1998  from_integer(CHARACTER_FOR_UNKNOWN, index_expr->type());
1999  if(
2000  const auto sparse_array = interval_sparse_arrayt::of_expr(array, unknown))
2001  {
2002  if(const auto index_value = numeric_cast<std::size_t>(index))
2003  return sparse_array->at(*index_value);
2004  return sparse_array->to_if_expression(index);
2005  }
2006 
2007  INVARIANT(
2008  array.is_nil() || array.id() == ID_symbol,
2009  std::string(
2010  "apart from symbols, array valuations can be interpreted as "
2011  "sparse arrays, id: ") +
2012  id2string(array.id()));
2013  return index_exprt(array, index);
2014  }
2015 
2016  if(is_char_array_type(ecopy.type(), ns))
2017  {
2019  arr.length() = generator.array_pool.get_length(arr);
2020 
2021  if(
2022  const auto from_dependencies =
2023  dependencies.eval(arr, [&](const exprt &expr) { return get(expr); }))
2024  return *from_dependencies;
2025 
2026  if(
2027  const auto arr_model_opt =
2028  get_array(super_get, ns, debug(), arr))
2029  return *arr_model_opt;
2030 
2031  if(generator.get_created_strings().count(arr))
2032  {
2033  const exprt length = super_get(arr.length());
2034  if(const auto n = numeric_cast<std::size_t>(length))
2035  {
2036  const interval_sparse_arrayt sparse_array(
2038  return sparse_array.concretize(*n, length.type());
2039  }
2040  }
2041  return arr;
2042  }
2043  return supert::get(ecopy);
2044 }
2045 
2055  const namespacet &ns,
2056  const exprt &axiom,
2057  const symbol_exprt &var)
2058 {
2059  satcheck_no_simplifiert sat_check;
2060  boolbvt solver(ns, sat_check);
2061  solver << axiom;
2062 
2064  return solver.get(var);
2065  else
2066  return { };
2067 }
2068 
2070 typedef std::map<exprt, std::vector<exprt>> array_index_mapt;
2071 
2074 {
2075  array_index_mapt indices;
2076  // clang-format off
2077  std::for_each(
2078  expr.depth_begin(),
2079  expr.depth_end(),
2080  [&](const exprt &expr)
2081  {
2082  const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
2083  if(index_expr)
2084  indices[index_expr->array()].push_back(index_expr->index());
2085  });
2086  // clang-format on
2087  return indices;
2088 }
2089 
2095 static bool
2097 {
2098  for(auto it = expr.depth_begin(); it != expr.depth_end();)
2099  {
2100  if(
2101  it->id() != ID_plus && it->id() != ID_minus &&
2102  it->id() != ID_unary_minus && *it != var)
2103  {
2104  if(find_qvar(*it, var))
2105  return false;
2106  else
2107  it.next_sibling_or_parent();
2108  }
2109  else
2110  ++it;
2111  }
2112  return true;
2113 }
2114 
2123 {
2124  for(auto it = constr.body.depth_begin(); it != constr.body.depth_end();)
2125  {
2126  if(*it == constr.univ_var)
2127  return false;
2128  if(it->id() == ID_index)
2129  it.next_sibling_or_parent();
2130  else
2131  ++it;
2132  }
2133  return true;
2134 }
2135 
2143  messaget::mstreamt &stream,
2144  const namespacet &ns,
2145  const string_constraintt &constraint)
2146 {
2147  const auto eom=messaget::eom;
2148  const array_index_mapt body_indices = gather_indices(constraint.body);
2149  // Must validate for each string. Note that we have an invariant that the
2150  // second value in the pair is non-empty.
2151  for(const auto &pair : body_indices)
2152  {
2153  // Condition 1: All indices of the same string must be the of the same form
2154  const exprt rep=pair.second.back();
2155  for(size_t j=0; j<pair.second.size()-1; j++)
2156  {
2157  const exprt i=pair.second[j];
2158  const equal_exprt equals(rep, i);
2159  const exprt result=simplify_expr(equals, ns);
2160  if(result.is_false())
2161  {
2162  stream << "Indices not equal: " << to_string(constraint)
2163  << ", str: " << format(pair.first) << eom;
2164  return false;
2165  }
2166  }
2167 
2168  // Condition 2: f must be linear in the quantified variable
2169  if(!is_linear_arithmetic_expr(rep, constraint.univ_var))
2170  {
2171  stream << "f is not linear: " << to_string(constraint)
2172  << ", str: " << format(pair.first) << eom;
2173  return false;
2174  }
2175 
2176  // Condition 3: the quantified variable can only occur in indices in the
2177  // body
2178  if(!universal_only_in_index(constraint))
2179  {
2180  stream << "Universal variable outside of index:" << to_string(constraint)
2181  << eom;
2182  return false;
2183  }
2184  }
2185 
2186  return true;
2187 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
static std::vector< exprt > generate_instantiations(messaget::mstreamt &stream, const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms)
Instantiation of all constraints.
The type of an expression.
Definition: type.h:22
const namespacet * ns
Definition: bv_refinement.h:37
static void display_index_set(messaget::mstreamt &stream, const index_set_pairt &index_set)
Write index set to the given stream, use for debugging.
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
static exprt sum_over_map(std::map< exprt, int > &m, const typet &type, bool negated=false)
exprt & true_case()
Definition: std_expr.h:3393
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)
Check axioms takes the model given by the underlying solver and answers whether it satisfies the stri...
static std::unordered_set< exprt, irep_hash > find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
Find indexes of str used in expr that contains qvar, for instance with arguments (str[k+1]==&#39;a&#39;), str, and k, the function should return k+1.
BigInt mp_integer
Definition: mp_arith.h:22
static exprt instantiate(messaget::mstreamt &stream, const string_constraintt &axiom, const exprt &str, const exprt &val)
Substitute qvar the universally quantified variable of axiom, by an index val, in axiom...
void add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
const std::set< array_string_exprt > & get_created_strings() const
Set of strings that have been created by the generator.
bool is_nil() const
Definition: irep.h:172
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
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)
Debugging function which finds the valuation of the given array in super_get and concretize unknown c...
std::vector< equal_exprt > equations
std::map< exprt, std::vector< exprt > > array_index_mapt
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:162
const exprt & univ_lower_bound() const
const std::vector< string_constraintt > & get_constraints() const
bool equality_propagation
Definition: prop_conv.h:112
exprt get_witness_of(const string_not_contains_constraintt &c, const exprt &univ_val) const
exprt & op0()
Definition: expr.h:72
exprt simplify_expr(const exprt &src, const namespacet &ns)
void clean_cache()
Clean the cache used by eval
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
Definition: expr_util.cpp:152
union_find_replacet string_identifiers_resolution_from_equations(std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Symbol resolution for expressions of type string typet.
Deprecated expression utility functions.
static optionalt< exprt > find_counter_example(const namespacet &ns, const exprt &axiom, const symbol_exprt &var)
Creates a solver with axiom as the only formula added and runs it.
bool add_node(string_dependenciest &dependencies, const equal_exprt &equation, array_poolt &array_pool)
When right hand side of equation is a builtin_function add a "string_builtin_function" node to the gr...
const std::vector< exprt > & get_lemmas() const
Axioms are of three kinds: universally quantified string constraint, not contains string constraints ...
const irep_idt & get_identifier() const
Definition: std_expr.h:128
bool is_false() const
Definition: expr.cpp:131
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by a canonical element of the set they belong to.
string_refinementt constructor arguments
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
std::map< exprt, std::set< exprt > > current
const componentst & components() const
Definition: std_types.h:245
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
static void update_index_set(index_set_pairt &index_set, const namespacet &ns, const std::vector< exprt > &current_constraints)
Add to the index set all the indices that appear in the formulas.
exprt get_length(const array_string_exprt &s) const
Associate an actual finite length to infinite arrays.
The trinary if-then-else operator.
Definition: std_expr.h:3359
exprt & cond()
Definition: std_expr.h:3383
bool is_true() const
Definition: expr.cpp:124
static exprt substitute_array_access(const index_exprt &index_expr, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator, const bool left_propagate)
typet & type()
Definition: expr.h:56
const std::vector< string_not_contains_constraintt > & get_not_contains_constraints() const
depth_iteratort depth_begin()
Definition: expr.cpp:299
exprt univ_within_bounds() const
static union_find_replacet generate_symbol_resolution_from_equations(const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Add association for each char pointer in the equation.
Magic numbers used throughout the codebase.
A constant literal expression.
Definition: std_expr.h:4422
static bool validate(const string_refinementt::infot &info)
auto expr_dynamic_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:165
static optionalt< exprt > get_array(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr)
Get a model of an array and put it in a certain form.
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
boolean implication
Definition: std_expr.h:2339
void clear_constraints()
Clear all constraints and lemmas.
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
void l_set_to_true(literalt a)
Definition: prop.h:49
exprt substitute_array_lists(exprt expr, size_t string_max_length)
Replace array-lists by &#39;with&#39; expressions.
Definition: boolbv.h:31
const std::vector< symbol_exprt > & get_boolean_symbols() const
Boolean symbols for the results of some string functions.
Extract member of struct or union.
Definition: std_expr.h:3869
void operator()(const exprt &expr) override
TO_BE_DOCUMENTED.
Definition: std_types.h:1578
string_dependenciest dependencies
equality
Definition: std_expr.h:1354
string_refinementt(const infot &)
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.
bool can_cast_expr< function_application_exprt >(const exprt &base)
Definition: std_expr.h:4606
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:48
static void substitute_array_access_in_place(exprt &expr, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator, const bool left_propagate)
Auxiliary function for substitute_array_access Performs the same operation but modifies the argument ...
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.
const exprt & exists_lower_bound() const
const irep_idt & id() const
Definition: irep.h:259
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
exprt make_union(const exprt &a, const exprt &b)
Keeps a map of symbols to expressions, such as none of the mapped values exist as a key...
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 visit(class expr_visitort &visitor)
Definition: expr.cpp:263
An expression denoting infinity.
Definition: std_expr.h:4692
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 string_constraint_generatort &generator)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
#define CHARACTER_FOR_UNKNOWN
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...
Constraints to encode non containement of strings.
The NIL expression.
Definition: std_expr.h:4508
int solver(std::istream &in)
std::map< exprt, std::set< exprt > > cumulative
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...
Represents arrays by the indexes up to which the value remains the same.
exprt simplify_sum(const exprt &f)
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
Checks the data invariant for string_constraintt.
nonstd::optional< T > optionalt
Definition: optional.h:35
boolean AND
Definition: std_expr.h:2255
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:122
exprt & op1()
Definition: expr.h:75
union_find_replacet symbol_resolve
mstreamt & error() const
Definition: message.h:302
const std::size_t MAX_CONCRETE_STRING_SIZE
Definition: magic.h:14
TO_BE_DOCUMENTED.
Definition: namespace.h:74
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:893
const namespacet & ns
std::vector< exprt > instantiate_not_contains(const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt >> &index_pairs, const string_constraint_generatort &generator)
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
array constructor from single element
Definition: std_expr.h:1550
size_t size() const
Definition: dstring.h:89
bitvector_typet index_type()
Definition: c_types.cpp:16
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
decision_proceduret::resultt dec_solve() override
The unary minus expression.
Definition: std_expr.h:444
exprt & false_case()
Definition: std_expr.h:3403
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
static bool is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
bool is_constant() const
Definition: expr.cpp:119
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 bool find_qvar(const exprt &index, const symbol_exprt &qvar)
look for the symbol and return true if it is found
string_constraint_generatort generator
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
std::vector< exprt > operandst
Definition: expr.h:45
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...
String support via creating string constraints and progressively instantiating the universal constrai...
std::vector< string_constraintt > universal
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
static void make_char_array_pointer_associations(string_constraint_generatort &generator, std::vector< equal_exprt > &equations)
Fill the array_pointer correspondence and replace the right hand sides of the corresponding equations...
static void initial_index_set(index_set_pairt &index_set, const namespacet &ns, const string_constraintt &axiom)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
Definition: std_expr.h:1377
exprt get(const exprt &expr) const override
Definition: boolbv_get.cpp:21
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
std::vector< exprt > find_expressions(const std::size_t i)
exprt & index()
Definition: std_expr.h:1496
Maps equation to expressions contained in them and conversely expressions to equations that contain t...
const configt config_
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 std::string string_of_array(const array_exprt &arr)
convert the content of a string to a more readable representation.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
const exprt & exists_upper_bound() const
Base class for all expressions.
Definition: expr.h:42
static std::vector< exprt > extract_strings(const exprt &expr)
optionalt< exprt > make_array_pointer_association(const function_application_exprt &expr)
Associate array to pointer, and array to length.
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...
std::set< exprt > seen_instances
Operator to update elements in structs and arrays.
Definition: std_expr.h:3459
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define UNREACHABLE
Definition: invariant.h:271
exprt to_if_expression(const exprt &index) const
literalt neg(literalt a)
Definition: literal.h:192
static std::map< exprt, int > map_representation_of_sum(const exprt &f)
#define string_refinement_invariantt(reason)
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...
Universally quantified string constraint
string_axiomst axioms
const exprt & univ_upper_bound() const
arrays with given size
Definition: std_types.h:1013
binary minus
Definition: std_expr.h:959
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, otherwise returns empty optional.
static std::vector< exprt > extract_strings_from_lhs(const exprt &lhs)
This is meant to be used on the lhs of an equation with string subtype.
Expression to hold a symbol (variable)
Definition: std_expr.h:90
depth_iteratort depth_end()
Definition: expr.cpp:301
int8_t s1
Definition: bytecode_info.h:59
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 > &boolean_symbols, const std::vector< symbol_exprt > &index_symbols)
Display part of the current model by mapping the variables created by the solver to constant expressi...
mstreamt & debug() const
Definition: message.h:332
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
void set_to(const exprt &expr, bool value) override
Definition: boolbv.cpp:601
std::map< string_not_contains_constraintt, symbol_exprt > witness
const array_string_exprt & s0() const
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 is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
operandst & operands()
Definition: expr.h:66
std::vector< std::size_t > find_equations(const exprt &expr)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const std::vector< symbol_exprt > & get_index_symbols() const
Symbols used in existential quantifications.
exprt negation() const
std::vector< exprt > current_constraints
static array_index_mapt gather_indices(const exprt &expr)
exprt & array()
Definition: std_expr.h:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
bitvector_typet char_type()
Definition: c_types.cpp:114
array constructor from list of elements
Definition: std_expr.h:1617
void replace_symbols_in_equations(const union_find_replacet &symbol_resolve, std::vector< equal_exprt > &equations)
index_set_pairt index_sets
std::vector< string_not_contains_constraintt > not_contains
std::vector< std::pair< exprt, exprt > > to_vector() const
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:162
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:91
static exprt compute_inverse_function(messaget::mstreamt &stream, const exprt &qvar, const exprt &val, const exprt &f)
bool simplify(exprt &expr, const namespacet &ns)
void output_dot(std::ostream &stream) const
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
array index operator
Definition: std_expr.h:1462
static format_containert< T > format(const T &o)
Definition: format.h:35
const array_string_exprt & s1() const
find_qvar_visitort(const exprt &qvar)