cprover
smt1_convt Class Reference

#include <smt1_conv.h>

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

Classes

struct  identifiert
 

Public Types

enum  solvert {
  solvert::GENERIC, solvert::BOOLECTOR, solvert::CVC3, solvert::CVC4,
  solvert::MATHSAT, solvert::OPENSMT, solvert::YICES, solvert::Z3
}
 
- 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
}
 

Public Member Functions

 smt1_convt (const namespacet &_ns, const std::string &_benchmark, const std::string &_source, const std::string &_logic, solvert _solver, std::ostream &_out)
 
virtual ~smt1_convt ()
 
virtual resultt dec_solve ()
 
virtual literalt convert (const exprt &expr)
 
virtual void set_to (const exprt &expr, bool value)
 
virtual exprt get (const exprt &expr) const
 
virtual tvt l_get (literalt) const
 
virtual std::string decision_procedure_text () 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)
 
void set_to_true (const exprt &expr)
 
void set_to_false (const exprt &expr)
 
resultt operator() ()
 
virtual bool in_core (const exprt &expr)
 
- 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
 
typedef std::map< exprt, irep_idtarray_of_mapt
 
typedef std::map< exprt, irep_idtarray_expr_mapt
 
typedef std::map< exprt, exprtstring2array_mapt
 

Protected Member Functions

void write_header ()
 
void write_footer ()
 
void convert_expr (const exprt &expr, bool bool_as_bv)
 
void convert_type (const typet &type)
 
void convert_byte_update (const exprt &expr, bool bool_as_bv)
 
void convert_byte_extract (const byte_extract_exprt &expr, bool bool_as_bv)
 
void convert_typecast (const typecast_exprt &expr, bool bool_as_bv)
 
void convert_struct (const exprt &expr)
 
void convert_union (const exprt &expr)
 
void convert_constant (const constant_exprt &expr, bool bool_as_bv)
 
void convert_relation (const exprt &expr, bool bool_as_bv)
 
void convert_is_dynamic_object (const exprt &expr, bool bool_as_bv)
 
void convert_plus (const plus_exprt &expr)
 
void convert_minus (const minus_exprt &expr)
 
void convert_div (const div_exprt &expr)
 
void convert_mult (const mult_exprt &expr)
 
void convert_floatbv_plus (const exprt &expr)
 
void convert_floatbv_minus (const exprt &expr)
 
void convert_floatbv_div (const exprt &expr)
 
void convert_floatbv_mult (const exprt &expr)
 
void convert_mod (const mod_exprt &expr)
 
void convert_index (const index_exprt &expr, bool bool_as_bv)
 
void convert_member (const member_exprt &expr, bool bool_as_bv)
 
void convert_overflow (const exprt &expr)
 
void convert_with (const exprt &expr)
 
void convert_update (const exprt &expr)
 
std::string convert_identifier (const irep_idt &identifier)
 
void convert_literal (const literalt l)
 
void find_symbols (const exprt &expr)
 
void find_symbols (const typet &type)
 
void find_symbols_rec (const typet &type, std::set< irep_idt > &recstack)
 
void flatten_array (const exprt &op)
 
void from_bv_begin (const typet &type, bool bool_as_bv)
 
void from_bv_end (const typet &type, bool bool_as_bv)
 
void from_bool_begin (const typet &type, bool bool_as_bv)
 
void from_bool_end (const typet &type, bool bool_as_bv)
 
typet array_index_type () const
 
void array_index (const exprt &expr)
 
void convert_address_of_rec (const exprt &expr, const pointer_typet &result_type)
 
void set_value (identifiert &identifier, const std::string &index, const std::string &value)
 
exprt ce_value (const typet &type, const std::string &index, const std::string &v, bool in_struct) const
 
exprt binary2struct (const struct_typet &type, const std::string &binary) const
 
exprt binary2union (const union_typet &type, const std::string &binary) const
 
void convert_nary (const exprt &expr, const irep_idt op_string, bool bool_as_bv)
 

Protected Attributes

std::string benchmark
 
std::string source
 
std::string logic
 
solvert solver
 
std::ostream & out
 
boolbv_widtht boolbv_width
 
