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 Symbol Documentation

◆ array_index_mapt

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

◆ gather_indices()

static array_index_mapt gather_indices ( const exprt & expr )

◆ is_linear_arithmetic_expr()

static bool is_linear_arithmetic_expr ( const exprt & expr,

const symbol_exprt & var

)

Parameters: expr an expression

var a symbol

Returns: Boolean telling whether expr is a linear function of var.

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

)

Parameters: stream message stream

ns namespace

[in] constraint the string constraint to check

Returns: whether the constraint satisfies the invariant

Definition at line 2008 of file string_refinement.cpp.

◆ universal_only_in_index()

static bool universal_only_in_index ( const string_constraintt & constr )

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

Parameters: [in] constr The string constraint to check

Returns: true if the universal variable only occurs in index expressions, false otherwise.

Definition at line 1988 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:

/home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint.h
/home/runner/work/cbmc/cbmc/src/solvers/strings/string_refinement.cpp
/home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint.cpp