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 string_constraint_generatort &generator)
25 {
26  std::vector<exprt> lemmas;
27 
28  const array_string_exprt s0 = axiom.s0();
29  const array_string_exprt s1 = axiom.s1();
30 
31  for(const auto &pair : index_pairs)
32  {
33  // We have s0[x+f(x)] and s1[f(x)], so to have i0 indexing s0 and i1
34  // indexing s1, we need x = i0 - i1 and f(i0 - i1) = f(x) = i1.
35  const exprt &i0=pair.first;
36  const exprt &i1=pair.second;
37  const minus_exprt val(i0, i1);
38  const and_exprt universal_bound(
39  binary_relation_exprt(axiom.univ_lower_bound(), ID_le, val),
40  binary_relation_exprt(axiom.univ_upper_bound(), ID_gt, val));
41  const exprt f=generator.get_witness_of(axiom, val);
42  const equal_exprt relevancy(f, i1);
43  const and_exprt premise(relevancy, axiom.premise(), universal_bound);
44 
45  const notequal_exprt differ(s0[i0], s1[i1]);
46  const and_exprt existential_bound(
47  binary_relation_exprt(axiom.exists_lower_bound(), ID_le, i1),
48  binary_relation_exprt(axiom.exists_upper_bound(), ID_gt, i1));
49  const and_exprt body(differ, existential_bound);
50 
51  const implies_exprt lemma(premise, body);
52  lemmas.push_back(lemma);
53  }
54 
55  return lemmas;
56 }
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const exprt & univ_lower_bound() const
exprt get_witness_of(const string_not_contains_constraintt &c, const exprt &univ_val) const
boolean implication
Definition: std_expr.h:2339
equality
Definition: std_expr.h:1354
const exprt & exists_lower_bound() const
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...
Constraints to encode non containement of strings.
boolean AND
Definition: std_expr.h:2255
inequality
Definition: std_expr.h:1406
const exprt & exists_upper_bound() const
Base class for all expressions.
Definition: expr.h:42
const exprt & univ_upper_bound() const
binary minus
Definition: std_expr.h:959
int8_t s1
Definition: bytecode_info.h:59
const array_string_exprt & s0() const
const array_string_exprt & s1() const