#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:

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

static optionalt< 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. 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 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. More...

static optionalt< 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. More...

static optionalt< 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. 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< 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. More...

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. 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< exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
	Add association for each char pointer in the equation. More...

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

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

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

static optionalt< 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. 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, array_poolt &array_pool)
	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, 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. 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, 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` More...

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

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

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< exprt > &	equations,
		const namespacet &	ns,
		messaget::mstreamt &	stream
	)

static

Add association for each char pointer in the equation.

Parameters

symbol_solver	a union_find_replacet object to keep track of char pointer equations
equations	vector of equations
ns	namespace
stream	output 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 301 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 427 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 1573 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 1351 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 1331 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 1116 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 399 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 374 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 optionalt< 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 1908 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 optionalt< 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 1002 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 1068 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 1546 of file string_refinement.cpp.

◆ get_valid_array_size()

static optionalt<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 958 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 1606 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 1516 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 1635 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 1658 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 1739 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 1290 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 1506 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 463 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 1050 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 1171 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 1182 of file string_refinement.cpp.

◆ substitute_array_access() [3/5]

static optionalt< exprt > substitute_array_access	(	const index_exprt &	index_expr,
		symbol_generatort &	symbol_generator,
		const bool	left_propagate
	)

static

Definition at line 1203 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 1156 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 1271 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 1232 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 1781 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 1690 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 1531 of file string_refinement.cpp.

◆ validate()

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

static

Definition at line 150 of file string_refinement.cpp.

expr	an expression containing array accesses
symbol_generator	a symbol generator
left_propagate	should values be propagated to the left in with expressions

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