cprover
smt2_convt Class Reference

#include <smt2_conv.h>

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

Classes

struct  identifiert
 
class  let_visitort
 
class  smt2_symbolt
 

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

 smt2_convt (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
 
virtual ~smt2_convt ()
 
virtual resultt dec_solve ()
 
virtual literalt convert (const exprt &expr)
 
virtual void set_frozen (literalt a)
 
virtual void set_to (const exprt &expr, bool value)
 
virtual exprt get (const exprt &expr) const
 
virtual std::string decision_procedure_text () const
 
virtual void print_assignment (std::ostream &out) const
 
virtual tvt l_get (literalt l) const
 
virtual void set_assumptions (const bvt &bv)
 
void convert_expr (const exprt &)
 
void convert_type (const typet &)
 
void convert_literal (const literalt)
 
- Public Member Functions inherited from prop_convt
 prop_convt (const namespacet &_ns)
 
virtual ~prop_convt ()
 
literalt operator() (const exprt &expr)
 
virtual void set_frozen (const bvt &)
 
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 ()
 

Public Attributes

bool use_FPA_theory
 
bool use_datatypes
 
bool use_array_of_bool
 
bool emit_set_logic
 

Protected Types

enum  wheret { wheret::BEGIN, wheret::END }
 
typedef std::pair< unsigned, symbol_exprtlet_count_idt
 
typedef std::unordered_map< exprt, let_count_idt, irep_hashseen_expressionst
 
typedef std::unordered_map< irep_idt, identifiert, irep_id_hashidentifier_mapt
 
typedef std::map< typet, std::string > datatype_mapt
 
typedef std::map< exprt, irep_idtdefined_expressionst
 
typedef std::set< std::string > smt2_identifierst
 

Protected Member Functions

void write_header ()
 
void write_footer (std::ostream &)
 
bool use_array_theory (const exprt &)
 
void flatten_array (const exprt &)
 produce a flat bit-vector for a given array of fixed size More...
 
void unflatten_array (const exprt &)
 
void convert_byte_update (const byte_update_exprt &expr)
 
void convert_byte_extract (const byte_extract_exprt &expr)
 
void convert_typecast (const typecast_exprt &expr)
 
void convert_floatbv_typecast (const floatbv_typecast_exprt &expr)
 
void convert_struct (const struct_exprt &expr)
 
void convert_union (const union_exprt &expr)
 
void convert_constant (const constant_exprt &expr)
 
void convert_relation (const exprt &expr)
 
void convert_is_dynamic_object (const exprt &expr)
 
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_rounding_mode_FPA (const exprt &expr)
 Converting a constant or symbolic rounding mode to SMT-LIB. More...
 
void convert_floatbv_plus (const ieee_float_op_exprt &expr)
 
void convert_floatbv_minus (const ieee_float_op_exprt &expr)
 
void convert_floatbv_div (const ieee_float_op_exprt &expr)
 
void convert_floatbv_mult (const ieee_float_op_exprt &expr)
 
void convert_mod (const mod_exprt &expr)
 
void convert_index (const index_exprt &expr)
 
void convert_member (const member_exprt &expr)
 
void convert_overflow (const exprt &expr)
 
void convert_with (const with_exprt &expr)
 
void convert_update (const exprt &expr)
 
std::string convert_identifier (const irep_idt &identifier)
 
exprt convert_operands (const exprt &)
 
void find_symbols (const exprt &expr)
 
void find_symbols (const typet &type)
 
void find_symbols_rec (const typet &type, std::set< irep_idt > &recstack)
 
exprt letify (exprt &expr)
 
exprt letify_rec (exprt &expr, std::vector< exprt > &let_order, const seen_expressionst &map, unsigned i)
 
void collect_bindings (exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
 
exprt substitute_let (exprt &expr, const seen_expressionst &map)
 
constant_exprt parse_literal (const irept &, const typet &type)
 
exprt parse_struct (const irept &s, const struct_typet &type)
 
exprt parse_union (const irept &s, const union_typet &type)
 
exprt parse_array (const irept &s, const array_typet &type)
 
exprt parse_rec (const irept &s, const typet &type)
 
void convert_floatbv (const exprt &expr)
 
std::string type2id (const typet &) const
 
std::string floatbv_suffix (const exprt &) const
 
const smt2_symboltto_smt2_symbol (const exprt &expr)
 
void flatten2bv (const exprt &)
 
void unflatten (wheret, const typet &, unsigned nesting=0)
 
void convert_address_of_rec (const exprt &expr, const pointer_typet &result_type)
 
void define_object_size (const irep_idt &id, const exprt &expr)
 

Protected Attributes

std::ostream & out
 
std::string benchmark
 
std::string notes
 
std::string logic
 
solvert solver
 
bvt assumptions
 
boolbv_widtht boolbv_width
 
unsigned let_id_count
 
std::set< irep_idtbvfp_set
 
pointer_logict pointer_logic
 
identifier_mapt identifier_map
 
datatype_mapt datatype_map
 
defined_expressionst defined_expressions
 
defined_expressionst object_sizes
 
smt2_identifierst smt2_identifiers
 
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
 

Static Protected Attributes

static const unsigned LET_COUNT =2
 

Additional Inherited Members

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

Detailed Description

Definition at line 28 of file smt2_conv.h.

Member Typedef Documentation

§ datatype_mapt

typedef std::map<typet, std::string> smt2_convt::datatype_mapt
protected

Definition at line 284 of file smt2_conv.h.

§ defined_expressionst

typedef std::map<exprt, irep_idt> smt2_convt::defined_expressionst
protected

Definition at line 293 of file smt2_conv.h.

§ identifier_mapt

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

Definition at line 278 of file smt2_conv.h.

§ let_count_idt

typedef std::pair<unsigned, symbol_exprt> smt2_convt::let_count_idt
protected

Definition at line 177 of file smt2_conv.h.

§ seen_expressionst

typedef std::unordered_map<exprt, let_count_idt, irep_hash> smt2_convt::seen_expressionst
protected

Definition at line 178 of file smt2_conv.h.

§ smt2_identifierst

typedef std::set<std::string> smt2_convt::smt2_identifierst
protected

Definition at line 298 of file smt2_conv.h.

Member Enumeration Documentation

§ solvert

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

Definition at line 31 of file smt2_conv.h.

§ wheret

enum smt2_convt::wheret
strongprotected
Enumerator
BEGIN 
END 

Definition at line 253 of file smt2_conv.h.

Constructor & Destructor Documentation

§ smt2_convt()

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

§ ~smt2_convt()

virtual smt2_convt::~smt2_convt ( )
inlinevirtual

Definition at line 101 of file smt2_conv.h.

References dec_solve().

Member Function Documentation

§ collect_bindings()

void smt2_convt::collect_bindings ( exprt expr,
seen_expressionst map,
std::vector< exprt > &  let_order 
)
protected

§ convert()

§ convert_address_of_rec()

§ convert_byte_extract()

void smt2_convt::convert_byte_extract ( const byte_extract_exprt expr)
protected

§ convert_byte_update()

§ convert_constant()

§ convert_div()

§ convert_expr()

void smt2_convt::convert_expr ( const exprt expr)

Definition at line 846 of file smt2_conv.cpp.

References base_type_eq(), boolbv_width, BV_ADDR_BITS, convert_address_of_rec(), convert_byte_extract(), convert_byte_update(), convert_constant(), convert_div(), convert_floatbv(), convert_floatbv_div(), convert_floatbv_minus(), convert_floatbv_mult(), convert_floatbv_plus(), convert_floatbv_typecast(), convert_identifier(), convert_index(), convert_is_dynamic_object(), convert_literal(), convert_member(), convert_minus(), convert_mod(), convert_mult(), convert_plus(), convert_relation(), convert_struct(), convert_type(), convert_typecast(), convert_union(), convert_update(), convert_with(), datatype_map, defined_expressions, flatten2bv(), forall_operands, from_integer(), irept::get(), symbol_exprt::get_identifier(), pointer_logict::get_invalid_object(), bitvector_typet::get_width(), irept::id(), id2string(), irept::id_string(), index_type(), INVALIDEXPR, exprt::is_constant(), MATHSAT, decision_proceduret::ns, object_sizes, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), out, pointer_logic, power(), vector_typet::size(), SMT2_TODO, solver, let_exprt::symbol(), to_byte_extract_expr(), to_byte_update_expr(), to_constant_expr(), to_div_expr(), to_fixedbv_type(), to_floatbv_typecast_expr(), to_ieee_float_op_expr(), to_index_expr(), to_integer(), to_let_expr(), to_literal_expr(), to_member_expr(), to_minus_expr(), to_mod_expr(), to_mult_expr(), to_plus_expr(), to_pointer_type(), to_signedbv_type(), to_struct_expr(), to_symbol_expr(), to_typecast_expr(), to_union_expr(), to_vector_type(), to_with_expr(), exprt::type(), UNEXPECTEDCASE, use_datatypes, use_FPA_theory, let_exprt::value(), and let_exprt::where().

Referenced by convert(), convert_address_of_rec(), convert_byte_extract(), convert_div(), convert_floatbv(), convert_floatbv_div(), convert_floatbv_minus(), convert_floatbv_mult(), convert_floatbv_plus(), convert_floatbv_typecast(), convert_index(), convert_is_dynamic_object(), convert_member(), convert_minus(), convert_mod(), convert_mult(), convert_plus(), convert_relation(), convert_rounding_mode_FPA(), convert_struct(), convert_typecast(), convert_with(), define_object_size(), find_symbols(), flatten2bv(), flatten_array(), set_assumptions(), and set_to().

§ convert_floatbv()

§ convert_floatbv_div()

void smt2_convt::convert_floatbv_div ( const ieee_float_op_exprt expr)
protected

§ convert_floatbv_minus()

void smt2_convt::convert_floatbv_minus ( const ieee_float_op_exprt expr)
protected

§ convert_floatbv_mult()

void smt2_convt::convert_floatbv_mult ( const ieee_float_op_exprt expr)
protected

§ convert_floatbv_plus()

§ convert_floatbv_typecast()

§ convert_identifier()

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

§ convert_index()

§ convert_is_dynamic_object()

void smt2_convt::convert_is_dynamic_object ( const exprt expr)
protected

§ convert_literal()

void smt2_convt::convert_literal ( const literalt  l)

§ convert_member()

§ convert_minus()

§ convert_mod()

void smt2_convt::convert_mod ( const mod_exprt expr)
protected

§ convert_mult()

§ convert_operands()

exprt smt2_convt::convert_operands ( const exprt )
protected

§ convert_overflow()

void smt2_convt::convert_overflow ( const exprt expr)
protected

Definition at line 3952 of file smt2_conv.cpp.

References UNREACHABLE.

§ convert_plus()

§ convert_relation()

void smt2_convt::convert_relation ( const exprt expr)
protected

§ convert_rounding_mode_FPA()

void smt2_convt::convert_rounding_mode_FPA ( const exprt expr)
protected

Converting a constant or symbolic rounding mode to SMT-LIB.

Only called when use_FPA_theory is enabled

parameters: The expression representing the rounding mode.
Returns
SMT-LIB output to out.

Definition at line 2958 of file smt2_conv.cpp.

References binary2integer(), convert_expr(), constant_exprt::get_value(), irept::id(), id2string(), INVALIDEXPR, out, to_bitvector_type(), to_constant_expr(), exprt::type(), and use_FPA_theory.

Referenced by convert_floatbv_div(), convert_floatbv_minus(), convert_floatbv_mult(), convert_floatbv_plus(), and convert_floatbv_typecast().

§ convert_struct()

§ convert_type()

§ convert_typecast()

§ convert_union()

void smt2_convt::convert_union ( const union_exprt expr)
protected

§ convert_update()

void smt2_convt::convert_update ( const exprt expr)
protected

Definition at line 3567 of file smt2_conv.cpp.

References exprt::operands(), and SMT2_TODO.

Referenced by convert_expr().

§ convert_with()

§ dec_solve()

decision_proceduret::resultt smt2_convt::dec_solve ( )
virtual

Implements decision_proceduret.

Reimplemented in smt2_dect.

Definition at line 172 of file smt2_conv.cpp.

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

Referenced by ~smt2_convt().

§ decision_procedure_text()

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

Implements decision_proceduret.

Reimplemented in smt2_dect.

Definition at line 114 of file smt2_conv.h.

References l_get(), out, and print_assignment().

§ define_object_size()

void smt2_convt::define_object_size ( const irep_idt id,
const exprt expr 
)
protected

§ find_symbols() [1/2]

§ find_symbols() [2/2]

void smt2_convt::find_symbols ( const typet type)
protected

Definition at line 4411 of file smt2_conv.cpp.

References find_symbols_rec().

§ find_symbols_rec()

§ flatten2bv()

§ flatten_array()

void smt2_convt::flatten_array ( const exprt expr)
protected

produce a flat bit-vector for a given array of fixed size

Definition at line 2489 of file smt2_conv.cpp.

References convert_expr(), namespace_baset::follow(), from_integer(), INVALIDEXPR, decision_proceduret::ns, out, array_typet::size(), to_array_type(), to_integer(), and exprt::type().

Referenced by convert_struct().

§ floatbv_suffix()

std::string smt2_convt::floatbv_suffix ( const exprt expr) const
protected

§ get()

§ l_get()

tvt smt2_convt::l_get ( literalt  l) const
virtual

§ letify()

exprt smt2_convt::letify ( exprt expr)
protected

Definition at line 4613 of file smt2_conv.cpp.

References collect_bindings(), and letify_rec().

Referenced by find_symbols(), and smt2_convt::let_visitort::operator()().

§ letify_rec()

exprt smt2_convt::letify_rec ( exprt expr,
std::vector< exprt > &  let_order,
const seen_expressionst map,
unsigned  i 
)
protected

§ parse_array()

exprt smt2_convt::parse_array ( const irept s,
const array_typet type 
)
protected

§ parse_literal()

§ parse_rec()

§ parse_struct()

§ parse_union()

exprt smt2_convt::parse_union ( const irept s,
const union_typet type 
)
protected

§ print_assignment()

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

Implements decision_proceduret.

Definition at line 51 of file smt2_conv.cpp.

References boolean_assignment.

Referenced by decision_procedure_text().

§ set_assumptions()

virtual void smt2_convt::set_assumptions ( const bvt bv)
inlinevirtual

Reimplemented from prop_convt.

Definition at line 117 of file smt2_conv.h.

References assumptions, convert_expr(), convert_literal(), and convert_type().

§ set_frozen()

virtual void smt2_convt::set_frozen ( literalt  a)
inlinevirtual

Reimplemented from prop_convt.

Definition at line 111 of file smt2_conv.h.

References set_to().

§ set_to()

§ substitute_let()

exprt smt2_convt::substitute_let ( exprt expr,
const seen_expressionst map 
)
protected

Definition at line 4678 of file smt2_conv.cpp.

References Forall_operands, and exprt::operands().

Referenced by letify_rec(), and smt2_convt::let_visitort::operator()().

§ to_smt2_symbol()

const smt2_symbolt& smt2_convt::to_smt2_symbol ( const exprt expr)
inlineprotected

Definition at line 243 of file smt2_conv.h.

References exprt::has_operands(), and irept::id().

Referenced by convert_floatbv().

§ type2id()

§ unflatten()

§ unflatten_array()

void smt2_convt::unflatten_array ( const exprt )
protected

§ use_array_theory()

bool smt2_convt::use_array_theory ( const exprt expr)
protected

§ write_footer()

void smt2_convt::write_footer ( std::ostream &  out)
protected

§ write_header()

void smt2_convt::write_header ( )
protected

Definition at line 71 of file smt2_conv.cpp.

References BOOLECTOR, CVC3, CVC4, emit_set_logic, GENERIC, logic, MATHSAT, notes, OPENSMT, out, solver, YICES, and Z3.

Referenced by smt2_convt().

Member Data Documentation

§ assumptions

bvt smt2_convt::assumptions
protected

Definition at line 129 of file smt2_conv.h.

Referenced by set_assumptions(), and write_footer().

§ benchmark

std::string smt2_convt::benchmark
protected

Definition at line 126 of file smt2_conv.h.

§ boolbv_width

§ boolean_assignment

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

Definition at line 303 of file smt2_conv.h.

Referenced by l_get(), print_assignment(), and smt2_dect::read_result().

§ bvfp_set

std::set<irep_idt> smt2_convt::bvfp_set
protected

Definition at line 228 of file smt2_conv.h.

Referenced by find_symbols().

§ datatype_map

§ defined_expressions

defined_expressionst smt2_convt::defined_expressions
protected

Definition at line 294 of file smt2_conv.h.

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

§ emit_set_logic

bool smt2_convt::emit_set_logic

Definition at line 107 of file smt2_conv.h.

Referenced by smt2_convt(), and write_header().

§ identifier_map

identifier_mapt smt2_convt::identifier_map
protected

Definition at line 280 of file smt2_conv.h.

Referenced by find_symbols(), get(), smt2_dect::read_result(), and set_to().

§ LET_COUNT

const unsigned smt2_convt::LET_COUNT =2
staticprotected

Definition at line 180 of file smt2_conv.h.

Referenced by letify_rec(), and smt2_convt::let_visitort::operator()().

§ let_id_count

unsigned smt2_convt::let_id_count
protected

Definition at line 179 of file smt2_conv.h.

Referenced by collect_bindings().

§ logic

std::string smt2_convt::logic
protected

Definition at line 126 of file smt2_conv.h.

Referenced by smt2_dect::decision_procedure_text(), and write_header().

§ no_boolean_variables

unsigned smt2_convt::no_boolean_variables
protected

Definition at line 302 of file smt2_conv.h.

Referenced by convert(), and smt2_dect::read_result().

§ notes

std::string smt2_convt::notes
protected

Definition at line 126 of file smt2_conv.h.

Referenced by write_header().

§ object_sizes

defined_expressionst smt2_convt::object_sizes
protected

Definition at line 296 of file smt2_conv.h.

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

§ out

§ pointer_logic

pointer_logict smt2_convt::pointer_logic
protected

§ smt2_identifiers

smt2_identifierst smt2_convt::smt2_identifiers
protected

Definition at line 299 of file smt2_conv.h.

Referenced by convert_literal(), find_symbols(), set_to(), and write_footer().

§ solver

solvert smt2_convt::solver
protected

§ use_array_of_bool

bool smt2_convt::use_array_of_bool

Definition at line 106 of file smt2_conv.h.

Referenced by convert_index(), convert_type(), and smt2_convt().

§ use_datatypes

§ use_FPA_theory


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