cprover
cvc_convt Class Reference

#include <cvc_conv.h>

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

Classes

struct  identifiert
 

Public Member Functions

 cvc_convt (const namespacet &_ns, std::ostream &_out)
 
virtual ~cvc_convt ()
 
virtual void set_to (const exprt &expr, bool value)
 
virtual literalt convert (const exprt &expr)
 
virtual tvt l_get (literalt) const
 
virtual void print_assignment (std::ostream &out) const
 
- Public Member Functions inherited from prop_convt
 prop_convt (const namespacet &_ns)
 
virtual ~prop_convt ()
 
literalt operator() (const exprt &expr)
 
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
 
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 Types

typedef std::unordered_map< irep_idt, identifiert, irep_id_hashidentifier_mapt
 

Protected Member Functions

virtual void convert_expr (const exprt &expr)
 
virtual void convert_type (const typet &type)
 
virtual void convert_address_of_rec (const exprt &expr)
 

Protected Attributes

std::ostream & out
 
pointer_logict pointer_logic
 
unsigned no_boolean_variables
 
identifier_mapt identifier_map
 
std::vector< bool > boolean_assignment
 
- Protected Attributes inherited from decision_proceduret
const namespacetns
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Private Member Functions

void convert_identifier (const std::string &identifier)
 
void convert_typecast_expr (const exprt &expr)
 
void convert_binary_expr (const exprt &expr, const exprt &op)
 
void convert_struct_expr (const exprt &expr)
 
void convert_constant_expr (const exprt &expr)
 
void convert_equality_expr (const exprt &expr)
 
void convert_comparison_expr (const exprt &expr)
 
void convert_plus_expr (const exprt &expr)
 
void convert_minus_expr (const exprt &expr)
 
void convert_with_expr (const exprt &expr)
 
void convert_literal (const literalt l)
 
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 cvc_pointer_type ()
 

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 17 of file cvc_conv.h.

Member Typedef Documentation

◆ identifier_mapt

typedef std::unordered_map<irep_idt, identifiert, irep_id_hash> cvc_convt::identifier_mapt
protected

Definition at line 59 of file cvc_conv.h.

Constructor & Destructor Documentation

◆ cvc_convt()

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

Definition at line 20 of file cvc_conv.h.

◆ ~cvc_convt()

virtual cvc_convt::~cvc_convt ( )
inlinevirtual

Definition at line 28 of file cvc_conv.h.

Member Function Documentation

◆ array_index()

std::string cvc_convt::array_index ( unsigned  i)
staticprivate

Definition at line 522 of file cvc_conv.cpp.

References configt::ansi_c, config, configt::ansi_ct::int_width, and integer2binary().

Referenced by convert_constant_expr().

◆ array_index_type()

std::string cvc_convt::array_index_type ( )
staticprivate

Definition at line 509 of file cvc_conv.cpp.

Referenced by convert_constant_expr(), convert_expr(), and convert_type().

◆ bin_zero()

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

Definition at line 490 of file cvc_conv.cpp.

References messaget::result().

Referenced by convert_address_of_rec(), and convert_constant_expr().

◆ convert()

◆ convert_address_of_rec()

◆ convert_array_index()

void cvc_convt::convert_array_index ( const exprt expr)
private

◆ convert_array_value()

void cvc_convt::convert_array_value ( const exprt expr)
private

Definition at line 719 of file cvc_conv.cpp.

References convert_as_bv().

Referenced by convert_constant_expr(), convert_expr(), and convert_with_expr().

◆ convert_as_bv()

void cvc_convt::convert_as_bv ( const exprt expr)
private

◆ convert_binary_expr()

void cvc_convt::convert_binary_expr ( const exprt expr,
const exprt op 
)
private

◆ convert_comparison_expr()

void cvc_convt::convert_comparison_expr ( const exprt expr)
private

◆ convert_constant_expr()

◆ convert_equality_expr()

void cvc_convt::convert_equality_expr ( const exprt expr)
private

Definition at line 330 of file cvc_conv.cpp.

References convert_expr(), irept::id(), exprt::op0(), exprt::op1(), exprt::operands(), out, and exprt::type().

Referenced by convert_expr().

◆ convert_expr()

◆ convert_identifier()

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

Definition at line 664 of file cvc_conv.cpp.

References out.

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

◆ convert_literal()

void cvc_convt::convert_literal ( const literalt  l)
private

Definition at line 474 of file cvc_conv.cpp.

References const_literal(), out, literalt::sign(), and literalt::var_no().

Referenced by convert().

◆ convert_minus_expr()

void cvc_convt::convert_minus_expr ( const exprt expr)
private

◆ convert_plus_expr()

◆ convert_struct_expr()

void cvc_convt::convert_struct_expr ( const exprt expr)
private

◆ convert_type()

◆ convert_typecast_expr()

void cvc_convt::convert_typecast_expr ( const exprt expr)
private

◆ convert_with_expr()

void cvc_convt::convert_with_expr ( const exprt expr)
private

◆ cvc_pointer_type()

std::string cvc_convt::cvc_pointer_type ( )
staticprivate

◆ find_symbols() [1/2]

void cvc_convt::find_symbols ( const exprt expr)
private

◆ find_symbols() [2/2]

void cvc_convt::find_symbols ( const typet type)
private

Definition at line 1342 of file cvc_conv.cpp.

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

◆ gen_array_index_type()

typet cvc_convt::gen_array_index_type ( )
staticprivate

Definition at line 515 of file cvc_conv.cpp.

References irept::set().

Referenced by convert_array_index().

◆ l_get()

tvt cvc_convt::l_get ( literalt  l) const
virtual

◆ print_assignment()

void cvc_convt::print_assignment ( std::ostream &  out) const
virtual

Implements decision_proceduret.

Definition at line 25 of file cvc_conv.cpp.

References boolean_assignment, and out.

◆ set_to()

void cvc_convt::set_to ( const exprt expr,
bool  value 
)
virtual

Member Data Documentation

◆ boolean_assignment

std::vector<bool> cvc_convt::boolean_assignment
protected

◆ identifier_map

identifier_mapt cvc_convt::identifier_map
protected

Definition at line 61 of file cvc_conv.h.

Referenced by find_symbols(), and set_to().

◆ no_boolean_variables

unsigned cvc_convt::no_boolean_variables
protected

Definition at line 44 of file cvc_conv.h.

Referenced by convert(), cvc_dect::read_assert(), and cvc_dect::read_cvcl_result().

◆ out

◆ pointer_logic

pointer_logict cvc_convt::pointer_logic
protected

Definition at line 43 of file cvc_conv.h.

Referenced by convert_address_of_rec(), and convert_constant_expr().


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