cprover
dplib_convt Class Reference

#include <dplib_conv.h>

Inheritance diagram for dplib_convt:
[legend]
Collaboration diagram for dplib_convt:
[legend]

Classes

struct  identifiert
 

Public Member Functions

 dplib_convt (const namespacet &_ns, std::ostream &_out)
 
virtual ~dplib_convt ()
 
- Public Member Functions inherited from prop_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
 
- Public Member Functions inherited from decision_proceduret
 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
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

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
 
- Protected Attributes inherited from decision_proceduret
const namespacetns
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Private Types

typedef std::unordered_map< irep_idt, identifiert, irep_id_hashidentifier_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

- Public Types inherited from decision_proceduret
enum  resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR }
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 19 of file dplib_conv.h.

Member Typedef Documentation

§ identifier_mapt

typedef std::unordered_map<irep_idt, identifiert, irep_id_hash> dplib_convt::identifier_mapt
private

Definition at line 68 of file dplib_conv.h.

Constructor & Destructor Documentation

§ dplib_convt()

dplib_convt::dplib_convt ( const namespacet _ns,
std::ostream &  _out 
)
inline

Definition at line 22 of file dplib_conv.h.

§ ~dplib_convt()

virtual dplib_convt::~dplib_convt ( )
inlinevirtual

Definition at line 29 of file dplib_conv.h.

Member Function Documentation

§ array_index()

std::string dplib_convt::array_index ( unsigned  i)
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().

§ array_index_type()

std::string dplib_convt::array_index_type ( )
staticprivate

Definition at line 39 of file dplib_conv.cpp.

Referenced by convert_dplib_expr(), and convert_dplib_type().

§ bin_zero()

std::string dplib_convt::bin_zero ( unsigned  bits)
staticprivate

Definition at line 24 of file dplib_conv.cpp.

References messaget::result().

Referenced by convert_address_of_rec(), and convert_dplib_expr().

§ convert_address_of_rec()

§ convert_array_index()

void dplib_convt::convert_array_index ( const exprt expr)
private

§ convert_array_value()

void dplib_convt::convert_array_value ( const exprt expr)
private

Definition at line 224 of file dplib_conv.cpp.

References convert_as_bv().

Referenced by convert_dplib_expr().

§ convert_as_bv()

void dplib_convt::convert_as_bv ( const exprt 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().

§ convert_dplib_expr()

§ convert_dplib_type()

§ convert_identifier()

void dplib_convt::convert_identifier ( const std::string &  identifier)
private

Definition at line 176 of file dplib_conv.cpp.

Referenced by convert_dplib_expr(), find_symbols(), and set_to().

§ convert_rest()

literalt dplib_convt::convert_rest ( const exprt expr)
protectedvirtual

§ dplib_pointer_type()

std::string dplib_convt::dplib_pointer_type ( )
staticprivate

§ find_symbols() [1/2]

void dplib_convt::find_symbols ( const exprt expr)
private

§ find_symbols() [2/2]

void dplib_convt::find_symbols ( const typet type)
private

Definition at line 1159 of file dplib_conv.cpp.

References find_symbols(), irept::id(), array_typet::size(), and to_array_type().

§ gen_array_index_type()

typet dplib_convt::gen_array_index_type ( )
staticprivate

Definition at line 44 of file dplib_conv.cpp.

References irept::set().

Referenced by convert_array_index().

§ set_to()

Member Data Documentation

§ identifier_map

identifier_mapt dplib_convt::identifier_map
private

Definition at line 70 of file dplib_conv.h.

Referenced by find_symbols(), and set_to().

§ out

std::ostream& dplib_convt::out
protected

Definition at line 32 of file dplib_conv.h.

§ pointer_logic

pointer_logict dplib_convt::pointer_logic
protected

Definition at line 40 of file dplib_conv.h.

Referenced by convert_address_of_rec(), and convert_dplib_expr().


The documentation for this class was generated from the following files: