cprover
Loading...
Searching...
No Matches
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/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:

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.
 
return f to_expr (positive)
 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.
 
exprt instantiate (const string_constraintt &axiom, const exprt &str, const exprt &val)
 Instantiates a string constraint by substituting the quantifiers.
 

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.

◆ 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
axioma universally quantified formula
stran array of characters
valan index expression
Returns
axiom with substitued qvar

Definition at line 173 of file string_constraint_instantiation.cpp.

◆ to_expr()

return f to_expr ( positive )

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. static std::unordered_set<exprt, irep_hash> find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar) { decltype(find_indexes(expr, str, qvar)) result; auto index_str_containing_qvar = [&](const exprt &e) { if(auto index_expr = expr_try_dynamic_cast<index_exprt>(e)) { const auto &arr = index_expr->array(); const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str); return str_it != arr.depth_end() && contains(index_expr->index(), qvar); } return false; };

std::for_each(expr.depth_begin(), expr.depth_end(), [&](const exprt &e) { if(index_str_containing_qvar(e)) result.insert(to_index_expr(e).index()); }); return result; }

linear_functiont::linear_functiont(const exprt &f) { type = f.type(); list of expressions to process with a boolean flag telling whether they appear positively or negatively (true is for positive) std::list<std::pair<exprt, bool>> to_process; to_process.emplace_back(f, true);

while(!to_process.empty()) { const exprt cur = to_process.back().first; bool positive = to_process.back().second; to_process.pop_back(); if(auto integer = numeric_cast<mp_integer>(cur)) { constant_coefficient += positive ? integer.value() : -integer.value(); } else if(cur.id() == ID_plus) { for(const auto &op : cur.operands()) to_process.emplace_back(op, positive); } else if(cur.id() == ID_minus) { to_process.emplace_back(to_minus_expr(cur).op1(), !positive); to_process.emplace_back(to_minus_expr(cur).op0(), positive); } else if(cur.id() == ID_unary_minus) { to_process.emplace_back(to_unary_minus_expr(cur).op(), !positive); } else { if(positive) ++coefficients[cur]; else –coefficients[cur]; } } }

void linear_functiont::add(const linear_functiont &other) { do { if(!(type == other.type)) { invariant_violated_string( FILE, func , LINE, "type == other.type", "Precondition"); } } while(false); constant_coefficient += other.constant_coefficient; for(auto pair : other.coefficients) coefficients[pair.first] += pair.second; }

exprt linear_functiont::to_expr(bool negated) const { exprt sum = nil_exprt{}; const exprt constant_expr = from_integer(constant_coefficient, type); if(constant_coefficient != 0) sum = negated ? (exprt)unary_minus_exprt{constant_expr} : constant_expr;

for(const auto &term : coefficients) { const exprt &t = term.first; const mp_integer factor = negated ? (-term.second) : term.second; if(factor == -1) { if(sum.is_nil()) sum = unary_minus_exprt(t); else sum = minus_exprt(sum, t); } else if(factor == 1) { if(sum.is_nil()) sum = t; else sum = plus_exprt(sum, t); } else if(factor != 0) { const mult_exprt to_add{t, from_integer(factor, t.type())}; if(sum.is_nil()) sum = to_add; else sum = plus_exprt(sum, to_add); } } return sum.is_nil() ? from_integer(0, type) : sum; }

exprt linear_functiont::solve( linear_functiont f, const exprt &var, const exprt &val) { auto it = f.coefficients.find(var); do { if(!(it != f.coefficients.end())) { invariant_violated_string( FILE, func , LINE, "it != f.coefficients.end()", "Precondition"); } } while(false); do { if(!(it->second == 1 || it->second == -1)) { invariant_violated_string( FILE, func , LINE, "it->second == 1 || it->second == -1", "Precondition"); } } while(false); const bool positive = it->second == 1;

Transform f into f(var <- 0) f.coefficients.erase(it); Transform f(var <- 0) into f(var <- 0) - val f.add(linear_functiont{unary_minus_exprt{val}});

If the coefficient of var is 1 then solution `val - f(var <- 0),