cprover
string_constraint_instantiation.cpp File Reference

Defines related function for string constraints. More...

#include "string_constraint_instantiation.h"
#include <algorithm>
#include <unordered_set>
#include <util/expr_iterator.h>
+ Include dependency graph for string_constraint_instantiation.cpp:

Go to the source code of this file.

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_hashfind_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 19 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]exprthe expression to search
[in]strthe string which must be indexed
[in]qvarthe universal variable that must be in the index
Returns
index expressions in expr on str containing qvar.

Definition at line 33 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.

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.