23 const std::set<std::pair<exprt, exprt>> &index_pairs,
24 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
27 std::vector<exprt> lemmas;
32 for(
const auto &pair : index_pairs)
36 const exprt &i0=pair.first;
37 const exprt &i1=pair.second;
50 const and_exprt body(differ, existential_bound);
53 lemmas.push_back(lemma);
A base class for relations, i.e., binary predicates.
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...
Defines related function for string constraints.
Constraints to encode non containement of strings.
Base class for all expressions.