cprover
|
Generates string constraints to link results from string functions with their arguments. More...
#include <util/string_expr.h>
#include <solvers/refinement/refined_string_type.h>
#include <solvers/refinement/string_constraint.h>
Go to the source code of this file.
Classes | |
class | string_constraint_generatort |
Generates string constraints to link results from string functions with their arguments.
This is inspired by the PASS paper at HVC'13: "PASS: String Solving with Parameterized Array and Interval Automaton" by Guodong Li and Indradeep Ghosh, which gives examples of constraints for several functions.
Definition in file string_constraint_generator.h.