Loading...

Searching...

No Matches

string_refinement.cpp File Reference

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

#include "string_refinement.h"
#include <solvers/sat/satcheck.h>
#include <stack>
#include <unordered_set>
#include <util/expr_iterator.h>
#include <util/expr_util.h>
#include <util/format_type.h>
#include <util/magic.h>
#include <util/range.h>
#include <util/simplify_expr.h>
#include "equation_symbol_mapping.h"
#include "string_constraint_instantiation.h"
#include "string_dependencies.h"
#include "string_refinement_invariant.h"

+ Include dependency graph for string_refinement.cpp:

[フレーム]

Go to the source code of this file.

Functions

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

static std::optional< exprt > find_counter_example (const namespacet &ns, const exprt &axiom, const symbol_exprt &var, message_handlert &message_handler)

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

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.

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.

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.

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.

static std::vector< exprt > instantiate (const string_not_contains_constraintt &axiom, const index_set_pairt &index_set, 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.

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

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

static std::optional< exprt > substitute_array_access (const index_exprt &index_expr, symbol_generatort &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.

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.

static std::vector< exprt > generate_instantiations (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.

static void make_char_array_pointer_associations (string_constraint_generatort &generator, exprt &expr)

If expr is an equation whose right-hand-side is a associate_array_to_pointer call, add the correspondence and replace the call by an expression representing its result.

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.

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

Add association for each char pointer in the equation.

static std::vector< exprt > extract_strings_from_lhs (const exprt &lhs, const namespacet &ns)

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

static std::vector< exprt > extract_strings (const exprt &expr, const namespacet &ns)

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.

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

Symbol resolution for expressions of type string typet.

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

Get a model of the size of the input string.

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

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

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, array_poolt &array_pool)

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

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, array_poolt &array_pool)

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

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.

static exprt substitute_array_access (const array_exprt &array_expr, const exprt &index, symbol_generatort &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

static exprt substitute_array_access (const if_exprt &if_expr, const exprt &index, symbol_generatort &symbol_generator, const bool left_propagate)

static void substitute_array_access_in_place (exprt &expr, symbol_generatort &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.

exprt substitute_array_access (exprt expr, symbol_generatort &symbol_generator, const bool left_propagate)

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

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.

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.

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

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.

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:

exprt substitute_array_lists (exprt expr, size_t string_max_length)

Replace array-lists by 'with' expressions.

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< exprt > & equations,

const namespacet & ns,

messaget::mstreamt & stream

)

static

Add association for each char pointer in the equation.

Parameters: [in,out] symbol_solver a union_find_replacet object to keep track of char pointer equations. Char pointers that have been set equal by an equation are associated to the same element.

equations vector of equations

ns namespace

stream output stream

Definition at line 300 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: eq equation to add

symbol_resolve structure to which the equation will be added

ns namespace

Definition at line 432 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_set set of indexes

ns namespace

s an expression containing strings

i an expression representing an index

Definition at line 1584 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 1362 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: T can be either string_constraintt or string_not_contains_constraintt

Definition at line 1342 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,

array_poolt & array_pool

)

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 1127 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 172 of file string_refinement.cpp.

◆ extract_strings()

static std::vector< exprt > extract_strings ( const exprt & expr,

const namespacet & ns

)

static

Parameters: expr an expression

ns namespace to resolve type tags

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 404 of file string_refinement.cpp.

◆ extract_strings_from_lhs()

static std::vector< exprt > extract_strings_from_lhs ( const exprt & lhs,

const namespacet & ns

)

static

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

Parameters: lhs expression which is either of string type, or a symbol representing a struct with some string members

ns namespace to resolve type tags

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 376 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_value map containing values of specific vector cells

Returns: Vector containing values as described in the map

Definition at line 130 of file string_refinement.cpp.

◆ find_counter_example()

static std::optional< exprt > find_counter_example ( const namespacet & ns,

const exprt & axiom,

const symbol_exprt & var,

message_handlert & message_handler

)

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: ns namespace

[in] axiom the axiom to be checked

[in] var the variable whose evaluation will be stored in witness

message_handler message handler

Returns: the witness of the satisfying assignment if one exists. If UNSAT, then behaviour is undefined.

Definition at line 1919 of file string_refinement.cpp.

◆ generate_instantiations()

static std::vector< exprt > generate_instantiations ( 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 std::map<string_not_contains_constraintt, symbol_exprt>&) for details.)

