cprover
|
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"
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. | |
Defines related function for string constraints.
Definition in file string_constraint_instantiation.cpp.
|
static |
Look for symbol qvar
in the expression index
and return true if found.
qvar
appears in index
. Definition at line 24 of file string_constraint_instantiation.cpp.
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\).
axiom | a universally quantified formula |
str | an array of characters |
val | an index expression |
axiom
with substitued qvar
Definition at line 173 of file string_constraint_instantiation.cpp.
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
.
/
[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 / |
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),