cprover
smt2_dect Class Reference

Decision procedure interface for various SMT 2.x solvers. More...

#include <smt2_dec.h>

+ Inheritance diagram for smt2_dect:
+ Collaboration diagram for smt2_dect:

Public Member Functions

 smt2_dect (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver)
 
virtual resultt dec_solve ()
 
virtual std::string decision_procedure_text () const
 
virtual bool has_set_assumptions () const
 
- Public Member Functions inherited from smt2_convt
 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 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 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 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...
 

Protected Member Functions

resultt read_result (std::istream &in)
 
- Protected Member Functions inherited from smt2_convt
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)
 
 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 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 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)
 
- Protected 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 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)
 
- Protected 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() ()
 
- Protected 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...
 

Additional Inherited Members

- Public Types inherited from smt2_convt
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
}
 
- 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...
 
- Public Attributes inherited from smt2_convt
bool use_FPA_theory
 
bool use_datatypes
 
bool use_array_of_bool
 
bool emit_set_logic
 
- 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...
 
- Protected Types inherited from smt2_convt
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
 
enum  solvert {
  solvert::GENERIC, solvert::BOOLECTOR, solvert::CPROVER_SMT2, solvert::CVC3,
  solvert::CVC4, solvert::MATHSAT, solvert::YICES, solvert::Z3
}
 
- Protected Types inherited from decision_proceduret
enum  resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR }
 
- Protected 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 Protected 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...
 
- Protected Attributes inherited from smt2_stringstreamt
std::stringstream stringstream
 
- Protected Attributes inherited from smt2_convt
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
 
bool use_FPA_theory
 
bool use_datatypes
 
bool use_array_of_bool
 
bool emit_set_logic
 
- Protected Attributes inherited from decision_proceduret
const namespacetns
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 
- Static Protected Attributes inherited from smt2_convt
static const std::size_t LET_COUNT = 2
 
- Static Protected 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

Decision procedure interface for various SMT 2.x solvers.

Definition at line 25 of file smt2_dec.h.

Constructor & Destructor Documentation

◆ smt2_dect()

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

Definition at line 28 of file smt2_dec.h.

Member Function Documentation

◆ dec_solve()

decision_proceduret::resultt smt2_dect::dec_solve ( )
virtual

Reimplemented from smt2_convt.

Definition at line 37 of file smt2_dec.cpp.

◆ decision_procedure_text()

std::string smt2_dect::decision_procedure_text ( ) const
virtual

Reimplemented from smt2_convt.

Definition at line 21 of file smt2_dec.cpp.

◆ has_set_assumptions()

virtual bool smt2_dect::has_set_assumptions ( ) const
inlinevirtual

Reimplemented from prop_convt.

Definition at line 42 of file smt2_dec.h.

◆ read_result()

decision_proceduret::resultt smt2_dect::read_result ( std::istream &  in)
protected

Definition at line 131 of file smt2_dec.cpp.


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