Definition at line 220 of file string_refinement.cpp.

◆ get_array()

static std::optional< exprt > get_array ( const std::function< exprt(const exprt &)> & super_get,

const namespacet & ns,

messaget::mstreamt & stream,

const array_string_exprt & arr,

const array_poolt & array_pool

)

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_get function returning the valuation of an expression in a model

ns namespace

stream output stream for warning messages

arr expression of type array representing a string

array_pool pool of arrays representing strings

Returns: an optional array expression or array_of_exprt

Definition at line 1012 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,

array_poolt & array_pool

)

static

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

Parameters: super_get give a valuation to variables

ns namespace

stream output stream

arr array expression

array_pool pool of arrays representing strings

Returns: expression corresponding to arr in the model

Definition at line 1078 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

accu a vector to which symbols and constant arrays contained in the expression will be appended

Definition at line 1557 of file string_refinement.cpp.

◆ get_valid_array_size()

static std::optional< exprt > get_valid_array_size ( const std::function< exprt(const exprt &)> & super_get,

const namespacet & ns,

messaget::mstreamt & stream,

const array_string_exprt & arr,

const array_poolt & array_pool

)

static

Get a model of the size of the input string.

First ask the solver for a size value. If the solver has no value, get the size directly from the type. This is the case for string literals that are not part of the decision procedure (e.g. literals in return values). If the size value is not a constant or not a valid integer (size_t), return no value.

Parameters: super_get function returning the valuation of an expression in a model

ns namespace

stream output stream for warning messages

arr expression of type array representing a string

array_pool pool of arrays representing strings

Returns: an optional expression representing the size of the array that can be cast to size_t

Definition at line 968 of file string_refinement.cpp.

◆ initial_index_set() [1/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_set the index_set to initialize

ns namespace, used for simplifying indexes

qvar the quantified variable q

upper_bound bound u on the quantified variable

s expression representing a string

i expression representing the index at which s is accessed

Definition at line 1617 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_axiomst & axioms

)

static

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

Parameters: index_set set of indexes to update

ns namespace

axioms a list of string axioms

Definition at line 1527 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_constraintt & axiom

)

static

Definition at line 1646 of file string_refinement.cpp.

◆ initial_index_set() [4/4]

static void initial_index_set ( index_set_pairt & index_set,

const namespacet & ns,

const string_not_contains_constraintt & axiom

)

static

Definition at line 1669 of file string_refinement.cpp.

◆ instantiate()

static std::vector< exprt > instantiate ( const string_not_contains_constraintt & axiom,

const index_set_pairt & index_set,

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] axiom the axiom to instantiate

index_set set of indexes

witnesses axiom's witnesses for non-containment

Returns: the lemmas produced through instantiation

Definition at line 1750 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

)

static void make_char_array_pointer_associations ( string_constraint_generatort & generator,

exprt & expr

)

static

If expr is an equation whose right-hand-side is a associate_array_to_pointer call, add the correspondence and replace the call by an expression representing its result.

Definition at line 247 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: constraint the not_contains constraint to add the negation of

univ_var the universal variable for the negation of the axiom

get valuation function, the result should have been simplified

Returns: the negation of the axiom under the current evaluation

Definition at line 1301 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 273 of file string_refinement.cpp.

◆ simplify_sum()

exprt simplify_sum ( const exprt & f )

Parameters: f an expression with only plus and minus expr

