cprover
string_constraint_instantiation.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Defines functions related to string constraints.
4 
5 Author: Jesse Sigal, jesse.sigal@diffblue.com
6 
7 \*******************************************************************/
8 
11 
13 
21 std::vector<exprt> instantiate_not_contains(
23  const std::set<std::pair<exprt, exprt>> &index_pairs,
24  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
25  &witnesses)
26 {
27  std::vector<exprt> lemmas;
28 
29  const array_string_exprt s0 = axiom.s0;
30  const array_string_exprt s1 = axiom.s1;
31 
32  for(const auto &pair : index_pairs)
33  {
34  // We have s0[x+f(x)] and s1[f(x)], so to have i0 indexing s0 and i1
35  // indexing s1, we need x = i0 - i1 and f(i0 - i1) = f(x) = i1.
36  const exprt &i0=pair.first;
37  const exprt &i1=pair.second;
38  const minus_exprt val(i0, i1);
39  const and_exprt universal_bound(
40  binary_relation_exprt(axiom.univ_lower_bound, ID_le, val),
41  binary_relation_exprt(axiom.univ_upper_bound, ID_gt, val));
42  const exprt f = index_exprt(witnesses.at(axiom), val);
43  const equal_exprt relevancy(f, i1);
44  const and_exprt premise(relevancy, axiom.premise, universal_bound);
45 
46  const notequal_exprt differ(s0[i0], s1[i1]);
47  const and_exprt existential_bound(
48  binary_relation_exprt(axiom.exists_lower_bound, ID_le, i1),
49  binary_relation_exprt(axiom.exists_upper_bound, ID_gt, i1));
50  const and_exprt body(differ, existential_bound);
51 
52  const implies_exprt lemma(premise, body);
53  lemmas.push_back(lemma);
54  }
55 
56  return lemmas;
57 }
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
std::vector< exprt > instantiate_not_contains(const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt >> &index_pairs, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
Boolean implication.
Definition: std_expr.h:2485
Equality.
Definition: std_expr.h:1484
Defines related function for string constraints.
Constraints to encode non containement of strings.
Boolean AND.
Definition: std_expr.h:2409
Disequality.
Definition: std_expr.h:1545
Base class for all expressions.
Definition: expr.h:54
Binary minus.
Definition: std_expr.h:1106
int8_t s1
Definition: bytecode_info.h:59
Array index operator.
Definition: std_expr.h:1595