string_constraintt Class Referencefinal

Universally quantified string constraint


#include <string_constraint.h>

+ Collaboration diagram for string_constraintt:

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...

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 59 of file string_constraint.h.

Constructor & Destructor Documentation

◆ string_constraintt() [1/3]

string_constraintt::string_constraintt ( )

◆ string_constraintt() [2/3]

string_constraintt::string_constraintt ( const symbol_exprt _univ_var,
const exprt lower_bound,
const exprt upper_bound,
const exprt body 

Definition at line 32 of file string_constraint.cpp.

◆ string_constraintt() [3/3]

string_constraintt::string_constraintt ( symbol_exprt  univ_var,
exprt  upper_bound,
exprt  body 

Definition at line 78 of file string_constraint.h.

Member Function Documentation

◆ negation()

exprt string_constraintt::negation ( ) const

Definition at line 101 of file string_constraint.h.

◆ replace_expr()

void string_constraintt::replace_expr ( union_find_replacet replace_map)

Definition at line 94 of file string_constraint.h.

◆ univ_within_bounds()

exprt string_constraintt::univ_within_bounds ( ) const

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

Definition at line 1928 of file string_refinement.cpp.

◆ gather_indices()

static array_index_mapt gather_indices ( const exprt expr)

Definition at line 1931 of file string_refinement.cpp.

◆ is_linear_arithmetic_expr()

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

Definition at line 1954 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 

Checks the data invariant for string_constraintt.

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

Definition at line 2000 of file string_refinement.cpp.

◆ universal_only_in_index()

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.

This function returns true if this is the case and false otherwise.

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

Definition at line 1980 of file string_refinement.cpp.

Member Data Documentation

◆ body

exprt string_constraintt::body

Definition at line 67 of file string_constraint.h.

◆ lower_bound

exprt string_constraintt::lower_bound

Definition at line 65 of file string_constraint.h.

◆ univ_var

symbol_exprt string_constraintt::univ_var

Definition at line 64 of file string_constraint.h.

◆ upper_bound

exprt string_constraintt::upper_bound

Definition at line 66 of file string_constraint.h.

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