cprover
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:

Definition at line 125 of file string_constraint.h.

Member Data Documentation

◆ exists_lower_bound

exprt string_not_contains_constraintt::exists_lower_bound

Definition at line 130 of file string_constraint.h.

◆ exists_upper_bound

exprt string_not_contains_constraintt::exists_upper_bound

Definition at line 131 of file string_constraint.h.

◆ premise

exprt string_not_contains_constraintt::premise

Definition at line 129 of file string_constraint.h.

◆ s0

array_string_exprt string_not_contains_constraintt::s0

Definition at line 132 of file string_constraint.h.

◆ s1

array_string_exprt string_not_contains_constraintt::s1

Definition at line 133 of file string_constraint.h.

◆ univ_lower_bound

exprt string_not_contains_constraintt::univ_lower_bound

Definition at line 127 of file string_constraint.h.

◆ univ_upper_bound

exprt string_not_contains_constraintt::univ_upper_bound

Definition at line 128 of file string_constraint.h.


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