13 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_VALUE_H
15 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_VALUE_H
19 #include <unordered_set>
24 using valuest = std::unordered_set<exprt, irep_hash>;
49 const std::vector<abstract_object_pointert> &operands,
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Base class for all expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The type of an expression, extends irept.
static constexpr CLONE std::size_t max_value_set_size
TODO arbitrary limit, make configurable.
const valuest & get_values() const
Get the possible values for this abstract object.
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
valuest values
If BOTTOM then empty.
std::unordered_set< exprt, irep_hash > valuest
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
Print the value of the abstract object.
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
value_set_abstract_valuet(const typet &type, bool top=true, bool bottom=false)