10 #ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H 11 #define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H 44 const std::vector<bool> &unknown,
46 const typet &type)
const override;
69 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H The type of an expression, extends irept.
literalt convert_rest(const exprt &expr) override
bvt convert_bitvector(const exprt &expr) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
std::list< postponedt > postponed_listt
virtual void add_addr(const exprt &expr, bvt &bv)
pointer_logict pointer_logic
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bv_pointerst(const namespacet &_ns, propt &_prop)
postponed_listt postponed_list
void post_process() override
void encode(std::size_t object, bvt &bv)
exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override
Base class for all expressions.
void do_postponed(const postponedt &postponed)
virtual bvt convert_pointer_type(const exprt &expr)
bool convert_address_of_rec(const exprt &expr, bvt &bv)
std::vector< literalt > bvt
void offset_arithmetic(bvt &bv, const mp_integer &x)