cprover
|
#include <string_constraint.h>
Public Member Functions | |
string_constraintt ()=delete | |
string_constraintt (const symbol_exprt &_univ_var, const exprt &lower_bound, const exprt &upper_bound, const exprt &body) | |
string_constraintt (symbol_exprt univ_var, exprt upper_bound, exprt body) | |
exprt | univ_within_bounds () const |
void | replace_expr (union_find_replacet &replace_map) |
exprt | negation () const |
Public Attributes | |
symbol_exprt | univ_var |
exprt | lower_bound |
exprt | upper_bound |
exprt | body |
Related Functions | |
(Note that these are not member functions.) | |
typedef std::map< exprt, std::vector< exprt > > | array_index_mapt |
static array_index_mapt | gather_indices (const exprt &expr) |
static bool | is_linear_arithmetic_expr (const exprt &expr, const symbol_exprt &var) |
static bool | universal_only_in_index (const string_constraintt &constr) |
The universally quantified variable is only allowed to occur in index expressions in the body of a string constraint. More... | |
static bool | is_valid_string_constraint (messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint) |
Checks the data invariant for string_constraintt. More... | |
This represents a universally quantified string constraint as laid out in DOI: 10.1007/978-3-319-03077-7. The paper seems to specify a universal constraint as follows.
A universal constraint is of the form \( \forall i.\ PI(i) \Rightarrow PV(i)\) where \(PI\) and \(PV\) satisfies the following conditions:
PI
, called the index guard, must follow the grammarPV
is called the value constraint. The index variable i
can only be used in array read expressions of the form a[i]
. ie. PV
is of the form \(P'(s_0[f_0(i)],\ldots, s_k[f_k(i)] )\), moreover when focusing on one specific string, all indices are the same [stated in a roundabout manner]. \(L(n)\) and \(P(n, s_0,\ldots, s_k)\) may contain other (free) variables, but in \(P\), \(n\) can only occur as an argument to an \(f\) [explicitly stated, implied].Definition at line 58 of file string_constraint.h.
|
delete |
string_constraintt::string_constraintt | ( | const symbol_exprt & | _univ_var, |
const exprt & | lower_bound, | ||
const exprt & | upper_bound, | ||
const exprt & | body | ||
) |
Definition at line 30 of file string_constraint.cpp.
References cannot_be_neg(), INVARIANT, lower_bound, irept::pretty(), and upper_bound.
|
inline |
Definition at line 77 of file string_constraint.h.
|
inline |
Definition at line 100 of file string_constraint.h.
References body, and univ_within_bounds().
Referenced by check_axioms().
|
inline |
Definition at line 93 of file string_constraint.h.
References body, lower_bound, union_find_replacet::replace_expr(), and upper_bound.
|
inline |
Definition at line 86 of file string_constraint.h.
References lower_bound, univ_var, and upper_bound.
Referenced by check_axioms(), and negation().
|
related |
Definition at line 2070 of file string_refinement.cpp.
|
related |
Definition at line 2073 of file string_refinement.cpp.
References index_exprt::array(), exprt::depth_begin(), exprt::depth_end(), expr_try_dynamic_cast(), and index_exprt::index().
Referenced by is_valid_string_constraint().
|
related |
expr | an expression |
var | a symbol |
expr
is a linear function of var
. Definition at line 2096 of file string_refinement.cpp.
References exprt::depth_begin(), exprt::depth_end(), and find_qvar().
Referenced by is_valid_string_constraint().
|
related |
Checks the data invariant for string_constraintt.
stream | message stream | |
ns | namespace | |
[in] | constraint | the string constraint to check |
Definition at line 2142 of file string_refinement.cpp.
References body, messaget::eom(), format(), gather_indices(), exprt::is_false(), is_linear_arithmetic_expr(), simplify_expr(), to_string(), univ_var, and universal_only_in_index().
|
related |
The universally quantified variable is only allowed to occur in index expressions in the body of a string constraint.
This function returns true if this is the case and false otherwise.
[in] | expr | The string constraint to check |
Definition at line 2122 of file string_refinement.cpp.
References body, exprt::depth_begin(), exprt::depth_end(), and univ_var.
Referenced by is_valid_string_constraint().
exprt string_constraintt::body |
Definition at line 66 of file string_constraint.h.
Referenced by check_axioms(), initial_index_set(), instantiate(), is_valid_string_constraint(), negation(), replace_expr(), to_string(), and universal_only_in_index().
exprt string_constraintt::lower_bound |
Definition at line 64 of file string_constraint.h.
Referenced by check_axioms(), instantiate(), replace_expr(), string_constraintt(), to_string(), and univ_within_bounds().
symbol_exprt string_constraintt::univ_var |
Definition at line 63 of file string_constraint.h.
Referenced by check_axioms(), initial_index_set(), instantiate(), is_valid_string_constraint(), to_string(), univ_within_bounds(), and universal_only_in_index().
exprt string_constraintt::upper_bound |
Definition at line 65 of file string_constraint.h.
Referenced by check_axioms(), initial_index_set(), instantiate(), replace_expr(), string_constraintt(), to_string(), and univ_within_bounds().