std::set< irep_idtquantified_symbols
 
pointer_logict pointer_logic
 
identifier_mapt identifier_map
 
unsigned array_index_bits
 
array_of_mapt array_of_map
 
array_expr_mapt array_expr_map
 
string2array_mapt string2array_map
 
unsigned no_boolean_variables
 
std::vector< bool > boolean_assignment
 
- Protected Attributes inherited from decision_proceduret
const namespacetns
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 31 of file smt1_conv.h.

Member Typedef Documentation

◆ array_expr_mapt

typedef std::map<exprt, irep_idt> smt1_convt::array_expr_mapt
protected

Definition at line 182 of file smt1_conv.h.

◆ array_of_mapt

typedef std::map<exprt, irep_idt> smt1_convt::array_of_mapt
protected

Definition at line 178 of file smt1_conv.h.

◆ identifier_mapt

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

Definition at line 171 of file smt1_conv.h.

◆ string2array_mapt

typedef std::map<exprt, exprt> smt1_convt::string2array_mapt
protected

Definition at line 186 of file smt1_conv.h.

Member Enumeration Documentation

◆ solvert

enum smt1_convt::solvert
strong
Enumerator
GENERIC 
BOOLECTOR 
CVC3 
CVC4 
MATHSAT 
OPENSMT 
YICES 
Z3 

Definition at line 34 of file smt1_conv.h.

Constructor & Destructor Documentation

◆ smt1_convt()

smt1_convt::smt1_convt ( const namespacet _ns,
const std::string &  _benchmark,
const std::string &  _source,
const std::string &  _logic,
solvert  _solver,
std::ostream &  _out 
)
inline

Definition at line 46 of file smt1_conv.h.

References write_header().

◆ ~smt1_convt()

virtual smt1_convt::~smt1_convt ( )
inlinevirtual

Definition at line 67 of file smt1_conv.h.

Member Function Documentation

◆ array_index()

void smt1_convt::array_index ( const exprt expr)
protected

◆ array_index_type()

typet smt1_convt::array_index_type ( ) const
protected

◆ binary2struct()

exprt smt1_convt::binary2struct ( const struct_typet type,
const std::string &  binary 
) const
protected

◆ binary2union()

exprt smt1_convt::binary2union ( const union_typet type,
const std::string &  binary 
) const
protected

◆ ce_value()

◆ convert()

◆ convert_address_of_rec()

◆ convert_byte_extract()

void smt1_convt::convert_byte_extract ( const byte_extract_exprt expr,
bool  bool_as_bv 
)
protected

Definition at line 356 of file smt1_conv.cpp.

References convert_expr(), flatten_byte_extract(), and decision_proceduret::ns.

Referenced by convert_expr().

◆ convert_byte_update()

void smt1_convt::convert_byte_update ( const exprt expr,
bool  bool_as_bv 
)
protected

◆ convert_constant()

◆ convert_div()

void smt1_convt::convert_div ( const div_exprt expr)
protected

◆ convert_expr()

void smt1_convt::convert_expr ( const exprt expr,
bool  bool_as_bv 
)
protected

Definition at line 531 of file smt1_conv.cpp.

References array_expr_map, array_index_bits, array_of_map, base_type_eq(), boolbv_width, BV_ADDR_BITS, convert_address_of_rec(), convert_byte_extract(), convert_byte_update(), convert_constant(), convert_div(), convert_floatbv_div(), convert_floatbv_minus(), convert_floatbv_mult(), convert_floatbv_plus(), convert_identifier(), convert_index(), convert_is_dynamic_object(), convert_literal(), convert_member(), convert_minus(), convert_mod(), convert_mult(), convert_nary(), convert_plus(), convert_relation(), convert_struct(), convert_type(), convert_typecast(), convert_union(), convert_update(), convert_with(), namespace_baset::follow(), forall_expr, from_bool_begin(), from_bool_end(), from_bv_begin(), from_bv_end(), from_integer(), irept::get(), symbol_exprt::get_identifier(), pointer_logict::get_invalid_object(), irept::id(), irept::id_string(), exprt::is_constant(), decision_proceduret::ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), out, pointer_logic, power(), string2array_map, to_byte_extract_expr(), to_constant_expr(), to_div_expr(), to_index_expr(), to_integer(), to_literal_expr(), to_member_expr(), to_minus_expr(), to_mod_expr(), to_mult_expr(), to_plus_expr(), to_pointer_type(), to_symbol_expr(), to_typecast_expr(), and exprt::type().

