cprover
|
Defines string constraints. More...
#include <langapi/language_ui.h>
#include <solvers/refinement/bv_refinement.h>
#include <solvers/refinement/refined_string_type.h>
Go to the source code of this file.
Classes | |
class | string_constraintt |
class | string_not_contains_constraintt |
Functions | |
const string_constraintt & | to_string_constraint (const exprt &expr) |
string_constraintt & | to_string_constraint (exprt &expr) |
const string_not_contains_constraintt & | to_string_not_contains_constraint (const exprt &expr) |
string_not_contains_constraintt & | to_string_not_contains_constraint (exprt &expr) |
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.
|
inline |
Definition at line 105 of file string_constraint.h.
References irept::id(), and exprt::operands().
Referenced by string_refinementt::dec_solve().
|
inline |
Definition at line 111 of file string_constraint.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 175 of file string_constraint.h.
References irept::id(), and exprt::operands().
Referenced by string_refinementt::dec_solve().
|
inline |
Definition at line 183 of file string_constraint.h.
References irept::id(), and exprt::operands().