cprover
string_constraint.h File Reference

Defines string constraints. More...

Include dependency graph for string_constraint.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  string_constraintt
 
class  string_not_contains_constraintt
 

Functions

const string_constrainttto_string_constraint (const exprt &expr)
 
string_constrainttto_string_constraint (exprt &expr)
 
const string_not_contains_constrainttto_string_not_contains_constraint (const exprt &expr)
 
string_not_contains_constrainttto_string_not_contains_constraint (exprt &expr)
 

Detailed Description

Defines string constraints.

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

Definition in file string_constraint.h.

Function Documentation

◆ to_string_constraint() [1/2]

const string_constraintt& to_string_constraint ( const exprt expr)
inline

Definition at line 105 of file string_constraint.h.

References irept::id(), and exprt::operands().

Referenced by string_refinementt::dec_solve().

◆ to_string_constraint() [2/2]

string_constraintt& to_string_constraint ( exprt expr)
inline

Definition at line 111 of file string_constraint.h.

References irept::id(), and exprt::operands().

◆ to_string_not_contains_constraint() [1/2]

const string_not_contains_constraintt& to_string_not_contains_constraint ( const exprt expr)
inline

Definition at line 175 of file string_constraint.h.

References irept::id(), and exprt::operands().

Referenced by string_refinementt::dec_solve().

◆ to_string_not_contains_constraint() [2/2]

string_not_contains_constraintt& to_string_not_contains_constraint ( exprt expr)
inline

Definition at line 183 of file string_constraint.h.

References irept::id(), and exprt::operands().