cprover
|
Defines related function for string constraints. More...
#include "string_constraint_instantiation.h"
#include <util/arith_tools.h>
#include <util/expr_iterator.h>
#include <util/format_expr.h>
#include "string_constraint.h"
#include <algorithm>
#include <list>
#include <unordered_set>
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 26 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 |
Definition at line 175 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 / |
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),