cprover
smt2_convt Class Reference

#include <smt2_conv.h>

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

Classes

struct  identifiert
 
struct  let_count_idt
 
class  let_visitort
 
class  smt2_symbolt
 

Public Types

enum  solvert {
  solvert::GENERIC, solvert::BOOLECTOR, solvert::CVC3, solvert::CVC4,
  solvert::MATHSAT, 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)
 
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
 
virtual void set_time_limit_seconds (uint32_t)
 
- Public Member Functions inherited from decision_proceduret
 decision_proceduret (const namespacet &_ns)
 
virtual ~decision_proceduret ()
 
void set_to_true (const exprt &expr)
 
void set_to_false (const exprt &expr)
 
resultt operator() ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

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 irep_hash_mapt< exprt, let_count_idtseen_expressionst
 
typedef std::unordered_map< irep_idt, identifiertidentifier_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, std::size_t 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
 
std::size_t 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
 
std::size_t 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 std::size_t LET_COUNT = 2
 

Additional Inherited Members

- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 32 of file smt2_conv.h.

Member Typedef Documentation

◆ datatype_mapt

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

Definition at line 297 of file smt2_conv.h.

◆ defined_expressionst

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

Definition at line 306 of file smt2_conv.h.

◆ identifier_mapt

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

Definition at line 291 of file smt2_conv.h.

◆ seen_expressionst

Definition at line 191 of file smt2_conv.h.

◆ smt2_identifierst

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

Definition at line 311 of file smt2_conv.h.

Member Enumeration Documentation

◆ solvert

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

Definition at line 35 of file smt2_conv.h.

◆ wheret

enum smt2_convt::wheret
strongprotected
Enumerator
BEGIN 
END 

Definition at line 267 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.

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 866 of file smt2_conv.cpp.

References base_type_eq(), boolbv_width, configt::bv_encoding, config, 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(), DATA_INVARIANT, datatype_map, defined_expressions, flatten2bv(), forall_operands, from_integer(), irept::get(), symbol_exprt::get_identifier(), nondet_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(), lower_popcount(), MATHSAT, decision_proceduret::ns, configt::bv_encodingt::object_bits, object_sizes, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), out, pointer_logic, power(), vector_typet::size(), SMT2_TODO, solver, let_exprt::symbol(), to_bitvector_type(), 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_nondet_symbol_expr(), to_plus_expr(), to_pointer_type(), to_popcount_expr(), 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(), 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 4072 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 3065 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 3687 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().

◆ 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.

◆ define_object_size()

◆ find_symbols() [1/2]

◆ find_symbols() [2/2]

void smt2_convt::find_symbols ( const typet type)
protected

Definition at line 4531 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 2579 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

Definition at line 827 of file smt2_conv.cpp.

References exprt::op0(), exprt::operands(), exprt::type(), and type2id().

Referenced by convert_floatbv(), and find_symbols().

◆ get()

◆ l_get()

tvt smt2_convt::l_get ( literalt  l) const
virtual

◆ letify()

exprt smt2_convt::letify ( exprt expr)
protected

Definition at line 4733 of file smt2_conv.cpp.

References collect_bindings(), and letify_rec().

Referenced by find_symbols().

◆ letify_rec()

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

◆ parse_array()

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

Definition at line 339 of file smt2_conv.cpp.

References irept::get_sub(), parse_rec(), array_typet::size(), typet::subtype(), and exprt::type().

Referenced by parse_rec().

◆ 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, and out.

◆ 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.

◆ set_frozen()

virtual void smt2_convt::set_frozen ( literalt  )
inlinevirtual

Reimplemented from prop_convt.

Definition at line 111 of file smt2_conv.h.

◆ set_to()

◆ substitute_let()

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

Definition at line 4798 of file smt2_conv.cpp.

References Forall_operands, and exprt::operands().

Referenced by letify_rec().

◆ to_smt2_symbol()

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

Definition at line 257 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, 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 316 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 242 of file smt2_conv.h.

Referenced by find_symbols().

◆ datatype_map

◆ defined_expressions

defined_expressionst smt2_convt::defined_expressions
protected

Definition at line 307 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 293 of file smt2_conv.h.

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

◆ LET_COUNT

const std::size_t smt2_convt::LET_COUNT = 2
staticprotected

Definition at line 195 of file smt2_conv.h.

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

◆ let_id_count

std::size_t smt2_convt::let_id_count
protected

Definition at line 194 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

std::size_t smt2_convt::no_boolean_variables
protected

Definition at line 315 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 309 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 312 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: