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 
15 #include "string_constraint.h"
17 
28  const string_constraintt &axiom,
29  const exprt &str,
30  const exprt &val);
31 
32 std::vector<exprt> instantiate_not_contains(
34  const std::set<std::pair<exprt, exprt>> &index_pairs,
35  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
36  &witnesses);
37 
42 {
43 public:
46  explicit linear_functiont(const exprt &f);
47 
49  void add(const linear_functiont &other);
50 
53  exprt to_expr(bool negated = false) const;
54 
59  static exprt solve(linear_functiont f, const exprt &var, const exprt &val);
60 
62  std::string format();
63 
64 private:
66  std::unordered_map<exprt, mp_integer, irep_hash> coefficients;
68 };
69 
70 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
linear_functiont::constant_coefficient
mp_integer constant_coefficient
Definition: string_constraint_instantiation.h:65
linear_functiont::format
std::string format()
Format the linear function as a string, can be used for debugging.
Definition: string_constraint_instantiation.cpp:159
typet
The type of an expression, extends irept.
Definition: type.h:29
linear_functiont::add
void add(const linear_functiont &other)
Make this function the sum of the current function with other.
Definition: string_constraint_instantiation.cpp:94
string_constraintt
Definition: string_constraint.h:60
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
linear_functiont::coefficients
std::unordered_map< exprt, mp_integer, irep_hash > coefficients
Definition: string_constraint_instantiation.h:66
linear_functiont::linear_functiont
linear_functiont(const exprt &f)
Put an expression f composed of additions and subtractions into its cannonical representation.
Definition: string_constraint_instantiation.cpp:53
exprt
Base class for all expressions.
Definition: expr.h:53
linear_functiont
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given...
Definition: string_constraint_instantiation.h:42
instantiate
exprt instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val)
Substitute qvar the universally quantified variable of axiom, by an index val, in axiom,...
Definition: string_constraint_instantiation.cpp:183
linear_functiont::to_expr
exprt to_expr(bool negated=false) const
Definition: string_constraint_instantiation.cpp:102
linear_functiont::solve
static exprt solve(linear_functiont f, const exprt &var, const exprt &val)
Return an expression y such that f(var <- y) = val.
Definition: string_constraint_instantiation.cpp:139
string_constraint.h
Defines string constraints.
string_refinementt::instantiate_not_contains
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...
Definition: string_constraint_instantiation.cpp:211
string_not_contains_constraintt
Constraints to encode non containement of strings.
Definition: string_constraint.h:127
string_constraint_generator.h
Generates string constraints to link results from string functions with their arguments.
linear_functiont::type
typet type
Definition: string_constraint_instantiation.h:67