cprover
string_constraint_instantiation.h File Reference

Defines related function for string constraints. More...

+ 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)
 Substitute qvar the universally quantified variable of axiom, by an index val, in axiom, so that the index used for str equals val. More...
 
std::vector< exprtinstantiate_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 
)

Substitute qvar the universally quantified variable of axiom, by an index val, 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'\).

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

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

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 183 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