string_constraint.cpp File Reference

#include "string_constraint.h"
#include <util/namespace.h>
#include <util/symbol_table.h>
#include <solvers/flattening/bv_pointers.h>
#include <solvers/sat/satcheck.h>

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

expr	the expression to check for negativity
message_handler	message 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]

expr

constraint to render

Returns

rendered string

Definition at line 58 of file string_constraint.cpp.