Referenced by array_index(), convert(), convert_address_of_rec(), convert_byte_extract(), convert_byte_update(), convert_div(), convert_index(), convert_is_dynamic_object(), convert_member(), convert_minus(), convert_mod(), convert_mult(), convert_nary(), convert_plus(), convert_relation(), convert_struct(), convert_typecast(), convert_union(), convert_with(), find_symbols(), flatten_array(), and set_to().

◆ convert_floatbv_div()

void smt1_convt::convert_floatbv_div ( const exprt expr)
protected

Definition at line 2215 of file smt1_conv.cpp.

References irept::id(), exprt::operands(), and exprt::type().

Referenced by convert_expr().

◆ convert_floatbv_minus()

void smt1_convt::convert_floatbv_minus ( const exprt expr)
protected

Definition at line 2168 of file smt1_conv.cpp.

References irept::id(), exprt::operands(), and exprt::type().

Referenced by convert_expr().

◆ convert_floatbv_mult()

void smt1_convt::convert_floatbv_mult ( const exprt expr)
protected

Definition at line 2286 of file smt1_conv.cpp.

References irept::id(), exprt::operands(), and exprt::type().

Referenced by convert_expr().

◆ convert_floatbv_plus()

void smt1_convt::convert_floatbv_plus ( const exprt expr)
protected

Definition at line 2121 of file smt1_conv.cpp.

References irept::id(), exprt::operands(), and exprt::type().

Referenced by convert_expr().

◆ convert_identifier()

std::string smt1_convt::convert_identifier ( const irep_idt identifier)
protected

◆ convert_index()

void smt1_convt::convert_index ( const index_exprt expr,
bool  bool_as_bv 
)
protected

◆ convert_is_dynamic_object()

void smt1_convt::convert_is_dynamic_object ( const exprt expr,
bool  bool_as_bv 
)
protected

◆ convert_literal()

void smt1_convt::convert_literal ( const literalt  l)
protected

Definition at line 2978 of file smt1_conv.cpp.

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

Referenced by convert(), and convert_expr().

◆ convert_member()

◆ convert_minus()

void smt1_convt::convert_minus ( const minus_exprt expr)
protected

◆ convert_mod()

void smt1_convt::convert_mod ( const mod_exprt expr)
protected

◆ convert_mult()

void smt1_convt::convert_mult ( const mult_exprt expr)
protected

◆ convert_nary()

void smt1_convt::convert_nary ( const exprt expr,
const irep_idt  op_string,
bool  bool_as_bv 
)
protected

Definition at line 3191 of file smt1_conv.cpp.

References convert_expr(), exprt::op0(), exprt::operands(), and out.

Referenced by convert_expr(), and convert_plus().

◆ convert_overflow()

void smt1_convt::convert_overflow ( const exprt expr)
protected

Definition at line 2743 of file smt1_conv.cpp.

◆ convert_plus()

◆ convert_relation()

void smt1_convt::convert_relation ( const exprt expr,
bool  bool_as_bv 
)
protected

◆ convert_struct()

void smt1_convt::convert_struct ( const exprt expr)
protected

◆ convert_type()

◆ convert_typecast()

◆ convert_union()

void smt1_convt::convert_union ( const exprt expr)
protected

◆ convert_update()

void smt1_convt::convert_update ( const exprt expr)
protected

Definition at line 2634 of file smt1_conv.cpp.

References exprt::operands().

Referenced by convert_expr().

◆ convert_with()

◆ dec_solve()

decision_proceduret::resultt smt1_convt::dec_solve ( )
virtual

Implements decision_proceduret.

Reimplemented in smt1_dect.

Definition at line 55 of file smt1_conv.cpp.

References decision_proceduret::D_ERROR, out, and write_footer().

◆ decision_procedure_text()

