Defines string constraints. More...

#include <util/format_expr.h>
#include <util/string_expr.h>
#include <util/union_find_replace.h>

Include dependency graph for string_constraint.h:

This graph shows which files directly or indirectly include this file:

Classes
class	string_constraintt

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

struct	std::hash< string_not_contains_constraintt >

Functions
std::string	to_string (const string_constraintt &expr)
	Used for debug printing. More...

std::string	to_string (const string_not_contains_constraintt &expr)
	Used for debug printing. More...

void	replace (const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)

bool	operator== (const string_not_contains_constraintt &left, const string_not_contains_constraintt &right)

Detailed Description

Defines string constraints.

These are formulas talking about strings. We implemented two forms of constraints: string_constraintt are formulas of the form \(\forall univ\_var \in [lb,ub[. prem => body\), and not_contains_constraintt of the form: \(\forall x \in [lb,ub[. p(x) => \exists y \in [lb,ub[. s1[x+y] \ne s2[y]\).

Definition in file string_constraint.h.

Function Documentation

◆ operator==()

bool operator==	(	const string_not_contains_constraintt &	left,
		const string_not_contains_constraintt &	right
	)

Definition at line 83 of file string_constraint.cpp.

◆ replace()

void replace	(	const union_find_replacet &	replace_map,
		string_not_contains_constraintt &	constraint
	)

Definition at line 70 of file string_constraint.cpp.

◆ to_string() [1/2]

std::string to_string ( const string_constraintt & expr )

inline

Used for debug printing.

Parameters

expr	constraint to render

Returns: rendered string

Definition at line 110 of file string_constraint.h.

◆ to_string() [2/2]

std::string to_string ( const string_not_contains_constraintt & expr )

Used for debug printing.

Parameters

[in] expr constraint to render

Returns: rendered string

Definition at line 58 of file string_constraint.cpp.