Loading...

Searching...

No Matches

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.

std::string to_string (const string_not_contains_constraintt &expr)

Used for debug printing.

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.