virtual std::string smt1_convt::decision_procedure_text ( ) const
inlinevirtual

Implements decision_proceduret.

Reimplemented in smt1_dect.

Definition at line 75 of file smt1_conv.h.

◆ find_symbols() [1/2]

◆ find_symbols() [2/2]

void smt1_convt::find_symbols ( const typet type)
protected

Definition at line 3024 of file smt1_conv.cpp.

References find_symbols_rec().

◆ find_symbols_rec()

◆ flatten_array()

void smt1_convt::flatten_array ( const exprt op)
protected

◆ from_bool_begin()

void smt1_convt::from_bool_begin ( const typet type,
bool  bool_as_bv 
)
protected

Definition at line 3010 of file smt1_conv.cpp.

References irept::id(), and out.

Referenced by convert_expr(), convert_is_dynamic_object(), convert_relation(), and convert_typecast().

◆ from_bool_end()

void smt1_convt::from_bool_end ( const typet type,
bool  bool_as_bv 
)
protected

Definition at line 3017 of file smt1_conv.cpp.

References irept::id(), and out.

Referenced by convert_expr(), convert_is_dynamic_object(), convert_relation(), and convert_typecast().

◆ from_bv_begin()

void smt1_convt::from_bv_begin ( const typet type,
bool  bool_as_bv 
)
protected

Definition at line 2996 of file smt1_conv.cpp.

References irept::id(), and out.

Referenced by convert_expr(), convert_index(), and convert_member().

◆ from_bv_end()

void smt1_convt::from_bv_end ( const typet type,
bool  bool_as_bv 
)
protected

Definition at line 3003 of file smt1_conv.cpp.

References irept::id(), and out.

Referenced by convert_expr(), convert_index(), and convert_member().

◆ get()

◆ l_get()

tvt smt1_convt::l_get ( literalt  l) const
virtual

◆ print_assignment()

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

Implements decision_proceduret.

Definition at line 35 of file smt1_conv.cpp.

References boolean_assignment, and out.

◆ set_to()

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

◆ set_value()

void smt1_convt::set_value ( identifiert identifier,
const std::string &  index,
const std::string &  value 
)
inlineprotected

◆ write_footer()

void smt1_convt::write_footer ( )
protected

Definition at line 70 of file smt1_conv.cpp.

References out.

Referenced by smt1_dect::dec_solve(), and dec_solve().

◆ write_header()

void smt1_convt::write_header ( )
protected

Definition at line 62 of file smt1_conv.cpp.

References benchmark, logic, out, and source.

Referenced by smt1_convt().

Member Data Documentation

◆ array_expr_map

array_expr_mapt smt1_convt::array_expr_map
protected

Definition at line 183 of file smt1_conv.h.

Referenced by convert_expr(), and find_symbols().

◆ array_index_bits

unsigned smt1_convt::array_index_bits
protected

◆ array_of_map

array_of_mapt smt1_convt::array_of_map
protected

◆ benchmark

std::string smt1_convt::benchmark
protected

Definition at line 79 of file smt1_conv.h.

Referenced by write_header().

◆ boolbv_width

◆ boolean_assignment

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

◆ identifier_map

◆ logic

std::string smt1_convt::logic
protected

Definition at line 79 of file smt1_conv.h.

Referenced by write_header().

◆ no_boolean_variables

unsigned smt1_convt::no_boolean_variables
protected

◆ out

◆ pointer_logic

pointer_logict smt1_convt::pointer_logic
protected

◆ quantified_symbols

std::set<irep_idt> smt1_convt::quantified_symbols
protected

Definition at line 121 of file smt1_conv.h.

Referenced by find_symbols().

◆ solver

solvert smt1_convt::solver
protected

Definition at line 80 of file smt1_conv.h.

Referenced by smt1_dect::dec_solve(), and smt1_dect::decision_procedure_text().

◆ source

std::string smt1_convt::source
protected

Definition at line 79 of file smt1_conv.h.

Referenced by write_header().

◆ string2array_map

string2array_mapt smt1_convt::string2array_map
protected

Definition at line 187 of file smt1_conv.h.

Referenced by convert_expr(), and find_symbols().


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