cprover
smt2_convt Class Reference

#include <smt2_conv.h>

+ Inheritance diagram for smt2_convt:
+ Collaboration diagram for smt2_convt:

Classes

struct  identifiert
 
struct  let_count_idt
 
class  let_visitort
 
class  smt2_symbolt
 

Public Types

enum  solvert {
  solvert::GENERIC, solvert::BOOLECTOR, solvert::CPROVER_SMT2, 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 message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. 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 commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 

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 303 of file smt2_conv.h.

◆ defined_expressionst

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

Definition at line 312 of file smt2_conv.h.

◆ identifier_mapt

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

Definition at line 297 of file smt2_conv.h.

◆ seen_expressionst

Definition at line 197 of file smt2_conv.h.

◆ smt2_identifierst

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

Definition at line 317 of file smt2_conv.h.

Member Enumeration Documentation

◆ solvert

enum smt2_convt::solvert
strong
Enumerator
GENERIC 
BOOLECTOR 
CPROVER_SMT2 
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 273 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

Definition at line 47 of file smt2_conv.h.

◆ ~smt2_convt()

virtual smt2_convt::~smt2_convt ( )
inlinevirtual

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

Definition at line 4767 of file smt2_conv.cpp.

◆ convert()

literalt smt2_convt::convert ( const exprt expr)
virtual

Implements prop_convt.

Definition at line 705 of file smt2_conv.cpp.

◆ convert_address_of_rec()

void smt2_convt::convert_address_of_rec ( const exprt expr,
const pointer_typet result_type 
)
protected

Definition at line 501 of file smt2_conv.cpp.

◆ convert_byte_extract()

void smt2_convt::convert_byte_extract ( const byte_extract_exprt expr)
protected

Definition at line 596 of file smt2_conv.cpp.

◆ convert_byte_update()

void smt2_convt::convert_byte_update ( const byte_update_exprt expr)
protected

Definition at line 605 of file smt2_conv.cpp.

◆ convert_constant()

void smt2_convt::convert_constant ( const constant_exprt expr)
protected

Definition at line 2700 of file smt2_conv.cpp.

◆ convert_div()

void smt2_convt::convert_div ( const div_exprt expr)
protected

Definition at line 3312 of file smt2_conv.cpp.

◆ convert_expr()

void smt2_convt::convert_expr ( const exprt expr)

Definition at line 862 of file smt2_conv.cpp.

◆ convert_floatbv()

void smt2_convt::convert_floatbv ( const exprt expr)
protected

Definition at line 828 of file smt2_conv.cpp.

◆ convert_floatbv_div()

void smt2_convt::convert_floatbv_div ( const ieee_float_op_exprt expr)
protected

Definition at line 3356 of file smt2_conv.cpp.

◆ convert_floatbv_minus()

void smt2_convt::convert_floatbv_minus ( const ieee_float_op_exprt expr)
protected

Definition at line 3292 of file smt2_conv.cpp.

◆ convert_floatbv_mult()

void smt2_convt::convert_floatbv_mult ( const ieee_float_op_exprt expr)
protected

Definition at line 3451 of file smt2_conv.cpp.

◆ convert_floatbv_plus()

void smt2_convt::convert_floatbv_plus ( const ieee_float_op_exprt expr)
protected

Definition at line 3156 of file smt2_conv.cpp.

◆ convert_floatbv_typecast()

void smt2_convt::convert_floatbv_typecast ( const floatbv_typecast_exprt expr)
protected

Definition at line 2425 of file smt2_conv.cpp.

◆ convert_identifier()

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

Definition at line 757 of file smt2_conv.cpp.

◆ convert_index()

void smt2_convt::convert_index ( const index_exprt expr)
protected

Definition at line 3725 of file smt2_conv.cpp.

◆ convert_is_dynamic_object()

void smt2_convt::convert_is_dynamic_object ( const exprt expr)
protected

Definition at line 2851 of file smt2_conv.cpp.

◆ convert_literal()

void smt2_convt::convert_literal ( const literalt  l)

Definition at line 737 of file smt2_conv.cpp.

◆ convert_member()

void smt2_convt::convert_member ( const member_exprt expr)
protected

Definition at line 3823 of file smt2_conv.cpp.

◆ convert_minus()

void smt2_convt::convert_minus ( const minus_exprt expr)
protected

Definition at line 3195 of file smt2_conv.cpp.

◆ convert_mod()

void smt2_convt::convert_mod ( const mod_exprt expr)
protected

Definition at line 2832 of file smt2_conv.cpp.

◆ convert_mult()

void smt2_convt::convert_mult ( const mult_exprt expr)
protected

Definition at line 3376 of file smt2_conv.cpp.

◆ convert_operands()

exprt smt2_convt::convert_operands ( const exprt )
protected

◆ convert_overflow()

void smt2_convt::convert_overflow ( const exprt expr)
protected

Definition at line 4080 of file smt2_conv.cpp.

◆ convert_plus()

void smt2_convt::convert_plus ( const plus_exprt expr)
protected

Definition at line 2977 of file smt2_conv.cpp.

◆ convert_relation()

void smt2_convt::convert_relation ( const exprt expr)
protected

Definition at line 2892 of file smt2_conv.cpp.

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

◆ convert_struct()

void smt2_convt::convert_struct ( const struct_exprt expr)
protected

Definition at line 2571 of file smt2_conv.cpp.

◆ convert_type()

void smt2_convt::convert_type ( const typet type)

Definition at line 4389 of file smt2_conv.cpp.

◆ convert_typecast()

void smt2_convt::convert_typecast ( const typecast_exprt expr)
protected

Definition at line 1915 of file smt2_conv.cpp.

◆ convert_union()

void smt2_convt::convert_union ( const union_exprt expr)
protected

Definition at line 2665 of file smt2_conv.cpp.

◆ convert_update()

void smt2_convt::convert_update ( const exprt expr)
protected

Definition at line 3718 of file smt2_conv.cpp.

◆ convert_with()

void smt2_convt::convert_with ( const with_exprt expr)
protected

Definition at line 3471 of file smt2_conv.cpp.

◆ dec_solve()

decision_proceduret::resultt smt2_convt::dec_solve ( )
virtual

Implements decision_proceduret.

Reimplemented in smt2_dect.

Definition at line 171 of file smt2_conv.cpp.

◆ decision_procedure_text()

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

Implements decision_proceduret.

Reimplemented in smt2_dect.

Definition at line 120 of file smt2_conv.h.

◆ define_object_size()

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

Definition at line 133 of file smt2_conv.cpp.

◆ find_symbols() [1/2]

void smt2_convt::find_symbols ( const exprt expr)
protected

Definition at line 4171 of file smt2_conv.cpp.

◆ find_symbols() [2/2]

void smt2_convt::find_symbols ( const typet type)
protected

Definition at line 4532 of file smt2_conv.cpp.

◆ find_symbols_rec()

void smt2_convt::find_symbols_rec ( const typet type,
std::set< irep_idt > &  recstack 
)
protected

Definition at line 4538 of file smt2_conv.cpp.

◆ flatten2bv()

void smt2_convt::flatten2bv ( const exprt expr)
protected

Definition at line 3884 of file smt2_conv.cpp.

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

◆ floatbv_suffix()

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

Definition at line 822 of file smt2_conv.cpp.

◆ get()

exprt smt2_convt::get ( const exprt expr) const
virtual

Implements decision_proceduret.

Definition at line 178 of file smt2_conv.cpp.

◆ l_get()

tvt smt2_convt::l_get ( literalt  l) const
virtual

Implements prop_convt.

Definition at line 53 of file smt2_conv.cpp.

◆ letify()

exprt smt2_convt::letify ( exprt expr)
protected

Definition at line 4735 of file smt2_conv.cpp.

◆ letify_rec()

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

Definition at line 4745 of file smt2_conv.cpp.

◆ parse_array()

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

Definition at line 340 of file smt2_conv.cpp.

◆ parse_literal()

constant_exprt smt2_convt::parse_literal ( const irept src,
const typet type 
)
protected

Definition at line 210 of file smt2_conv.cpp.

◆ parse_rec()

exprt smt2_convt::parse_rec ( const irept s,
const typet type 
)
protected

Definition at line 449 of file smt2_conv.cpp.

◆ parse_struct()

exprt smt2_convt::parse_struct ( const irept s,
const struct_typet type 
)
protected

Definition at line 385 of file smt2_conv.cpp.

◆ parse_union()

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

Definition at line 370 of file smt2_conv.cpp.

◆ print_assignment()

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

Implements decision_proceduret.

Definition at line 43 of file smt2_conv.cpp.

◆ set_assumptions()

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

Reimplemented from prop_convt.

Definition at line 123 of file smt2_conv.h.

◆ set_frozen()

virtual void smt2_convt::set_frozen ( literalt  )
inlinevirtual

Reimplemented from prop_convt.

Definition at line 117 of file smt2_conv.h.

◆ set_to()

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

Implements decision_proceduret.

Definition at line 4085 of file smt2_conv.cpp.

◆ substitute_let()

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

Definition at line 4799 of file smt2_conv.cpp.

◆ to_smt2_symbol()

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

Definition at line 263 of file smt2_conv.h.

◆ type2id()

std::string smt2_convt::type2id ( const typet type) const
protected

Definition at line 788 of file smt2_conv.cpp.

◆ unflatten()

void smt2_convt::unflatten ( wheret  where,
const typet type,
unsigned  nesting = 0 
)
protected

Definition at line 3973 of file smt2_conv.cpp.

◆ unflatten_array()

void smt2_convt::unflatten_array ( const exprt )
protected

◆ use_array_theory()

bool smt2_convt::use_array_theory ( const exprt expr)
protected

Definition at line 4367 of file smt2_conv.cpp.

◆ write_footer()

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

Definition at line 96 of file smt2_conv.cpp.

◆ write_header()

void smt2_convt::write_header ( )
protected

Definition at line 66 of file smt2_conv.cpp.

Member Data Documentation

◆ assumptions

bvt smt2_convt::assumptions
protected

Definition at line 135 of file smt2_conv.h.

◆ benchmark

std::string smt2_convt::benchmark
protected

Definition at line 132 of file smt2_conv.h.

◆ boolbv_width

boolbv_widtht smt2_convt::boolbv_width
protected

Definition at line 136 of file smt2_conv.h.

◆ boolean_assignment

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

Definition at line 322 of file smt2_conv.h.

◆ bvfp_set

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

Definition at line 248 of file smt2_conv.h.

◆ datatype_map

datatype_mapt smt2_convt::datatype_map
protected

Definition at line 304 of file smt2_conv.h.

◆ defined_expressions

defined_expressionst smt2_convt::defined_expressions
protected

Definition at line 313 of file smt2_conv.h.

◆ emit_set_logic

bool smt2_convt::emit_set_logic

Definition at line 113 of file smt2_conv.h.

◆ identifier_map

identifier_mapt smt2_convt::identifier_map
protected

Definition at line 299 of file smt2_conv.h.

◆ LET_COUNT

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

Definition at line 201 of file smt2_conv.h.

◆ let_id_count

std::size_t smt2_convt::let_id_count
protected

Definition at line 200 of file smt2_conv.h.

◆ logic

std::string smt2_convt::logic
protected

Definition at line 132 of file smt2_conv.h.

◆ no_boolean_variables

std::size_t smt2_convt::no_boolean_variables
protected

Definition at line 321 of file smt2_conv.h.

◆ notes

std::string smt2_convt::notes
protected

Definition at line 132 of file smt2_conv.h.

◆ object_sizes

defined_expressionst smt2_convt::object_sizes
protected

Definition at line 315 of file smt2_conv.h.

◆ out

std::ostream& smt2_convt::out
protected

Definition at line 131 of file smt2_conv.h.

◆ pointer_logic

pointer_logict smt2_convt::pointer_logic
protected

Definition at line 278 of file smt2_conv.h.

◆ smt2_identifiers

smt2_identifierst smt2_convt::smt2_identifiers
protected

Definition at line 318 of file smt2_conv.h.

◆ solver

solvert smt2_convt::solver
protected

Definition at line 133 of file smt2_conv.h.

◆ use_array_of_bool

bool smt2_convt::use_array_of_bool

Definition at line 112 of file smt2_conv.h.

◆ use_datatypes

bool smt2_convt::use_datatypes

Definition at line 111 of file smt2_conv.h.

◆ use_FPA_theory

bool smt2_convt::use_FPA_theory

Definition at line 110 of file smt2_conv.h.


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