#include "string_constraint_instantiation.h"
#include <algorithm>
#include <unordered_set>
#include <util/arith_tools.h>
#include <util/expr_iterator.h>
#include <util/format_expr.h>
#include "string_constraint.h"

Include dependency graph for string_constraint_instantiation.cpp:

Functions
static bool	contains (const exprt &index, const symbol_exprt &qvar)
	Look for symbol `qvar` in the expression `index` and return true if found. More...

static std::unordered_set< exprt, irep_hash >	find_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	instantiate (const string_constraintt &axiom, const exprt &str, const exprt &val)
	Instantiates a string constraint by substituting the quantifiers. More...

Detailed Description

Defines related function for string constraints.

Definition in file string_constraint_instantiation.cpp.

Function Documentation

◆ contains()

static bool contains	(	const exprt &	index,
		const symbol_exprt &	qvar
	)

static

Look for symbol qvar in the expression index and return true if found.

Returns: True, iff qvar appears in index.

Definition at line 24 of file string_constraint_instantiation.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]	expr	the expression to search
[in]	str	the string which must be indexed
[in]	qvar	the universal variable that must be in the index

Returns: index expressions in expr on str containing qvar.

Definition at line 38 of file string_constraint_instantiation.cpp.

◆ instantiate()

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

Instantiates a string constraint by substituting the quantifiers.

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 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'\). If there are several such indexes, the conjunction of the instantiations is returned, for instance for a formula: \(\forall q. s[q+x]='a' \land s[q]=c\) we would get \(s[v] = 'a' \land s[v-x] = c \land s[v+x] = 'a' \land s[v] = c\).