cprover
|
String support via creating string constraints and progressively instantiating the universal constraints as needed. More...
#include <util/string_expr.h>
#include <solvers/refinement/string_constraint.h>
#include <solvers/refinement/string_constraint_generator.h>
Go to the source code of this file.
Classes | |
class | string_refinementt |
Macros | |
#define | MAX_CONCRETE_STRING_SIZE 500 |
#define | MAX_NB_REFINEMENT 100 |
String support via creating string constraints and progressively instantiating the universal constraints as needed.
The procedure is described in the PASS paper at HVC'13: "PASS: String Solving with Parameterized Array and Interval Automaton" by Guodong Li and Indradeep Ghosh
Definition in file string_refinement.h.
#define MAX_CONCRETE_STRING_SIZE 500 |
Definition at line 30 of file string_refinement.h.
Referenced by string_refinementt::string_of_array().
#define MAX_NB_REFINEMENT 100 |
Definition at line 32 of file string_refinement.h.