23 const std::set<std::pair<exprt, exprt>> &index_pairs,
26 std::vector<exprt> lemmas;
31 for(
const auto &pair : index_pairs)
35 const exprt &i0=pair.first;
36 const exprt &i1=pair.second;
49 const and_exprt body(differ, existential_bound);
52 lemmas.push_back(lemma);
A generic base class for relations, i.e., binary predicates.
const exprt & univ_lower_bound() const
exprt get_witness_of(const string_not_contains_constraintt &c, const exprt &univ_val) const
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.
const exprt & premise() const
const exprt & exists_upper_bound() const
Base class for all expressions.
const exprt & univ_upper_bound() const
const array_string_exprt & s0() const
const array_string_exprt & s1() const