Returns: an equivalent expression in a canonical form

Definition at line 1517 of file string_refinement.cpp.

◆ string_identifiers_resolution_from_equations()

union_find_replacet string_identifiers_resolution_from_equations ( const 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: equations list of equations

ns namespace

stream output stream

Returns: union_find_replacet structure containing the correspondences.

Definition at line 470 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: arr a constant array expression

Returns: a string

Definition at line 1060 of file string_refinement.cpp.

◆ substitute_array_access() [1/5]

static exprt substitute_array_access ( const array_exprt & array_expr,

const exprt & index,

symbol_generatort & 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 1182 of file string_refinement.cpp.

◆ substitute_array_access() [2/5]

static exprt substitute_array_access ( const if_exprt & if_expr,

const exprt & index,

symbol_generatort & symbol_generator,

const bool left_propagate

)

static

Definition at line 1193 of file string_refinement.cpp.

◆ substitute_array_access() [3/5]

static std::optional< exprt > substitute_array_access ( const index_exprt & index_expr,

symbol_generatort & symbol_generator,

const bool left_propagate

)

static

Definition at line 1214 of file string_refinement.cpp.

◆ substitute_array_access() [4/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

Parameters: expr A (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.

index An index with which to build the equality condition

left_propagate If set to true, the expression will look like index<=0 ? 24 : index<=2 ? 42 : 12

Returns: An expression containing no 'with' expression

Definition at line 1167 of file string_refinement.cpp.

◆ substitute_array_access() [5/5]

exprt substitute_array_access ( exprt expr,

symbol_generatort & 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

expr an expression containing array accesses

symbol_generator a symbol generator

left_propagate should values be propagated to the left in with expressions

Returns
an expression containing no array access

Definition at line 1282 of file string_refinement.cpp.

◆ substitute_array_access_in_place()

static void substitute_array_access_in_place ( exprt & expr,

symbol_generatort & 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 1243 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: expr an expression containing array-list expressions

string_max_length maximum length allowed for strings

Returns: an expression containing no array-list

Definition at line 1792 of file string_refinement.cpp.

◆ update_index_set() [1/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_set set of indexes

ns namespace

formula a string constraint

Definition at line 1701 of file string_refinement.cpp.

◆ update_index_set() [2/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_set set of indexes to update

ns namespace

current_constraints a vector of string constraints

Definition at line 1542 of file string_refinement.cpp.

◆ validate()

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

static

Definition at line 150 of file string_refinement.cpp.

Functions

Detailed Description

Function Documentation

◆ add_equations_for_symbol_resolution()

◆ add_string_equation_to_symbol_resolution()

◆ add_to_index_set()

◆ check_axioms()

◆ debug_check_axioms_step()

◆ debug_model()

◆ display_index_set()

◆ extract_strings()

◆ extract_strings_from_lhs()

◆ fill_in_map_as_vector()

◆ find_counter_example()

◆ generate_instantiations()

◆ get_array()

◆ get_char_array_and_concretize()

◆ get_sub_arrays()

◆ get_valid_array_size()

◆ initial_index_set() [1/4]

◆ initial_index_set() [2/4]

◆ initial_index_set() [3/4]

◆ initial_index_set() [4/4]

◆ instantiate()

◆ is_valid_string_constraint()

◆ make_char_array_pointer_associations()

◆ negation_of_not_contains_constraint()

◆ replace_expr_copy()

◆ simplify_sum()

◆ string_identifiers_resolution_from_equations()

◆ string_of_array()

◆ substitute_array_access() [1/5]

◆ substitute_array_access() [2/5]

◆ substitute_array_access() [3/5]

◆ substitute_array_access() [4/5]

◆ substitute_array_access() [5/5]

◆ substitute_array_access_in_place()

◆ substitute_array_lists()

◆ update_index_set() [1/2]

◆ update_index_set() [2/2]

◆ validate()