cprover
smt2_dect Class Reference

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

#include <smt2_dec.h>

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

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 a)
 
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
 
- 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 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, 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)
 
 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 a)
 
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
 
- Protected 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)
 
- Protected 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 ()
 

Additional Inherited Members

- Public Types inherited from smt2_convt
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
}
 
- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Public Attributes inherited from smt2_convt
bool use_FPA_theory
 
bool use_datatypes
 
bool use_array_of_bool
 
bool emit_set_logic
 
- Protected Types inherited from smt2_convt
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
 
enum  solvert {
  solvert::GENERIC, solvert::BOOLECTOR, solvert::CVC3, solvert::CVC4,
  solvert::MATHSAT, solvert::OPENSMT, 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 mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- 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
 
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
 
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 unsigned LET_COUNT =2
 

Detailed Description

Decision procedure interface for various SMT 2.x solvers.

Definition at line 35 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 38 of file smt2_dec.h.

Member Function Documentation

◆ dec_solve()

◆ decision_procedure_text()

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

◆ has_set_assumptions()

virtual bool smt2_dect::has_set_assumptions ( ) const
inlinevirtual

Reimplemented from prop_convt.

Definition at line 52 of file smt2_dec.h.

◆ read_result()


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