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 <sstream>
23 #include <ansi-c/string_constant.h>
24 #include <util/cprover_prefix.h>
25 #include <util/replace_expr.h>
26 #include <solvers/sat/satcheck.h>
27 #include <langapi/language_util.h>
28 
30  const namespacet &_ns, propt &_prop, unsigned refinement_bound):
31  supert(_ns, _prop),
32  use_counter_example(false),
33  initial_loop_bound(refinement_bound)
34 { }
35 
38 {
39  debug() << "initializing mode" << eom;
40  symbolt init=ns.lookup(irep_idt(CPROVER_PREFIX"initialize"));
41  irep_idt mode=init.mode;
42  debug() << "mode detected as " << mode << eom;
43  generator.set_mode(mode);
44 }
45 
48 {
49  for(const auto &i : index_set)
50  {
51  const exprt &s=i.first;
52  debug() << "IS(" << from_expr(s) << ")=={";
53 
54  for(auto j : i.second)
55  debug() << from_expr(j) << "; ";
56  debug() << "}" << eom;
57  }
58 }
59 
63 {
64  debug() << "string_constraint_generatort::add_instantiations: "
65  << "going through the current index set:" << eom;
66  for(const auto &i : current_index_set)
67  {
68  const exprt &s=i.first;
69  debug() << "IS(" << from_expr(s) << ")=={";
70 
71  for(const auto &j : i.second)
72  debug() << from_expr(j) << "; ";
73  debug() << "}" << eom;
74 
75  for(const auto &j : i.second)
76  {
77  const exprt &val=j;
78 
79  for(const auto &ua : universal_axioms)
80  {
81  exprt lemma=instantiate(ua, s, val);
82  add_lemma(lemma);
83  }
84  }
85  }
86 }
87 
93 {
94  if(expr.id()==ID_function_application)
95  {
96  // can occur in __CPROVER_assume
98  assert(bv.size()==1);
99  return bv[0];
100  }
101  else
102  {
103  return supert::convert_rest(expr);
104  }
105 }
106 
113 {
114  const typet &type=expr.type();
115  const irep_idt &identifier=expr.get(ID_identifier);
116  assert(!identifier.empty());
117 
119  {
120  string_exprt str=
122  bvt bv=convert_bv(str);
123  return bv;
124  }
125  else
126  return supert::convert_symbol(expr);
127 }
128 
135 {
136  debug() << "string_refinementt::convert_function_application "
137  << from_expr(expr) << eom;
138  exprt f=generator.add_axioms_for_function_application(expr);
139  return convert_bv(f);
140 }
141 
146 {
148  return true;
149 
150  // We should not do that everytime, but I cannot find
151  // another good entry point
152  if(generator.get_mode()==ID_unknown)
153  set_mode();
154 
155  typet type=ns.follow(expr.lhs().type());
156 
157  if(expr.lhs().id()==ID_symbol &&
158  // We can have affectation of string from StringBuilder or CharSequence
159  // type==ns.follow(expr.rhs().type()) &&
160  type.id()!=ID_bool)
161  {
162  debug() << "string_refinementt " << from_expr(expr.lhs()) << " <- "
163  << from_expr(expr.rhs()) << eom;
164 
165 
166  if(expr.rhs().id()==ID_typecast)
167  {
168  exprt uncast=to_typecast_expr(expr.rhs()).op();
170  {
171  debug() << "(sr) detected casted string" << eom;
172  symbol_exprt sym=to_symbol_expr(expr.lhs());
174  return false;
175  }
176  }
177 
179  {
180  symbol_exprt sym=to_symbol_expr(expr.lhs());
182  return false;
183  }
184  else if(type==ns.follow(expr.rhs().type()))
185  {
186  if(is_unbounded_array(type))
187  return true;
188  bvt bv1=convert_bv(expr.rhs());
189  const irep_idt &identifier=
190  to_symbol_expr(expr.lhs()).get_identifier();
191  map.set_literals(identifier, type, bv1);
192  if(freeze_all)
193  set_frozen(bv1);
194  return false;
195  }
196  }
197 
198  return true;
199 }
200 
205 {
206  for(const exprt &axiom : generator.axioms)
207  if(axiom.id()==ID_string_constraint)
208  {
210  universal_axioms.push_back(c);
211  }
212  else if(axiom.id()==ID_string_not_contains_constraint)
213  {
217  const typet &index_type=rtype.get_index_type();
219  generator.witness[nc_axiom]=
220  generator.fresh_symbol("not_contains_witness", witness_type);
221  not_contains_axioms.push_back(nc_axiom);
222  }
223  else
224  {
225  add_lemma(axiom);
226  }
227 
230  cur.clear();
232 
233  while((initial_loop_bound--)>0)
234  {
236 
237  switch(res)
238  {
239  case D_SATISFIABLE:
240  if(!check_axioms())
241  {
242  debug() << "check_SAT: got SAT but the model is not correct" << eom;
243  }
244  else
245  {
246  debug() << "check_SAT: the model is correct" << eom;
247  return D_SATISFIABLE;
248  }
249 
250  debug() << "refining..." << eom;
251  // Since the model is not correct although we got SAT, we need to refine
252  // the property we are checking by adding more indices to the index set,
253  // and instantiating universal formulas with this indices.
254  // We will then relaunch the solver with these added lemmas.
255  current_index_set.clear();
257  cur.clear();
259 
260  if(current_index_set.empty())
261  {
262  debug() << "current index set is empty" << eom;
263  return D_SATISFIABLE;
264  }
265 
267  debug()<< "instantiating NOT_CONTAINS constraints" << eom;
268  for(unsigned i=0; i<not_contains_axioms.size(); i++)
269  {
270  debug()<< "constraint " << i << eom;
271  std::list<exprt> lemmas;
273  for(const exprt &lemma : lemmas)
274  add_lemma(lemma);
275  }
276  break;
277  default:
278  return res;
279  }
280  }
281  debug() << "string_refinementt::dec_solve reached the maximum number"
282  << "of steps allowed" << eom;
283  return D_ERROR;
284 }
285 
290 {
291  bvt ret;
292  ret.push_back(convert(boole));
293  size_t width=boolbv_width(orig.type());
294  ret.resize(width, const_literal(false));
295  return ret;
296 }
297 
300 void string_refinementt::add_lemma(const exprt &lemma, bool add_to_index_set)
301 {
302  if(!seen_instances.insert(lemma).second)
303  return;
304 
305  if(lemma.is_true())
306  {
307  debug() << "string_refinementt::add_lemma : tautology" << eom;
308  return;
309  }
310 
311  debug() << "adding lemma " << from_expr(lemma) << eom;
312 
313  prop.l_set_to_true(convert(lemma));
314  if(add_to_index_set)
315  cur.push_back(lemma);
316 }
317 
323  const exprt &arr, const exprt &size) const
324 {
325  if(size.id()!=ID_constant)
326  return "string of unknown size";
327  unsigned n;
329  n=0;
330 
332  return "very long string";
333  if(n==0)
334  return "\"\"";
335 
336  std::ostringstream buf;
337  buf << "\"";
338  exprt val=get(arr);
339 
340  if(val.id()=="array-list")
341  {
342  for(size_t i=0; i<val.operands().size()/2; i++)
343  {
344  exprt index=val.operands()[i*2];
345  unsigned idx;
346  if(!to_unsigned_integer(to_constant_expr(index), idx))
347  {
348  if(idx<n)
349  {
350  exprt value=val.operands()[i*2+1];
351  unsigned c;
352  if(!to_unsigned_integer(to_constant_expr(value), c))
353  buf << static_cast<char>(c);
354  }
355  }
356  }
357  }
358  else
359  {
360  return "unable to get array-list";
361  }
362 
363  buf << "\"";
364  return buf.str();
365 }
366 
371 {
372  exprt val=get(arr);
373  typet char_type=arr.type().subtype();
374  typet index_type=size.type();
375 
376  if(val.id()=="array-list")
377  {
379  exprt ret=array_of_exprt(from_integer(0, char_type), ret_type);
380 
381  for(size_t i=0; i<val.operands().size()/2; i++)
382  {
383  exprt index=val.operands()[i*2];
384  assert(index.type()==index_type);
385  exprt value=val.operands()[i*2+1];
386  assert(value.type()==char_type);
387  ret=with_exprt(ret, index, value);
388  }
389  return ret;
390  }
391  else
392  {
393  debug() << "unable to get array-list value of "
394  << from_expr(val) << eom;
395  return arr;
396  }
397 }
398 
402 {
403  debug() << "string_refinementt::check_axioms: ==============="
404  << "===========================================" << eom;
405  debug() << "string_refinementt::check_axioms: build the"
406  << " interpretation from the model of the prop_solver" << eom;
407  replace_mapt fmodel;
408 
409  for(auto it : generator.symbol_to_string)
410  {
411  string_exprt refined=it.second;
412  const exprt &econtent=refined.content();
413  const exprt &elength=refined.length();
414 
415  exprt len=get(elength);
416  exprt arr=get_array(econtent, len);
417 
418  fmodel[elength]=len;
419  fmodel[econtent]=arr;
420  debug() << it.first << "=" << from_expr(it.second)
421  << " of length " << from_expr(len) <<" := " << eom
422  << from_expr(get(econtent)) << eom
423  << string_of_array(econtent, len) << eom;
424  }
425 
426  for(auto it : generator.boolean_symbols)
427  {
428  debug() << "" << it.get_identifier() << " := "
429  << from_expr(get(it)) << eom;
430  fmodel[it]=get(it);
431  }
432 
433  for(auto it : generator.index_symbols)
434  {
435  debug() << "" << it.get_identifier() << " := "
436  << from_expr(get(it)) << eom;
437  fmodel[it]=get(it);
438  }
439 
440  // Maps from indexes of violated universal axiom to a witness of violation
441  std::map<size_t, exprt> violated;
442 
443  debug() << "there are " << universal_axioms.size()
444  << " universal axioms" << eom;
445  for(size_t i=0; i<universal_axioms.size(); i++)
446  {
447  const string_constraintt &axiom=universal_axioms[i];
448 
449  exprt negaxiom=and_exprt(axiom.premise(), not_exprt(axiom.body()));
450  replace_expr(fmodel, negaxiom);
451 
452  debug() << "negaxiom: " << from_expr(negaxiom) << eom;
453 
454  satcheck_no_simplifiert sat_check;
455  supert solver(ns, sat_check);
456  solver << negaxiom;
457 
458  switch(solver())
459  {
460  case decision_proceduret::D_SATISFIABLE:
461  {
462  exprt val=solver.get(axiom.univ_var());
463  violated[i]=val;
464  }
465  break;
466  case decision_proceduret::D_UNSATISFIABLE:
467  break;
468  default:
469  throw "failure in checking axiom";
470  }
471  }
472 
473  // tells whether one of the not_contains constraint can be violated
474  bool violated_not_contains=false;
475  debug() << "there are " << not_contains_axioms.size()
476  << " not_contains axioms" << eom;
477 
478  for(auto nc_axiom : not_contains_axioms)
479  {
480  typet index_type=nc_axiom.s0().length().type();
481  exprt zero=from_integer(0, index_type);
482  exprt witness=generator.get_witness_of(nc_axiom, zero);
483  exprt val=get(witness);
484  violated_not_contains=true;
485  }
486 
487  if(violated.empty() && !violated_not_contains)
488  {
489  debug() << "no violated property" << eom;
490  return true;
491  }
492  else
493  {
494  debug() << violated.size() << " string axioms can be violated" << eom;
495 
497  {
498  // Checking if the current solution satisfies the constraints
499  for(const auto &v : violated)
500  {
501  const exprt &val=v.second;
502  const string_constraintt &axiom=universal_axioms[v.first];
503 
504  exprt premise(axiom.premise());
505  exprt body(axiom.body());
506  implies_exprt instance(premise, body);
507  replace_expr(axiom.univ_var(), val, instance);
508  if(seen_instances.insert(instance).second)
509  add_lemma(instance);
510  else
511  debug() << "instance already seen" << eom;
512  }
513  }
514 
515  return false;
516  }
517 }
518 
524  const exprt &f) const
525 {
526  // number of time the leaf should be added (can be negative)
527  std::map<exprt, int> elems;
528 
529  std::list<std::pair<exprt, bool> > to_process;
530  to_process.push_back(std::make_pair(f, true));
531 
532  while(!to_process.empty())
533  {
534  exprt cur=to_process.back().first;
535  bool positive=to_process.back().second;
536  to_process.pop_back();
537  if(cur.id()==ID_plus)
538  {
539  to_process.push_back(std::make_pair(cur.op1(), positive));
540  to_process.push_back(std::make_pair(cur.op0(), positive));
541  }
542  else if(cur.id()==ID_minus)
543  {
544  to_process.push_back(std::make_pair(cur.op1(), !positive));
545  to_process.push_back(std::make_pair(cur.op0(), positive));
546  }
547  else if(cur.id()==ID_unary_minus)
548  {
549  to_process.push_back(std::make_pair(cur.op0(), !positive));
550  }
551  else
552  {
553  if(positive)
554  elems[cur]=elems[cur]+1;
555  else
556  elems[cur]=elems[cur]-1;
557  }
558  }
559  return elems;
560 }
561 
567  std::map<exprt, int> &m, bool negated) const
568 {
569  exprt sum=nil_exprt();
570  mp_integer constants=0;
572  if(m.empty())
573  return nil_exprt();
574  else
575  index_type=m.begin()->first.type();
576 
577  for(const auto &term : m)
578  {
579  // We should group constants together...
580  const exprt &t=term.first;
581  int second=negated?(-term.second):term.second;
582  if(t.id()==ID_constant)
583  {
584  std::string value(to_constant_expr(t).get_value().c_str());
585  constants+=binary2integer(value, true)*second;
586  }
587  else
588  {
589  switch(second)
590  {
591  case -1:
592  if(sum.is_nil())
593  sum=unary_minus_exprt(t);
594  else
595  sum=minus_exprt(sum, t);
596  break;
597 
598  case 1:
599  if(sum.is_nil())
600  sum=t;
601  else
602  sum=plus_exprt(sum, t);
603  break;
604 
605  default:
606  if(second>1)
607  {
608  for(int i=0; i<second; i++)
609  sum=plus_exprt(sum, t);
610  }
611  else
612  {
613  for(int i=0; i>second; i--)
614  sum=minus_exprt(sum, t);
615  }
616  }
617  }
618  }
619 
620  exprt index_const=from_integer(constants, index_type);
621  if(sum.is_not_nil())
622  return plus_exprt(sum, index_const);
623  else
624  return index_const;
625 }
626 
630 {
631  std::map<exprt, int> map=map_representation_of_sum(f);
632  return sum_over_map(map);
633 }
634 
643  const exprt &qvar, const exprt &val, const exprt &f)
644 {
645  exprt positive, negative;
646  // number of time the element should be added (can be negative)
647  // qvar has to be equal to val - f(0) if it appears positively in f
648  // (ie if f(qvar)=f(0) + qvar) and f(0) - val if it appears negatively
649  // in f. So we start by computing val - f(0).
650  std::map<exprt, int> elems=map_representation_of_sum(minus_exprt(val, f));
651 
652  // true if qvar appears negatively in f (positively in elems):
653  bool neg=false;
654 
655  auto it=elems.find(qvar);
656  assert(it!=elems.end());
657  if(it->second==1 || it->second==-1)
658  {
659  neg=(it->second==1);
660  }
661  else
662  {
663  assert(it->second==0);
664  debug() << "in string_refinementt::compute_inverse_function:"
665  << " warning: occurrences of qvar canceled out " << eom;
666  }
667 
668  elems.erase(it);
669  return sum_over_map(elems, neg);
670 }
671 
672 
673 
675 {
676 private:
677  const exprt &qvar_;
678 
679 public:
680  bool found;
681 
682  explicit find_qvar_visitort(const exprt &qvar): qvar_(qvar), found(false) {}
683 
684  void operator()(const exprt &expr)
685  {
686  if(expr==qvar_)
687  found=true;
688  }
689 };
690 
694 static bool find_qvar(const exprt index, const symbol_exprt &qvar)
695 {
696  find_qvar_visitort v2(qvar);
697  index.visit(v2);
698  return v2.found;
699 }
700 
705  const std::vector<string_constraintt> &string_axioms)
706 {
707  for(const auto &axiom : string_axioms)
708  initial_index_set(axiom);
709 }
710 
713 void string_refinementt::update_index_set(const std::vector<exprt> &cur)
714 {
715  for(const auto &axiom : cur)
716  update_index_set(axiom);
717 }
718 
723 {
724  symbol_exprt qvar=axiom.univ_var();
725  std::list<exprt> to_process;
726  to_process.push_back(axiom.body());
727 
728  while(!to_process.empty())
729  {
730  exprt cur=to_process.back();
731  to_process.pop_back();
732  if(cur.id()==ID_index)
733  {
734  const exprt &s=cur.op0();
735  const exprt &i=cur.op1();
736 
737  bool has_quant_var=find_qvar(i, qvar);
738 
739  // if cur is of the form s[i] and no quantified variable appears in i
740  if(!has_quant_var)
741  {
742  current_index_set[s].insert(i);
743  index_set[s].insert(i);
744  }
745  else
746  {
747  // otherwise we add k-1
748  exprt e(i);
749  minus_exprt kminus1(
750  axiom.upper_bound(),
751  from_integer(1, axiom.upper_bound().type()));
752  replace_expr(qvar, kminus1, e);
753  current_index_set[s].insert(e);
754  index_set[s].insert(e);
755  }
756  }
757  else
758  forall_operands(it, cur)
759  to_process.push_back(*it);
760  }
761 }
762 
766 {
767  std::list<exprt> to_process;
768  to_process.push_back(formula);
769 
770  while(!to_process.empty())
771  {
772  exprt cur=to_process.back();
773  to_process.pop_back();
774  if(cur.id()==ID_index)
775  {
776  const exprt &s=cur.op0();
777  const exprt &i=cur.op1();
778  assert(s.type().id()==ID_array);
779  exprt simplified=simplify_sum(i);
780  if(index_set[s].insert(simplified).second)
781  {
782  debug() << "adding to index set of " << from_expr(s)
783  << ": " << from_expr(simplified) << eom;
784  current_index_set[s].insert(simplified);
785  }
786  }
787  else
788  {
789  forall_operands(it, cur)
790  to_process.push_back(*it);
791  }
792  }
793 }
794 
795 
796 // Will be used to visit an expression and return the index used
797 // with the given char array
799 {
800 private:
801  const exprt &str_;
802 
803 public:
804  explicit find_index_visitort(const exprt &str): str_(str) {}
805 
806  void operator()(const exprt &expr)
807  {
808  if(expr.id()==ID_index)
809  {
810  const index_exprt &i=to_index_expr(expr);
811  if(i.array()==str_)
812  throw i.index();
813  }
814  }
815 };
816 
821 exprt find_index(const exprt &expr, const exprt &str)
822 {
823  find_index_visitort v1(str);
824  try
825  {
826  expr.visit(v1);
827  return nil_exprt();
828  }
829  catch (exprt i) { return i; }
830 }
831 
832 
841  const string_constraintt &axiom, const exprt &str, const exprt &val)
842 {
843  exprt idx=find_index(axiom.body(), str);
844  if(idx.is_nil())
845  return true_exprt();
846  if(!find_qvar(idx, axiom.univ_var()))
847  return true_exprt();
848 
849  exprt r=compute_inverse_function(axiom.univ_var(), val, idx);
850  implies_exprt instance(axiom.premise(), axiom.body());
851  replace_expr(axiom.univ_var(), r, instance);
852  // We are not sure the index set contains only positive numbers
853  exprt bounds=and_exprt(
854  axiom.univ_within_bounds(),
856  from_integer(0, val.type()), ID_le, val));
857  replace_expr(axiom.univ_var(), r, bounds);
858  return implies_exprt(bounds, instance);
859 }
860 
861 
863  const string_not_contains_constraintt &axiom, std::list<exprt> &new_lemmas)
864 {
865  exprt s0=axiom.s0();
866  exprt s1=axiom.s1();
867 
868  debug() << "instantiate not contains " << from_expr(s0) << " : "
869  << from_expr(s1) << eom;
870  expr_sett index_set0=index_set[to_string_expr(s0).content()];
872 
873  for(auto it0 : index_set0)
874  for(auto it1 : index_set1)
875  {
876  debug() << from_expr(it0) << " : " << from_expr(it1) << eom;
877  exprt val=minus_exprt(it0, it1);
878  exprt witness=generator.get_witness_of(axiom, val);
879  and_exprt prem_and_is_witness(
880  axiom.premise(),
881  equal_exprt(witness, it1));
882 
883  not_exprt differ(
884  equal_exprt(
885  to_string_expr(s0)[it0],
886  to_string_expr(s1)[it1]));
887  exprt lemma=implies_exprt(prem_and_is_witness, differ);
888 
889  new_lemmas.push_back(lemma);
890  // we put bounds on the witnesses:
891  // 0 <= v <= |s0| - |s1| ==> 0 <= v+w[v] < |s0| && 0 <= w[v] < |s1|
892  exprt zero=from_integer(0, val.type());
893  binary_relation_exprt c1(zero, ID_le, plus_exprt(val, witness));
895  (to_string_expr(s0).length(), ID_gt, plus_exprt(val, witness));
896  binary_relation_exprt c3(to_string_expr(s1).length(), ID_gt, witness);
897  binary_relation_exprt c4(zero, ID_le, witness);
898 
899  minus_exprt diff(
900  to_string_expr(s0).length(),
901  to_string_expr(s1).length());
902 
903  and_exprt premise(
904  binary_relation_exprt(zero, ID_le, val),
905  binary_relation_exprt(diff, ID_ge, val));
906  exprt witness_bounds=implies_exprt(
907  premise,
908  and_exprt(and_exprt(c1, c2), and_exprt(c3, c4)));
909  new_lemmas.push_back(witness_bounds);
910  }
911 }
The type of an expression.
Definition: type.h:20
virtual decision_proceduret::resultt dec_solve()
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
Boolean negation.
Definition: std_expr.h:2648
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
Definition: std_expr.h:3826
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
static int8_t r
Definition: irep_hash.h:59
BigInt mp_integer
Definition: mp_arith.h:19
bool is_nil() const
Definition: irep.h:103
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
bool is_not_nil() const
Definition: irep.h:104
std::list< symbol_exprt > boolean_symbols
std::map< exprt, int > map_representation_of_sum(const exprt &f) const
application of (mathematical) function
Definition: std_expr.h:3785
virtual literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:175
bool equality_propagation
Definition: prop_conv.h:107
exprt get_witness_of(const string_not_contains_constraintt &c, const exprt &univ_val) const
string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:133
#define CPROVER_PREFIX
std::vector< exprt > cur
exprt find_index(const exprt &expr, const exprt &str)
find an index used in the expression for str, for instance with arguments (str[k] == &#39;a&#39;) and str...
irep_idt mode
Language mode.
Definition: symbol.h:55
literalt convert_rest(const exprt &expr) override
Definition: bv_pointers.cpp:19
boolbv_widtht boolbv_width
Definition: boolbv.h:90
const string_not_contains_constraintt & to_string_not_contains_constraint(const exprt &expr)
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:673
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool boolbv_set_equality_to_true(const equal_exprt &expr)
add lemmas to the solver corresponding to the given equation
static symbol_exprt fresh_symbol(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
const symbol_exprt & univ_var() const
bool is_true() const
Definition: expr.cpp:133
virtual void set_frozen(literalt a) override
Definition: prop_conv.h:91
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
exprt univ_within_bounds() const
void add_instantiations()
compute the index set for all formulas, instantiate the formulas with the found indexes, and add them as lemmas.
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
const exprt & upper_bound() const
boolean implication
Definition: std_expr.h:1926
virtual bvt convert_symbol(const exprt &expr)
Definition: boolbv.cpp:378
void set_mode()
determine which language should be used
void l_set_to_true(literalt a)
Definition: prop.h:47
equality
Definition: std_expr.h:1082
bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
convert a positive integer expression to an unsigned int
Definition: arith_tools.cpp:95
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
find_index_visitort(const exprt &str)
std::map< irep_idt, string_exprt > symbol_to_string
const irep_idt & id() const
Definition: irep.h:189
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
void visit(class expr_visitort &visitor)
Definition: expr.cpp:483
An expression denoting infinity.
Definition: std_expr.h:3908
The boolean constant true.
Definition: std_expr.h:3742
exprt get_array(const exprt &arr, const exprt &size)
gets a model of an array and put it in a certain form
static bool is_unrefined_string_type(const typet &type)
std::set< exprt > expr_sett
const exprt & length() const
Definition: string_expr.h:35
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
The NIL expression.
Definition: std_expr.h:3764
const refined_string_typet & to_refined_string_type(const typet &type)
literalt convert_rest(const exprt &expr)
if the expression is a function application, we convert it using our own convert_function_application...
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:121
boolean AND
Definition: std_expr.h:1852
static bool find_qvar(const exprt index, const symbol_exprt &qvar)
looks for the symbol and return true if it is found
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
string_exprt find_or_add_string_of_symbol(const symbol_exprt &sym)
if a symbol represent a string is present in the symbol_to_string table, returns the corresponding st...
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bvt convert_bool_bv(const exprt &boole, const exprt &orig)
fills as many 0 as necessary in the bit vectors to have the right width
exprt simplify_sum(const exprt &f) const
string_refinementt(const namespacet &_ns, propt &_prop, unsigned refinement_bound)
bool check_axioms()
return true if the current model satisfies all the axioms
void update_index_set(const exprt &formula)
add to the index set all the indices that appear in the formula
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:702
const namespacet & ns
array constructor from single element
Definition: std_expr.h:1252
virtual bvt convert_function_application(const function_application_exprt &expr)
generate an expression, add lemmas stating that this expression corresponds to the result of the give...
exprt compute_inverse_function(const exprt &qvar, const exprt &val, const exprt &f)
exprt instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val)
const typet & get_index_type() const
bitvector_typet index_type()
Definition: c_types.cpp:15
The unary minus expression.
Definition: std_expr.h:346
TO_BE_DOCUMENTED.
Definition: prop.h:22
std::string string_of_array(const exprt &arr, const exprt &size) const
convert the content of a string to a more readable representation.
string_constraint_generatort generator
void initial_index_set(const string_constraintt &axiom)
add to the index set all the indices that appear in the formula and the upper bound minus one ...
String support via creating string constraints and progressively instantiating the universal constrai...
literalt const_literal(bool value)
Definition: literal.h:187
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:78
mstreamt & debug()
Definition: message.h:253
void set_string_symbol_equal_to_expr(const symbol_exprt &sym, const exprt &str)
add a correspondence to make sure the symbol points to the same string as the second argument ...
exprt get(const exprt &expr) const override
Definition: boolbv_get.cpp:21
std::map< exprt, expr_sett > current_index_set
exprt & index()
Definition: std_expr.h:1208
#define MAX_CONCRETE_STRING_SIZE
Base class for all expressions.
Definition: expr.h:46
void display_index_set()
display the current index set, for debugging
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
decision_proceduret::resultt dec_solve()
use a refinement loop to instantiate universal axioms, call the sat solver, and instantiate more inde...
const exprt & content() const
Definition: string_expr.h:39
Operator to update elements in structs and arrays.
Definition: std_expr.h:2861
void operator()(const exprt &expr)
literalt neg(literalt a)
Definition: literal.h:192
std::list< symbol_exprt > index_symbols
exprt sum_over_map(std::map< exprt, int > &m, bool negated=false) const
void instantiate_not_contains(const string_not_contains_constraintt &axiom, std::list< exprt > &new_lemmas)
void operator()(const exprt &expr)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition: replace_expr.h:20
arrays with given size
Definition: std_types.h:901
binary minus
Definition: std_expr.h:758
Expression to hold a symbol (variable)
Definition: std_expr.h:82
int8_t s1
Definition: bytecode_info.h:59
std::vector< string_not_contains_constraintt > not_contains_axioms
dstringt irep_idt
Definition: irep.h:32
boolbv_mapt map
Definition: boolbv.h:99
std::map< exprt, expr_sett > index_set
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
const typet & subtype() const
Definition: type.h:31
const string_constraintt & to_string_constraint(const exprt &expr)
std::map< string_not_contains_constraintt, symbol_exprt > witness
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const exprt & premise() const
bool empty() const
Definition: dstring.h:61
std::vector< string_constraintt > universal_axioms
exprt & array()
Definition: std_expr.h:1198
void add_lemma(const exprt &lemma, bool add_to_index_set=true)
add the given lemma to the solver
bitvector_typet char_type()
Definition: c_types.cpp:113
std::vector< literalt > bvt
Definition: literal.h:197
const exprt & body() const
const string_exprt & s0() const
const string_exprt & s1() const
array index operator
Definition: std_expr.h:1170
virtual bvt convert_symbol(const exprt &expr)
if the expression as string type, look up for the string in the list of string symbols that we mainta...
find_qvar_visitort(const exprt &qvar)