cprover
string_constraintt Class Referencefinal

Universally quantified string constraint

More...

#include <string_constraint.h>

Collaboration diagram for string_constraintt:
[legend]

Public Member Functions

 string_constraintt ()=delete
 
 string_constraintt (symbol_exprt _univ_var, exprt lower_bound, exprt upper_bound, 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 58 of file string_constraint.h.

Constructor & Destructor Documentation

◆ string_constraintt() [1/3]

string_constraintt::string_constraintt ( )
delete

◆ string_constraintt() [2/3]

string_constraintt::string_constraintt ( symbol_exprt  _univ_var,
exprt  lower_bound,
exprt  upper_bound,
exprt  body 
)
inline

Definition at line 70 of file string_constraint.h.

◆ string_constraintt() [3/3]

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

Definition at line 83 of file string_constraint.h.

Member Function Documentation

◆ negation()

exprt string_constraintt::negation ( ) const
inline

Definition at line 106 of file string_constraint.h.

References body, and univ_within_bounds().

Referenced by check_axioms().

◆ replace_expr()

void string_constraintt::replace_expr ( union_find_replacet replace_map)
inline

◆ univ_within_bounds()

exprt string_constraintt::univ_within_bounds ( ) const
inline

Definition at line 92 of file string_constraint.h.

References lower_bound, univ_var, and upper_bound.

Referenced by check_axioms(), and negation().

Friends And Related Function Documentation

◆ array_index_mapt

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

Definition at line 2098 of file string_refinement.cpp.

◆ gather_indices()

static array_index_mapt gather_indices ( const exprt expr)
related

◆ 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 2124 of file string_refinement.cpp.

References exprt::depth_begin(), exprt::depth_end(), and find_qvar().

Referenced by is_valid_string_constraint().

◆ 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 2170 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().

◆ 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]exprThe string constraint to check
Returns
true if the universal variable only occurs in index expressions, false otherwise.

Definition at line 2150 of file string_refinement.cpp.

References body, exprt::depth_begin(), exprt::depth_end(), and univ_var.

Referenced by is_valid_string_constraint().

Member Data Documentation

◆ body

◆ lower_bound

exprt string_constraintt::lower_bound

◆ univ_var

◆ upper_bound

exprt string_constraintt::upper_bound

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