cprover
string_constraint_instantiation.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Defines related function for string constraints.
4 
5 Author: Jesse Sigal, jesse.sigal@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
13 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
14 
17 
18 std::vector<exprt> instantiate_not_contains(
20  const std::set<std::pair<exprt, exprt>> &index_pairs,
21  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
22  &witnesses);
23 
24 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
Generates string constraints to link results from string functions with their arguments.
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 string constraints.
Constraints to encode non containement of strings.