CBMC
string_constraint.cpp File Reference
+ Include dependency graph for string_constraint.cpp:

Go to the source code of this file.

Functions

static bool cannot_be_neg (const exprt &expr, message_handlert &message_handler)
 Runs a solver instance to verify whether an expression can only be non-negative. 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)
 

Function Documentation

◆ cannot_be_neg()

static bool cannot_be_neg ( const exprt expr,
message_handlert message_handler 
)
static

Runs a solver instance to verify whether an expression can only be non-negative.

Parameters
exprthe expression to check for negativity
message_handlermessage handler
Returns
true if expr < 0 is unsatisfiable, false otherwise

Definition at line 22 of file string_constraint.cpp.

◆ 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()

std::string to_string ( const string_not_contains_constraintt expr)

Used for debug printing.

Parameters
[in]exprconstraint to render
Returns
rendered string

Definition at line 58 of file string_constraint.cpp.