string_constraint_instantiation.h File Reference

Defines related function for string constraints. More...

#include <util/std_expr.h>
#include <set>

Include dependency graph for string_constraint_instantiation.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	linear_functiont
	Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given by constant_coefficient 2 and coefficients: x -> 2, y -> -1. More...

Functions
exprt	instantiate (const string_constraintt &axiom, const exprt &str, const exprt &val)
	Instantiates a string constraint by substituting the quantifiers. More...
std::vector< exprt >	instantiate_not_contains (const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt >> &index_pairs, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)

Detailed Description

Defines related function for string constraints.

Definition in file string_constraint_instantiation.h.

Function Documentation

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

Parameters

axiom	a universally quantified formula
str	an array of characters
val	an index expression

Returns

axiom with substitued qvar

Definition at line 175 of file string_constraint_instantiation.cpp.

instantiate_not_contains()

std::vector<exprt> instantiate_not_contains ( const string_not_contains_constraintt &  axiom, const std::set< std::pair< exprt, exprt >> &  index_pairs, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &  witnesses  )

related