cprover
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)
 Runs a solver instance to verify whether an expression can only be. More...
 

Function Documentation

◆ cannot_be_neg()

static bool cannot_be_neg ( const exprt expr)
static

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

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

Definition at line 18 of file string_constraint.cpp.

References decision_proceduret::D_UNSATISFIABLE, from_integer(), solver(), and exprt::type().

Referenced by string_constraintt::string_constraintt().