cprover
string_refinement.cpp File Reference

String support via creating string constraints and progressively instantiating the universal constraints as needed. More...

Include dependency graph for string_refinement.cpp:

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...
 

Detailed Description

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.

Function Documentation

◆ find_index()

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

parameters: a formula expr and a char array str
Returns
an index expression

Definition at line 821 of file string_refinement.cpp.

References exprt::visit().

Referenced by string_refinementt::instantiate().

◆ find_qvar()

static bool find_qvar ( const exprt  index,
const symbol_exprt qvar 
)
static

looks for the symbol and return true if it is found

parameters: an index expression and a symbol qvar
Returns
a Boolean

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().