CBMC
Public Member Functions | Public Attributes | Related Functions | List of all members
string_constraintt Class Referencefinal

#include <string_constraint.h>

+ Collaboration diagram for string_constraintt:

Public Member Functions

 string_constraintt (const symbol_exprt &_univ_var, const exprt &lower_bound, const exprt &upper_bound, const exprt &body, message_handlert &message_handler)
 
 string_constraintt (symbol_exprt univ_var, exprt upper_bound, exprt body, message_handlert &message_handler)
 
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...
 

Detailed Description

Universally quantified string constraint

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:

  • The predicate PI , called the index guard, must follow the grammar
    • \(iguard : iguard \land iguard \mid iguard \lor iguard \mid iterm \le iterm \mid iterm = iterm \)
    • \(iterm : integer\_constant1 \times i + integer\_constant2 \)
  • The predicate PV 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 55 of file string_constraint.h.

Constructor & Destructor Documentation

◆ string_constraintt() [1/2]

string_constraintt::string_constraintt ( const symbol_exprt &  _univ_var,
const exprt &  lower_bound,
const exprt &  upper_bound,
const exprt &  body,
message_handlert &  message_handler 
)

Definition at line 34 of file string_constraint.cpp.

◆ string_constraintt() [2/2]

string_constraintt::string_constraintt ( symbol_exprt  univ_var,
exprt  upper_bound,
exprt  body,
message_handlert &  message_handler 
)
inline

Definition at line 73 of file string_constraint.h.

Member Function Documentation

◆ negation()

exprt string_constraintt::negation ( ) const
inline

Definition at line 101 of file string_constraint.h.

◆ replace_expr()

void string_constraintt::replace_expr ( union_find_replacet &  replace_map)
inline

Definition at line 94 of file string_constraint.h.

◆ univ_within_bounds()

exprt string_constraintt::univ_within_bounds ( ) const
inline

Definition at line 87 of file string_constraint.h.

Friends And Related Function Documentation

◆ array_index_mapt

typedef std::map<exprt, std::vector<exprt> > array_index_mapt
related

Definition at line 1925 of file string_refinement.cpp.

◆ gather_indices()

static array_index_mapt gather_indices ( const exprt &  expr)
related

Definition at line 1928 of file string_refinement.cpp.

◆ is_linear_arithmetic_expr()

static bool is_linear_arithmetic_expr ( const exprt &  expr,
const symbol_exprt &  var 
)
related
Parameters
expran expression
vara symbol
Returns
Boolean telling whether expr is a linear function of var.

Definition at line 1951 of file string_refinement.cpp.

◆ is_valid_string_constraint()

static bool is_valid_string_constraint ( messaget::mstreamt &  stream,
const namespacet &  ns,
const string_constraintt &  constraint 
)
related

Checks the data invariant for string_constraintt.

Parameters
streammessage stream
nsnamespace
[in]constraintthe string constraint to check
Returns
whether the constraint satisfies the invariant

Definition at line 1997 of file string_refinement.cpp.

◆ universal_only_in_index()

static bool universal_only_in_index ( const string_constraintt &  constr)
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.

Parameters
[in]constrThe string constraint to check
Returns
true if the universal variable only occurs in index expressions, false otherwise.

Definition at line 1977 of file string_refinement.cpp.

Member Data Documentation

◆ body

exprt string_constraintt::body

Definition at line 63 of file string_constraint.h.

◆ lower_bound

exprt string_constraintt::lower_bound

Definition at line 61 of file string_constraint.h.

◆ univ_var

symbol_exprt string_constraintt::univ_var

Definition at line 60 of file string_constraint.h.

◆ upper_bound

exprt string_constraintt::upper_bound

Definition at line 62 of file string_constraint.h.

The documentation for this class was generated from the following files: