10 #ifndef CPROVER_SOLVERS_SMT2_SMT2_CONV_H 11 #define CPROVER_SOLVERS_SMT2_SMT2_CONV_H 49 const std::string &_benchmark,
50 const std::string &_notes,
51 const std::string &_logic,
118 virtual void set_to(
const exprt &expr,
bool value);
224 std::vector<exprt> &let_order,
231 std::vector<exprt> &let_order);
255 {
set(ID_identifier, _identifier); }
259 return get(ID_identifier);
266 return static_cast<const smt2_symbolt&>(expr);
325 #endif // CPROVER_SOLVERS_SMT2_SMT2_CONV_H void unflatten(wheret, const typet &, unsigned nesting=0)
The type of an expression, extends irept.
smt2_symbolt(const irep_idt &_identifier, const typet &_type)
exprt parse_union(const irept &s, const union_typet &type)
exprt convert_operands(const exprt &)
datatype_mapt datatype_map
virtual tvt l_get(literalt l) const
Semantic type conversion.
void flatten2bv(const exprt &)
An expression without operands.
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
exprt parse_array(const irept &s, const array_typet &type)
exprt letify(exprt &expr)
let_count_idt(std::size_t _count, const symbol_exprt &_let_symbol)
virtual resultt dec_solve()
void convert_literal(const literalt)
void convert_typecast(const typecast_exprt &expr)
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
void convert_expr(const exprt &)
void convert_constant(const constant_exprt &expr)
void convert_update(const exprt &expr)
const_iterator find(const Key &key) const
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
void convert_floatbv(const exprt &expr)
std::unordered_map< irep_idt, identifiert > identifier_mapt
void convert_plus(const plus_exprt &expr)
std::string type2id(const typet &) const
A constant literal expression.
Structure type, corresponds to C style structs.
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
virtual void set_assumptions(const bvt &bv)
identifier_mapt identifier_map
void convert_type(const typet &)
bool use_array_theory(const exprt &)
Extract member of struct or union.
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
exprt substitute_let(exprt &expr, const seen_expressionst &map)
virtual literalt convert(const exprt &expr)
void convert_mult(const mult_exprt &expr)
void convert_relation(const exprt &expr)
const irep_idt & id() const
void define_object_size(const irep_idt &id, const exprt &expr)
Expression classes for byte-level operators.
virtual void print_assignment(std::ostream &out) const
defined_expressionst object_sizes
void convert_mod(const mod_exprt &expr)
virtual std::string decision_procedure_text() const
void operator()(exprt &expr)
void convert_floatbv_div(const ieee_float_op_exprt &expr)
void convert_struct(const struct_exprt &expr)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
void convert_div(const div_exprt &expr)
Union constructor from single element.
API to expression classes.
void convert_index(const index_exprt &expr)
boolbv_widtht boolbv_width
exprt letify_rec(exprt &expr, std::vector< exprt > &let_order, const seen_expressionst &map, std::size_t i)
const irep_idt & get(const irep_namet &name) const
virtual void set_frozen(literalt)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
Base class for tree-like data structures with sharing.
std::string convert_identifier(const irep_idt &identifier)
The plus expression Associativity is not specified.
constant_exprt parse_literal(const irept &, const typet &type)
void convert_minus(const minus_exprt &expr)
const_iterator end() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::string floatbv_suffix(const exprt &) const
const irep_idt & get_identifier() const
bool has_operands() const
Return true if there is at least one operand.
smt2_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
Binary multiplication Associativity is not specified.
std::map< typet, std::string > datatype_mapt
typename mapt::const_iterator const_iterator
virtual exprt get(const exprt &expr) const
void convert_byte_update(const byte_update_exprt &expr)
void convert_is_dynamic_object(const exprt &expr)
void unflatten_array(const exprt &)
Semantic type conversion from/to floating-point formats.
const seen_expressionst & let_map
Base class for all expressions.
std::set< irep_idt > bvfp_set
let_visitort(const seen_expressionst &map)
Operator to update elements in structs and arrays.
void convert_overflow(const exprt &expr)
void find_symbols(const exprt &expr)
std::size_t no_boolean_variables
void convert_member(const member_exprt &expr)
exprt parse_rec(const irept &s, const typet &type)
void convert_union(const union_exprt &expr)
virtual void set_to(const exprt &expr, bool value)
static const std::size_t LET_COUNT
void convert_with(const with_exprt &expr)
Expression to hold a symbol (variable)
std::vector< bool > boolean_assignment
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
void convert_byte_extract(const byte_extract_exprt &expr)
std::map< exprt, irep_idt > defined_expressionst
exprt parse_struct(const irept &s, const struct_typet &type)
void write_footer(std::ostream &)
Struct constructor from list of elements.
std::set< std::string > smt2_identifierst
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
smt2_identifierst smt2_identifiers
std::vector< literalt > bvt
defined_expressionst defined_expressions
void set(const irep_namet &name, const irep_idt &value)
pointer_logict pointer_logic
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
void collect_bindings(exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
irep_hash_mapt< exprt, let_count_idt > seen_expressionst