Go to the documentation of this file.
14 #include <unordered_set>
32 static std::unordered_set<exprt, irep_hash>
36 auto index_str_containing_qvar = [&](
const exprt &e) {
37 if(
auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
39 const auto &arr = index_expr->array();
40 const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
41 return str_it != arr.depth_end() &&
contains(index_expr->index(), qvar);
47 if(index_str_containing_qvar(e))
48 result.insert(to_index_expr(e).index());
58 std::list<std::pair<exprt, bool>> to_process;
59 to_process.emplace_back(f,
true);
61 while(!to_process.empty())
63 const exprt cur = to_process.back().first;
64 bool positive = to_process.back().second;
65 to_process.pop_back();
66 if(
auto integer = numeric_cast<mp_integer>(cur))
70 else if(cur.
id() == ID_plus)
73 to_process.emplace_back(op, positive);
75 else if(cur.
id() == ID_minus)
80 else if(cur.
id() == ID_unary_minus)
111 const exprt &t = term.first;
112 const mp_integer factor = negated ? (-term.second) : term.second;
147 const bool positive = it->second == 1;
161 std::ostringstream stream;
164 stream <<
" + " << pair.second <<
" * " <<
::format(pair.first);
191 const exprt univ_var_value =
199 conjuncts.push_back(instance);
213 const std::set<std::pair<exprt, exprt>> &index_pairs,
214 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
217 std::vector<exprt> lemmas;
222 for(
const auto &pair : index_pairs)
226 const exprt &i0 = pair.first;
227 const exprt &i1 = pair.second;
240 const and_exprt body(differ, existential_bound);
243 lemmas.push_back(lemma);
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
mp_integer constant_coefficient
depth_iteratort depth_begin()
std::string format()
Format the linear function as a string, can be used for debugging.
void add(const linear_functiont &other)
Make this function the sum of the current function with other.
std::unordered_map< exprt, mp_integer, irep_hash > coefficients
linear_functiont(const exprt &f)
Put an expression f composed of additions and subtractions into its cannonical representation.
The plus expression Associativity is not specified.
Base class for all expressions.
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given...
Expression to hold a symbol (variable)
exprt instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val)
Instantiates a string constraint by substituting the quantifiers.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
typet & type()
Return the type of the expression.
static std::unordered_set< exprt, irep_hash > find_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'),...
exprt to_expr(bool negated=false) const
static exprt solve(linear_functiont f, const exprt &var, const exprt &val)
Return an expression y such that f(var <- y) = val.
#define PRECONDITION(CONDITION)
Binary multiplication Associativity is not specified.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
The unary minus expression.
const irep_idt & id() const
std::vector< exprt > operandst
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
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)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
Defines related function for string constraints.
A base class for relations, i.e., binary predicates whose two operands have the same type.
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
Constraints to encode non containement of strings.
depth_iteratort depth_end()