cprover
|
String support via creating string constraints and progressively instantiating the universal constraints as needed. More...
#include <solvers/refinement/string_refinement.h>
#include <sstream>
#include <ansi-c/string_constant.h>
#include <util/cprover_prefix.h>
#include <util/replace_expr.h>
#include <solvers/sat/satcheck.h>
#include <langapi/language_util.h>
Go to the source code of this file.
Classes | |
class | find_qvar_visitort |
class | find_index_visitort |
Functions | |
static bool | find_qvar (const exprt index, const symbol_exprt &qvar) |
looks for the symbol and return true if it is found More... | |
exprt | find_index (const exprt &expr, const exprt &str) |
find an index used in the expression for str, for instance with arguments (str[k] == 'a') and str, the function should return k More... | |
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.cpp.
find an index used in the expression for str, for instance with arguments (str[k] == 'a') and str, the function should return k
Definition at line 821 of file string_refinement.cpp.
References exprt::visit().
Referenced by string_refinementt::instantiate().
|
static |
looks for the symbol and return true if it is found
Definition at line 694 of file string_refinement.cpp.
References find_qvar_visitort::found, and exprt::visit().
Referenced by string_refinementt::initial_index_set(), and string_refinementt::instantiate().