cprover
string_refinement.cpp File Reference

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

#include <solvers/refinement/string_refinement.h>
#include <iomanip>
#include <numeric>
#include <stack>
#include <util/expr_iterator.h>
#include <util/expr_util.h>
#include <util/simplify_expr.h>
#include <solvers/sat/satcheck.h>
#include <solvers/refinement/string_constraint_instantiation.h>
#include <unordered_set>
#include <util/magic.h>
+ Include dependency graph for string_refinement.cpp:

Go to the source code of this file.

Classes

class  find_qvar_visitort
 

Functions

static bool is_valid_string_constraint (messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
 
static optionalt< exprtfind_counter_example (const namespacet &ns, const exprt &axiom, const symbol_exprt &var)
 Creates a solver with axiom as the only formula added and runs it. More...
 
static std::pair< bool, std::vector< exprt > > check_axioms (const string_axiomst &axioms, string_constraint_generatort &generator, const std::function< exprt(const exprt &)> &get, messaget::mstreamt &stream, const namespacet &ns, bool use_counter_example, const union_find_replacet &symbol_resolve, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &not_contain_witnesses)
 Check axioms takes the model given by the underlying solver and answers whether it satisfies the string constraints. More...
 
static void initial_index_set (index_set_pairt &index_set, const namespacet &ns, const string_constraintt &axiom)
 
static void initial_index_set (index_set_pairt &index_set, const namespacet &ns, const string_not_contains_constraintt &axiom)
 
static void initial_index_set (index_set_pairt &index_set, const namespacet &ns, const string_axiomst &axioms)
 Add to the index set all the indices that appear in the formulas and the upper bound minus one. More...
 
exprt simplify_sum (const exprt &f)
 
static void update_index_set (index_set_pairt &index_set, const namespacet &ns, const std::vector< exprt > &current_constraints)
 Add to the index set all the indices that appear in the formulas. More...
 
static void update_index_set (index_set_pairt &index_set, const namespacet &ns, const exprt &formula)
 Add to the index set all the indices that appear in the formula. More...
 
static exprt instantiate (const string_constraintt &axiom, const exprt &str, const exprt &val)
 Substitute qvar the universally quantified variable of axiom, by an index val, in axiom, so that the index used for str equals val. More...
 
static std::vector< exprtinstantiate (const string_not_contains_constraintt &axiom, const index_set_pairt &index_set, const string_constraint_generatort &generator, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)
 Instantiates a quantified formula representing not_contains by substituting the quantifiers and generating axioms. More...
 
static optionalt< exprtget_array (const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr)
 Get a model of an array and put it in a certain form. More...
 
static exprt substitute_array_access (const index_exprt &index_expr, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator, const bool left_propagate)
 
template<typename T >
static std::vector< T > fill_in_map_as_vector (const std::map< std::size_t, T > &index_value)
 Convert index-value map to a vector of values. More...
 
static bool validate (const string_refinementt::infot &info)
 
static void display_index_set (messaget::mstreamt &stream, const index_set_pairt &index_set)
 Write index set to the given stream, use for debugging. More...
 
static std::vector< exprtgenerate_instantiations (const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &not_contain_witnesses)
 Instantiation of all constraints. More...
 
static void make_char_array_pointer_associations (string_constraint_generatort &generator, std::vector< equal_exprt > &equations)
 Fill the array_pointer correspondence and replace the right hand sides of the corresponding equations. More...
 
static exprt replace_expr_copy (const union_find_replacet &symbol_resolve, exprt expr)
 Substitute sub-expressions in equation by representative elements of symbol_resolve whenever possible. More...
 
static void add_equations_for_symbol_resolution (union_find_replacet &symbol_solver, const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
 Add association for each char pointer in the equation. More...
 
static std::vector< exprtextract_strings_from_lhs (const exprt &lhs)
 This is meant to be used on the lhs of an equation with string subtype. More...
 
static std::vector< exprtextract_strings (const exprt &expr)
 
static void add_string_equation_to_symbol_resolution (const equal_exprt &eq, union_find_replacet &symbol_resolve, const namespacet &ns)
 Given an equation on strings, mark these strings as belonging to the same set in the symbol_resolve structure. More...
 
union_find_replacet string_identifiers_resolution_from_equations (std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
 Symbol resolution for expressions of type string typet. More...
 
static std::string string_of_array (const array_exprt &arr)
 convert the content of a string to a more readable representation. More...
 
static exprt get_char_array_and_concretize (const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr)
 Debugging function which finds the valuation of the given array in super_get and concretize unknown characters. More...
 
void debug_model (const string_constraint_generatort &generator, messaget::mstreamt &stream, const namespacet &ns, const std::function< exprt(const exprt &)> &super_get, const std::vector< symbol_exprt > &symbols)
 Display part of the current model by mapping the variables created by the solver to constant expressions given by the current model. More...
 
static exprt substitute_array_access (const with_exprt &expr, const exprt &index, const bool left_propagate)
 Create a new expression where 'with' expressions on arrays are replaced by 'if' expressions. More...
 
static exprt substitute_array_access (const array_exprt &array_expr, const exprt &index, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator)
 Create an equivalent expression where array accesses are replaced by 'if' expressions: for instance in array access arr[index], where: arr := {12, 24, 48} the constructed expression will be: index==0 ? 12 : index==1 ? 24 : 48 Avoids repetition so arr := {12, 12, 24, 48} will give index<=1 ? 12 : index==1 ? 24 : 48 More...
 
static exprt substitute_array_access (const if_exprt &if_expr, const exprt &index, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator, const bool left_propagate)
 
static void substitute_array_access_in_place (exprt &expr, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator, const bool left_propagate)
 Auxiliary function for substitute_array_access Performs the same operation but modifies the argument instead of returning the resulting expression. More...
 
exprt substitute_array_access (exprt expr, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator, const bool left_propagate)
 Create an equivalent expression where array accesses and 'with' expressions are replaced by 'if' expressions, in particular: More...
 
static exprt negation_of_not_contains_constraint (const string_not_contains_constraintt &constraint, const symbol_exprt &univ_var, const std::function< exprt(const exprt &)> &get)
 Negates the constraint to be fed to a solver. More...
 
template<typename T >
static void debug_check_axioms_step (messaget::mstreamt &stream, const T &axiom, const T &axiom_in_model, const exprt &negaxiom, const exprt &with_concretized_arrays)
 Debugging function which outputs the different steps an axiom goes through to be checked in check axioms. More...
 
static std::map< exprt, int > map_representation_of_sum (const exprt &f)
 
static exprt sum_over_map (std::map< exprt, int > &m, const typet &type, bool negated=false)
 
static exprt compute_inverse_function (const exprt &qvar, const exprt &val, const exprt &f)
 
static bool find_qvar (const exprt &index, const symbol_exprt &qvar)
 look for the symbol and return true if it is found More...
 
static void get_sub_arrays (const exprt &array_expr, std::vector< exprt > &accu)
 An expression representing an array of characters can be in the form of an if expression for instance cond?array1:(cond2:array2:array3). More...
 
static void add_to_index_set (index_set_pairt &index_set, const namespacet &ns, const exprt &s, exprt i)
 Add i to the index set all the indices that appear in the formula. More...
 
static void initial_index_set (index_set_pairt &index_set, const namespacet &ns, const exprt &qvar, const exprt &upper_bound, const exprt &s, const exprt &i)
 Given an array access of the form s[i] assumed to be part of a formula \( \forall q < u. charconstraint \), initialize the index set of s so that: More...
 
static std::unordered_set< exprt, irep_hashfind_indexes (const exprt &expr, const exprt &str, const symbol_exprt &qvar)
 Find indexes of str used in expr that contains qvar, for instance with arguments (str[k+1]=='a'), str, and k, the function should return k+1. More...
 
exprt substitute_array_lists (exprt expr, size_t string_max_length)
 Replace array-lists by 'with' expressions. 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

◆ add_equations_for_symbol_resolution()

static void add_equations_for_symbol_resolution ( union_find_replacet symbol_solver,
const std::vector< equal_exprt > &  equations,
const namespacet ns,
messaget::mstreamt stream 
)
static

Add association for each char pointer in the equation.

Parameters
symbol_solvera union_find_replacet object to keep track of char pointer equations
equationsvector of equations
nsnamespace
streamoutput stream
Returns
union_find_replacet where char pointer that have been set equal by an equation are associated to the same element

Definition at line 315 of file string_refinement.cpp.

◆ add_string_equation_to_symbol_resolution()

static void add_string_equation_to_symbol_resolution ( const equal_exprt eq,
union_find_replacet symbol_resolve,
const namespacet ns 
)
static

Given an equation on strings, mark these strings as belonging to the same set in the symbol_resolve structure.

The lhs and rhs of the equation, should have string type or be struct with string members.

Parameters
eqequation to add
symbol_resolvestructure to which the equation will be added
nsnamespace

Definition at line 433 of file string_refinement.cpp.

◆ add_to_index_set()

static void add_to_index_set ( index_set_pairt index_set,
const namespacet ns,
const exprt s,
exprt  i 
)
static

Add i to the index set all the indices that appear in the formula.

Parameters
index_setset of indexes
nsnamespace
san expression containing strings
ian expression representing an index

Definition at line 1659 of file string_refinement.cpp.

◆ check_axioms()

static std::pair< bool, std::vector< exprt > > check_axioms ( const string_axiomst axioms,
string_constraint_generatort generator,
const std::function< exprt(const exprt &)> &  get,
messaget::mstreamt stream,
const namespacet ns,
bool  use_counter_example,
const union_find_replacet symbol_resolve,
const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &  not_contain_witnesses 
)
static

Check axioms takes the model given by the underlying solver and answers whether it satisfies the string constraints.

For each string_constraint a:

  • the negation of a is an existential formula b;
  • we substituted symbols in b by their values found in get;
  • arrays are concretized, meaning we attribute a value for characters that are unknown to get, for details see substitute_array_access;
  • b is simplified and array accesses are replaced by expressions without arrays;
  • we give lemma b to a fresh solver;
  • if no counter-example to b is found, this means the constraint a is satisfied by the valuation given by get.
    Returns
    true if the current model satisfies all the axioms, false otherwise with a list of lemmas which are obtained by instantiating constraints at indexes given by counter-examples.
    true if the current model satisfies all the axioms

Definition at line 1246 of file string_refinement.cpp.

◆ compute_inverse_function()

static exprt compute_inverse_function ( const exprt qvar,
const exprt val,
const exprt f 
)
static
Parameters
streaman output stream
qvara symbol representing a universally quantified variable
valan expression
fan expression containing + and - operations in which qvar should appear exactly once.
Returns
an expression corresponding of $f^{-1}(val)$ where $f$ is seen as a function of $qvar$, i.e. the value that is necessary for qvar for f to be equal to val. For instance, if f corresponds to the expression $q + x$, compute_inverse_function(q,v,f) returns an expression for $v - x$.

Definition at line 1532 of file string_refinement.cpp.

◆ debug_check_axioms_step()

template<typename T >
static void debug_check_axioms_step ( messaget::mstreamt stream,
const T &  axiom,
const T &  axiom_in_model,
const exprt negaxiom,
const exprt with_concretized_arrays 
)
static

Debugging function which outputs the different steps an axiom goes through to be checked in check axioms.

Template Parameters
Tcan be either string_constraintt or string_not_contains_constraintt

Definition at line 1227 of file string_refinement.cpp.

◆ debug_model()

void debug_model ( const string_constraint_generatort generator,
messaget::mstreamt stream,
const namespacet ns,
const std::function< exprt(const exprt &)> &  super_get,
const std::vector< symbol_exprt > &  symbols 
)

Display part of the current model by mapping the variables created by the solver to constant expressions given by the current model.

Definition at line 1024 of file string_refinement.cpp.

◆ display_index_set()

static void display_index_set ( messaget::mstreamt stream,
const index_set_pairt index_set 
)
static

Write index set to the given stream, use for debugging.

Definition at line 181 of file string_refinement.cpp.

◆ extract_strings()

static std::vector<exprt> extract_strings ( const exprt expr)
static
Parameters
expran expression
Returns
all subexpressions of type string which are not if_exprt expressions this includes expressions of the form e.x if e is a symbol subexpression with a field x of type string

Definition at line 405 of file string_refinement.cpp.

◆ extract_strings_from_lhs()

static std::vector<exprt> extract_strings_from_lhs ( const exprt lhs)
static

This is meant to be used on the lhs of an equation with string subtype.

Parameters
lhsexpression which is either of string type, or a symbol representing a struct with some string members
Returns
if lhs is a string return this string, if it is a struct return the members of the expression that have string type.

Definition at line 382 of file string_refinement.cpp.

◆ fill_in_map_as_vector()

template<typename T >
static std::vector<T> fill_in_map_as_vector ( const std::map< std::size_t, T > &  index_value)
static

Convert index-value map to a vector of values.

If a value for an index is not defined, set it to the value referenced by the next higher index. The length of the resulting vector is the key of the map's last element + 1

Parameters
index_valuemap containing values of specific vector cells
Returns
Vector containing values as described in the map

Definition at line 139 of file string_refinement.cpp.

◆ find_counter_example()

static optionalt< exprt > find_counter_example ( const namespacet ns,
const exprt axiom,
const symbol_exprt var 
)
static

Creates a solver with axiom as the only formula added and runs it.

If it is SAT, then true is returned and the given evaluation of var is stored in witness. If UNSAT, then what witness is is undefined.

Parameters
nsnamespace
[in]axiomthe axiom to be checked
[in]varthe variable whose evaluation will be stored in witness
Returns
: the witness of the satisfying assignment if one exists. If UNSAT, then behaviour is undefined.

Definition at line 2049 of file string_refinement.cpp.

◆ find_indexes()

static std::unordered_set<exprt, irep_hash> find_indexes ( const exprt expr,
const exprt str,
const symbol_exprt qvar 
)
static

Find indexes of str used in expr that contains qvar, for instance with arguments (str[k+1]=='a'), str, and k, the function should return k+1.

Parameters
[in]exprthe expression to search
[in]strthe string which must be indexed
[in]qvarthe universal variable that must be in the index
Returns
index expressions in expr on str containing qvar.

Definition at line 1813 of file string_refinement.cpp.

◆ find_qvar()

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

look for the symbol and return true if it is found

Parameters
indexan index expression
qvara symbol expression
Returns
a Boolean

Definition at line 1590 of file string_refinement.cpp.

◆ generate_instantiations()

static std::vector<exprt> generate_instantiations ( const string_constraint_generatort generator,
const index_set_pairt index_set,
const string_axiomst axioms,
const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &  not_contain_witnesses 
)
static

Instantiation of all constraints.

The string refinement decision procedure works with two types of quantified axioms, which are of the form \(\forall x.\ P(x)\) (string_constraintt) or of the form \(\forall x. P(x) \Rightarrow \exists y .s_0[x+y] \ne s_1[y] \) (string_not_contains_constraintt). They are instantiated in a way which depends on their form:

  • For formulas of the form \(\forall x.\ P(x)\) if string str appears in P indexed by some f(x) and val is in the index set of str we find y such that f(y)=val and add lemma P(y). (See instantiate(messaget::mstreamt&,const string_constraintt&,const exprt &,const exprt&) for details)

For formulas of the form \(\forall x. P(x) \Rightarrow \exists y .s_0[x+y] \ne s_1[y]) \) we need to look at the index set of both s_0 and s_1. (See instantiate(const string_not_contains_constraintt&,const index_set_pairt&,const string_constraint_generatort&,const std::map<string_not_contains_constraintt, symbol_exprt>&) for details)

Definition at line 231 of file string_refinement.cpp.

◆ get_array()

static optionalt< exprt > get_array ( const std::function< exprt(const exprt &)> &  super_get,
const namespacet ns,
messaget::mstreamt stream,
const array_string_exprt arr 
)
static

Get a model of an array and put it in a certain form.

If the model is incomplete or if it is too big, return no value.

Parameters
super_getfunction returning the valuation of an expression in a model
nsnamespace
streamoutput stream for warning messages
arrexpression of type array representing a string
Returns
an optional array expression or array_of_exprt

Definition at line 903 of file string_refinement.cpp.

◆ get_char_array_and_concretize()

static exprt get_char_array_and_concretize ( const std::function< exprt(const exprt &)> &  super_get,
const namespacet ns,
messaget::mstreamt stream,
const array_string_exprt arr 
)
static

Debugging function which finds the valuation of the given array in super_get and concretize unknown characters.

Parameters
super_getgive a valuation to variables
nsnamespace
streamoutput stream
arrarray expression
Returns
expression corresponding to arr in the model

Definition at line 977 of file string_refinement.cpp.

◆ get_sub_arrays()

static void get_sub_arrays ( const exprt array_expr,
std::vector< exprt > &  accu 
)
static

An expression representing an array of characters can be in the form of an if expression for instance cond?array1:(cond2:array2:array3).

We return all the array expressions contained in array_expr.

Parameters
array_expr: an expression representing an array
accua vector to which symbols and constant arrays contained in the expression will be appended

Definition at line 1632 of file string_refinement.cpp.

◆ initial_index_set() [1/4]

static void initial_index_set ( index_set_pairt index_set,
const namespacet ns,
const string_constraintt axiom 
)
static

Definition at line 1719 of file string_refinement.cpp.

◆ initial_index_set() [2/4]

static void initial_index_set ( index_set_pairt index_set,
const namespacet ns,
const string_not_contains_constraintt axiom 
)
static

Definition at line 1742 of file string_refinement.cpp.

◆ initial_index_set() [3/4]

static void initial_index_set ( index_set_pairt index_set,
const namespacet ns,
const string_axiomst axioms 
)
static

Add to the index set all the indices that appear in the formulas and the upper bound minus one.

Parameters
index_setset of indexes to update
nsnamespace
axiomsa list of string axioms

Definition at line 1602 of file string_refinement.cpp.

◆ initial_index_set() [4/4]

static void initial_index_set ( index_set_pairt index_set,
const namespacet ns,
const exprt qvar,
const exprt upper_bound,
const exprt s,
const exprt i 
)
static

Given an array access of the form s[i] assumed to be part of a formula \( \forall q < u. charconstraint \), initialize the index set of s so that:

  • \( i[q -> u - 1] \) appears in the index set of s if s is a symbol
  • if s is an array expression, all index from 0 to \( s.length - 1 \) are in the index set
  • if s is an if expression we apply this procedure to the true and false cases
    Parameters
    index_setthe index_set to initialize
    nsnamespace, used for simplifying indexes
    qvarthe quantified variable q
    upper_boundbound u on the quantified variable
    sexpression representing a string
    iexpression representing the index at which s is accessed

Definition at line 1692 of file string_refinement.cpp.

◆ instantiate() [1/2]

static exprt instantiate ( const string_constraintt axiom,
const exprt str,
const exprt val 
)
static

Substitute qvar the universally quantified variable of axiom, by an index val, in axiom, so that the index used for str equals val.

Instantiates a string constraint by substituting the quantifiers.

For instance, if axiom corresponds to \(\forall q.\ s[q+x]='a' \land t[q]='b'\), instantiate(axiom,s,v) would return an expression for \(s[v]='a' \land t[v-x]='b'\).

Parameters
streamoutput stream
axioma universally quantified formula
stran array of char variable
valan index expression
Returns
axiom with substitued qvar

For a string constraint of the form forall q. P(x), substitute q the universally quantified variable of axiom, by an index, in axiom, so that the index used for str equals val. For instance, if axiom is ‘forall q. s[q+x] = 'a’ && t[q] = 'b', instantiate(axiom,s,v)would return the expression s[v] = 'a' && t[v-x] = 'b'`. If there are several such indexes, the conjunction of the instantiations is returned, for instance for a formula: ‘forall q. s[q+x]='a’ && s[q]=cwe would get s[v] = 'a' && s[v-x] = c && s[v+x] = 'a' && s[v] = c`.

Parameters
axioma universally quantified formula
stran array of characters
valan index expression
Returns
instantiated formula

Definition at line 1848 of file string_refinement.cpp.

◆ instantiate() [2/2]

static std::vector< exprt > instantiate ( const string_not_contains_constraintt axiom,
const index_set_pairt index_set,
const string_constraint_generatort generator,
const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &  witnesses 
)
static

Instantiates a quantified formula representing not_contains by substituting the quantifiers and generating axioms.

For a formula of the form \(\phi = \forall x. P(x) \Rightarrow Q(x, f(x))\) let \(instantiate\_not\_contains(\phi) = ( (f(t) = u) \land P(t) ) \Rightarrow Q(t, u)\). Then \(\forall x.\ P(x) \Rightarrow Q(x, f(x)) \models \) Axioms of the form \(\forall x. P(x) \Rightarrow \exists y .Q(x, y) \) can be transformed into the the equisatisfiable formula \(\forall x. P(x) \Rightarrow Q(x, f(x))\) for a new function symbol f. Hence, after transforming axioms of the second type and by the above lemmas, we can create quantifier free formulas that are entailed by a (transformed) axiom.

Parameters
[in]axiomthe axiom to instantiate
index_setset of indexes
generatorconstraint generator object
Returns
the lemmas produced through instantiation

Definition at line 1887 of file string_refinement.cpp.

◆ is_valid_string_constraint()

static bool is_valid_string_constraint ( messaget::mstreamt stream,
const namespacet ns,
const string_constraintt constraint 
)
related

◆ make_char_array_pointer_associations()

static void make_char_array_pointer_associations ( string_constraint_generatort generator,
std::vector< equal_exprt > &  equations 
)
static

Fill the array_pointer correspondence and replace the right hand sides of the corresponding equations.

Definition at line 258 of file string_refinement.cpp.

◆ map_representation_of_sum()

static std::map<exprt, int> map_representation_of_sum ( const exprt f)
static
Parameters
fan expression with only addition and subtraction
Returns
a map where each leaf of the input is mapped to the number of times it is added. For instance, expression $x + x - y$ would give the map x -> 2, y -> -1.

Definition at line 1399 of file string_refinement.cpp.

◆ negation_of_not_contains_constraint()

static exprt negation_of_not_contains_constraint ( const string_not_contains_constraintt constraint,
const symbol_exprt univ_var,
const std::function< exprt(const exprt &)> &  get 
)
static

Negates the constraint to be fed to a solver.

The intended usage is to find an assignment of the universal variable that would violate the axiom. To avoid false positives, the symbols other than the universal variable should have been replaced by their valuation in the current model.

Precondition
Symbols other than the universal variable should have been replaced by their valuation in the current model.
Parameters
constraintthe not_contains constraint to add the negation of
univ_varthe universal variable for the negation of the axiom
getvaluation function, the result should have been simplified
Returns
: the negation of the axiom under the current evaluation

Definition at line 1192 of file string_refinement.cpp.

◆ replace_expr_copy()

static exprt replace_expr_copy ( const union_find_replacet symbol_resolve,
exprt  expr 
)
static

Substitute sub-expressions in equation by representative elements of symbol_resolve whenever possible.

Similar to symbol_resolve.replace_expr but doesn't mutate the expression and returns the transformed expression instead.

Definition at line 279 of file string_refinement.cpp.

◆ simplify_sum()

exprt simplify_sum ( const exprt f)
Parameters
fan expression with only plus and minus expr
Returns
an equivalent expression in a canonical form

Definition at line 1516 of file string_refinement.cpp.

◆ string_identifiers_resolution_from_equations()

union_find_replacet string_identifiers_resolution_from_equations ( std::vector< equal_exprt > &  equations,
const namespacet ns,
messaget::mstreamt stream 
)

Symbol resolution for expressions of type string typet.

We record equality between these expressions in the output if one of the function calls depends on them.

Parameters
equationslist of equations
nsnamespace
streamoutput stream
Returns
union_find_replacet structure containing the correspondences.

Definition at line 466 of file string_refinement.cpp.

◆ string_of_array()

static std::string string_of_array ( const array_exprt arr)
static

convert the content of a string to a more readable representation.

This should only be used for debugging.

Parameters
arra constant array expression
Returns
a string

Definition at line 960 of file string_refinement.cpp.

◆ substitute_array_access() [1/5]

static exprt substitute_array_access ( const index_exprt index_expr,
const std::function< symbol_exprt(const irep_idt &, const typet &)> &  symbol_generator,
const bool  left_propagate 
)
static

Definition at line 1106 of file string_refinement.cpp.

◆ substitute_array_access() [2/5]

static exprt substitute_array_access ( const with_exprt expr,
const exprt index,
const bool  left_propagate 
)
static

Create a new expression where 'with' expressions on arrays are replaced by 'if' expressions.

e.g. for an array access arr[index], where: arr := array_of(12) with {0:=24} with {2:=42} the constructed expression will be: index==0 ? 24 : index==2 ? 42 : 12 If left_propagate is set to true, the expression will look like index<=0 ? 24 : index<=2 ? 42 : 12

Parameters
exprA (possibly nested) 'with' expression on an array_of expression. The function checks that the expression is of the form with_expr(with_expr(...(array_of(...))). This is the form in which array valuations coming from the underlying solver are given.
indexAn index with which to build the equality condition
Returns
An expression containing no 'with' expression

Definition at line 1063 of file string_refinement.cpp.

◆ substitute_array_access() [3/5]

static exprt substitute_array_access ( const array_exprt array_expr,
const exprt index,
const std::function< symbol_exprt(const irep_idt &, const typet &)> &  symbol_generator 
)
static

Create an equivalent expression where array accesses are replaced by 'if' expressions: for instance in array access arr[index], where: arr := {12, 24, 48} the constructed expression will be: index==0 ? 12 : index==1 ? 24 : 48 Avoids repetition so arr := {12, 12, 24, 48} will give index<=1 ? 12 : index==1 ? 24 : 48

Definition at line 1078 of file string_refinement.cpp.

◆ substitute_array_access() [4/5]

static exprt substitute_array_access ( const if_exprt if_expr,
const exprt index,
const std::function< symbol_exprt(const irep_idt &, const typet &)> &  symbol_generator,
const bool  left_propagate 
)
static

Definition at line 1090 of file string_refinement.cpp.

◆ substitute_array_access() [5/5]

exprt substitute_array_access ( exprt  expr,
const std::function< symbol_exprt(const irep_idt &, const typet &)> &  symbol_generator,
const bool  left_propagate 
)

Create an equivalent expression where array accesses and 'with' expressions are replaced by 'if' expressions, in particular:

  • for an array access arr[index], where: arr := {12, 24, 48} the constructed expression will be: index==0 ? 12 : index==1 ? 24 : 48
  • for an array access arr[index], where: arr := array_of(12) with {0:=24} with {2:=42} the constructed expression will be: index==0 ? 24 : index==2 ? 42 : 12
  • for an array access (g1?arr1:arr2)[x] where arr1 := {12} and arr2 := {34}, the constructed expression will be: g1 ? 12 : 34
  • for an access in an empty array { }[x] returns a fresh symbol, this corresponds to a non-deterministic result Note that if left_propagate is set to true, the with case will result in something like: index <= 0 ? 24 : index <= 2 ? 42 : 12
    Parameters
    expran expression containing array accesses
    symbol_generatorfunction which given a prefix and a type generates a fresh symbol of the given type
    left_propagateshould values be propagated to the left in with expressions
    Returns
    an expression containing no array access

Definition at line 1172 of file string_refinement.cpp.

◆ substitute_array_access_in_place()

static void substitute_array_access_in_place ( exprt expr,
const std::function< symbol_exprt(const irep_idt &, const typet &)> &  symbol_generator,
const bool  left_propagate 
)
static

Auxiliary function for substitute_array_access Performs the same operation but modifies the argument instead of returning the resulting expression.

Definition at line 1136 of file string_refinement.cpp.

◆ substitute_array_lists()

exprt substitute_array_lists ( exprt  expr,
size_t  string_max_length 
)

Replace array-lists by 'with' expressions.

For instance array-list [ 0 , x , 1 , y ] is replaced by ARRAYOF(0) WITH [0:=x] WITH [1:=y]. Indexes exceeding the maximal string length are ignored.

Parameters
expran expression containing array-list expressions
string_max_lengthmaximum length allowed for strings
Returns
an expression containing no array-list

Definition at line 1929 of file string_refinement.cpp.

◆ sum_over_map()

static exprt sum_over_map ( std::map< exprt, int > &  m,
const typet type,
bool  negated = false 
)
static
Parameters
ma map from expressions to integers
typetype for the returned expression
negatedoptinal Boolean asking to negates the sum
Returns
a expression for the sum of each element in the map a number of times given by the corresponding integer in the map. For a map x -> 2, y -> -1 would give an expression $x + x - y$.

Definition at line 1443 of file string_refinement.cpp.

◆ update_index_set() [1/2]

static void update_index_set ( index_set_pairt index_set,
const namespacet ns,
const std::vector< exprt > &  current_constraints 
)
static

Add to the index set all the indices that appear in the formulas.

Parameters
index_setset of indexes to update
nsnamespace
current_constraintsa vector of string constraints

Definition at line 1617 of file string_refinement.cpp.

◆ update_index_set() [2/2]

static void update_index_set ( index_set_pairt index_set,
const namespacet ns,
const exprt formula 
)
static

Add to the index set all the indices that appear in the formula.

Parameters
index_setset of indexes
nsnamespace
formulaa string constraint

Definition at line 1774 of file string_refinement.cpp.

◆ validate()

static bool validate ( const string_refinementt::infot info)
static

Definition at line 162 of file string_refinement.cpp.