string_not_contains_constraintt Struct Reference

Constraints to encode non containement of strings. More...

#include <string_constraint.h>

Collaboration diagram for string_not_contains_constraintt:

Public Attributes
exprt	univ_lower_bound
exprt	univ_upper_bound
exprt	premise
exprt	exists_lower_bound
exprt	exists_upper_bound
array_string_exprt	s0
array_string_exprt	s1

Detailed Description

Constraints to encode non containement of strings.

string_not contains_constraintt are formulas of the form:

forall x in [univ_lower_bound, univ_upper_bound[.
  premise(x) =>
    exists y in [exists_lower_bound, exists_upper_bound[. s0[x+y] != s1[y]

Definition at line 126 of file string_constraint.h.

Member Data Documentation

exists_lower_bound

exprt string_not_contains_constraintt::exists_lower_bound

Definition at line 131 of file string_constraint.h.

exists_upper_bound

exprt string_not_contains_constraintt::exists_upper_bound

Definition at line 132 of file string_constraint.h.

premise

exprt string_not_contains_constraintt::premise

Definition at line 130 of file string_constraint.h.

s0

array_string_exprt string_not_contains_constraintt::s0

Definition at line 133 of file string_constraint.h.

s1

array_string_exprt string_not_contains_constraintt::s1

Definition at line 134 of file string_constraint.h.

univ_lower_bound

exprt string_not_contains_constraintt::univ_lower_bound

Definition at line 128 of file string_constraint.h.

univ_upper_bound

exprt string_not_contains_constraintt::univ_upper_bound

Definition at line 129 of file string_constraint.h.

---

The documentation for this struct was generated from the following file:

• /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/strings/string_constraint.h