cprover
|
#include <dplib_conv.h>
Classes | |
struct | identifiert |
Public Member Functions | |
dplib_convt (const namespacet &_ns, std::ostream &_out) | |
virtual | ~dplib_convt () |
![]() | |
prop_convt (const namespacet &_ns) | |
virtual | ~prop_convt () |
virtual literalt | convert (const exprt &expr)=0 |
literalt | operator() (const exprt &expr) |
virtual tvt | l_get (literalt a) const =0 |
virtual void | set_frozen (literalt a) |
virtual void | set_frozen (const bvt &) |
virtual void | set_assumptions (const bvt &_assumptions) |
virtual bool | has_set_assumptions () const |
virtual void | set_all_frozen () |
virtual bool | is_in_conflict (literalt l) const |
determine whether a variable is in the final conflict More... | |
virtual bool | has_is_in_conflict () const |
![]() | |
decision_proceduret (const namespacet &_ns) | |
virtual exprt | get (const exprt &expr) const =0 |
virtual void | print_assignment (std::ostream &out) const =0 |
void | set_to_true (const exprt &expr) |
void | set_to_false (const exprt &expr) |
virtual resultt | dec_solve ()=0 |
resultt | operator() () |
virtual bool | in_core (const exprt &expr) |
virtual std::string | decision_procedure_text () const =0 |
Protected Member Functions | |
virtual literalt | convert_rest (const exprt &expr) |
virtual void | convert_dplib_expr (const exprt &expr) |
virtual void | convert_dplib_type (const typet &type) |
virtual void | set_to (const exprt &expr, bool value) |
virtual void | convert_address_of_rec (const exprt &expr) |
Protected Attributes | |
std::ostream & | out |
pointer_logict | pointer_logic |
![]() | |
const namespacet & | ns |
Private Types | |
typedef std::unordered_map< irep_idt, identifiert, irep_id_hash > | identifier_mapt |
Private Member Functions | |
void | convert_identifier (const std::string &identifier) |
void | find_symbols (const exprt &expr) |
void | find_symbols (const typet &type) |
void | convert_array_value (const exprt &expr) |
void | convert_as_bv (const exprt &expr) |
void | convert_array_index (const exprt &expr) |
Static Private Member Functions | |
static typet | gen_array_index_type () |
static std::string | bin_zero (unsigned bits) |
static std::string | array_index_type () |
static std::string | array_index (unsigned i) |
static std::string | dplib_pointer_type () |
Private Attributes | |
identifier_mapt | identifier_map |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
Definition at line 19 of file dplib_conv.h.
|
private |
Definition at line 68 of file dplib_conv.h.
|
inline |
Definition at line 22 of file dplib_conv.h.
|
inlinevirtual |
Definition at line 29 of file dplib_conv.h.
|
staticprivate |
Definition at line 51 of file dplib_conv.cpp.
References configt::ansi_c, config, configt::ansi_ct::int_width, and integer2binary().
Referenced by convert_dplib_expr().
|
staticprivate |
Definition at line 39 of file dplib_conv.cpp.
Referenced by convert_dplib_expr(), and convert_dplib_type().
|
staticprivate |
Definition at line 24 of file dplib_conv.cpp.
References messaget::result().
Referenced by convert_address_of_rec(), and convert_dplib_expr().
|
protectedvirtual |
Definition at line 70 of file dplib_conv.cpp.
References pointer_logict::add_object(), configt::ansi_c, bin_zero(), config, convert_dplib_expr(), dplib_pointer_type(), from_integer(), member_exprt::get_component_name(), irept::id(), irept::id_string(), index_type(), exprt::is_zero(), member_offset(), decision_proceduret::ns, exprt::op0(), exprt::op1(), exprt::operands(), pointer_logic, configt::ansi_ct::pointer_width, irept::set(), to_member_expr(), to_struct_type(), and exprt::type().
Referenced by convert_dplib_expr().
|
private |
Definition at line 56 of file dplib_conv.cpp.
References convert_dplib_expr(), exprt::copy_to_operands(), gen_array_index_type(), and exprt::type().
Referenced by convert_dplib_expr().
|
private |
Definition at line 224 of file dplib_conv.cpp.
References convert_as_bv().
Referenced by convert_dplib_expr().
|
private |
Definition at line 212 of file dplib_conv.cpp.
References convert_dplib_expr(), irept::id(), and exprt::type().
Referenced by convert_array_value(), and convert_dplib_expr().
|
protectedvirtual |
Definition at line 229 of file dplib_conv.cpp.
References configt::ansi_c, array_index(), array_index_type(), bin_zero(), struct_union_typet::components(), config, convert_address_of_rec(), convert_array_index(), convert_array_value(), convert_as_bv(), convert_identifier(), dplib_pointer_type(), forall_operands, from_integer(), irept::get(), pointer_logict::get_null_object(), irept::get_string(), irept::id(), id2string(), irept::id_string(), exprt::is_false(), exprt::is_true(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), pointer_logic, configt::ansi_ct::pointer_width, to_array_expr(), to_integer(), to_string_constant(), to_struct_type(), exprt::type(), and unsafe_string2unsigned().
Referenced by convert_address_of_rec(), convert_array_index(), convert_as_bv(), convert_rest(), and set_to().
|
protectedvirtual |
Definition at line 1076 of file dplib_conv.cpp.
References array_index_type(), struct_union_typet::components(), dplib_pointer_type(), bitvector_typet::get_width(), irept::id(), irept::id_string(), typet::subtype(), to_array_type(), to_bv_type(), to_signedbv_type(), to_struct_type(), and to_unsignedbv_type().
Referenced by find_symbols(), and set_to().
|
private |
Definition at line 176 of file dplib_conv.cpp.
Referenced by convert_dplib_expr(), find_symbols(), and set_to().
Definition at line 154 of file dplib_conv.cpp.
References convert_dplib_expr(), find_symbols(), irept::id(), exprt::op0(), exprt::op1(), and exprt::operands().
|
staticprivate |
Definition at line 32 of file dplib_conv.cpp.
References configt::ansi_c, config, and configt::ansi_ct::pointer_width.
Referenced by convert_address_of_rec(), convert_dplib_expr(), and convert_dplib_type().
|
private |
Definition at line 1029 of file dplib_conv.cpp.
References convert_dplib_type(), convert_identifier(), forall_operands, irept::get(), irept::get_string(), irept::id(), id2string(), identifier_map, and exprt::type().
Referenced by convert_rest(), find_symbols(), and set_to().
|
private |
Definition at line 1159 of file dplib_conv.cpp.
References find_symbols(), irept::id(), array_typet::size(), and to_array_type().
|
staticprivate |
Definition at line 44 of file dplib_conv.cpp.
References irept::set().
Referenced by convert_array_index().
|
protectedvirtual |
Implements decision_proceduret.
Definition at line 965 of file dplib_conv.cpp.
References convert_dplib_expr(), convert_dplib_type(), convert_identifier(), find_symbols(), forall_operands, irept::get(), irept::id(), id2string(), identifier_map, exprt::is_true(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
|
private |
Definition at line 70 of file dplib_conv.h.
Referenced by find_symbols(), and set_to().
|
protected |
Definition at line 32 of file dplib_conv.h.
|
protected |
Definition at line 40 of file dplib_conv.h.
Referenced by convert_address_of_rec(), and convert_dplib_expr().