cprover
smt1_dect Class Reference

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

#include <smt1_dec.h>

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

Classes

struct  valuet
 

Public Member Functions

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

Protected Member Functions

resultt read_result_boolector (std::istream &in)
 read model produced by Boolector More...
 
resultt read_result_cvc3 (std::istream &in)
 
resultt read_result_opensmt (std::istream &in)
 
resultt read_result_mathsat (std::istream &in)
 
resultt read_result_yices (std::istream &in)
 
resultt read_result_z3 (std::istream &in)
 
bool string_to_expr_z3 (const typet &type, const std::string &value, exprt &e) const
 
std::string mathsat_value (const std::string &src)
 
- Protected Member Functions inherited from smt1_temp_filet
 smt1_temp_filet ()
 
 ~smt1_temp_filet ()
 
- Protected Member Functions inherited from smt1_convt
void write_header ()
 
void write_footer ()
 
void convert_expr (const exprt &expr, bool bool_as_bv)
 
void convert_type (const typet &type)
 
void convert_byte_update (const exprt &expr, bool bool_as_bv)
 
void convert_byte_extract (const byte_extract_exprt &expr, bool bool_as_bv)
 
void convert_typecast (const typecast_exprt &expr, bool bool_as_bv)
 
void convert_struct (const exprt &expr)
 
void convert_union (const exprt &expr)
 
void convert_constant (const constant_exprt &expr, bool bool_as_bv)
 
void convert_relation (const exprt &expr, bool bool_as_bv)
 
void convert_is_dynamic_object (const exprt &expr, bool bool_as_bv)
 
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_floatbv_plus (const exprt &expr)
 
void convert_floatbv_minus (const exprt &expr)
 
void convert_floatbv_div (const exprt &expr)
 
void convert_floatbv_mult (const exprt &expr)
 
void convert_mod (const mod_exprt &expr)
 
void convert_index (const index_exprt &expr, bool bool_as_bv)
 
void convert_member (const member_exprt &expr, bool bool_as_bv)
 
void convert_overflow (const exprt &expr)
 
void convert_with (const exprt &expr)
 
void convert_update (const exprt &expr)
 
std::string convert_identifier (const irep_idt &identifier)
 
void convert_literal (const literalt l)
 
void find_symbols (const exprt &expr)
 
void find_symbols (const typet &type)
 
void find_symbols_rec (const typet &type, std::set< irep_idt > &recstack)
 
void flatten_array (const exprt &op)
 
void from_bv_begin (const typet &type, bool bool_as_bv)
 
void from_bv_end (const typet &type, bool bool_as_bv)
 
void from_bool_begin (const typet &type, bool bool_as_bv)
 
void from_bool_end (const typet &type, bool bool_as_bv)
 
typet array_index_type () const
 
void array_index (const exprt &expr)
 
void convert_address_of_rec (const exprt &expr, const pointer_typet &result_type)
 
void set_value (identifiert &identifier, const std::string &index, const std::string &value)
 
exprt ce_value (const typet &type, const std::string &index, const std::string &v, bool in_struct) const
 
exprt binary2struct (const struct_typet &type, const std::string &binary) const
 
exprt binary2union (const union_typet &type, const std::string &binary) const
 
void convert_nary (const exprt &expr, const irep_idt op_string, bool bool_as_bv)
 
 smt1_convt (const namespacet &_ns, const std::string &_benchmark, const std::string &_source, const std::string &_logic, solvert _solver, std::ostream &_out)
 
virtual ~smt1_convt ()
 
virtual literalt convert (const exprt &expr)
 
virtual void set_to (const exprt &expr, bool value)
 
virtual exprt get (const exprt &expr) const
 
virtual tvt l_get (literalt) const
 
virtual void print_assignment (std::ostream &out) const
 
- Protected Member Functions inherited from prop_convt
 prop_convt (const namespacet &_ns)
 
virtual ~prop_convt ()
 
literalt operator() (const exprt &expr)
 
virtual void set_frozen (literalt a)
 
virtual void set_frozen (const bvt &)
 
virtual void set_assumptions (const bvt &_assumptions)
 
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
 
- 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 ()
 

Protected Attributes

std::string logic
 
bool dec_solve_was_called
 
- Protected Attributes inherited from smt1_temp_filet
std::ofstream temp_out
 
std::string temp_out_filename
 
std::string temp_result_filename
 
- Protected Attributes inherited from smt1_convt
std::string benchmark
 
std::string source
 
std::string logic
 
solvert solver
 
std::ostream & out
 
boolbv_widtht boolbv_width
 
std::set< irep_idtquantified_symbols
 
pointer_logict pointer_logic
 
identifier_mapt identifier_map
 
unsigned array_index_bits
 
array_of_mapt array_of_map
 
array_expr_mapt array_expr_map
 
string2array_mapt string2array_map
 
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
 

Additional Inherited Members

- Public Types inherited from smt1_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)
 
- Protected Types inherited from smt1_convt
typedef std::unordered_map< irep_idt, identifiert, irep_id_hashidentifier_mapt
 
typedef std::map< exprt, irep_idtarray_of_mapt
 
typedef std::map< exprt, irep_idtarray_expr_mapt
 
typedef std::map< exprt, exprtstring2array_mapt
 
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)
 

Detailed Description

Decision procedure interface for various SMT 1.x solvers.

Definition at line 30 of file smt1_dec.h.

Constructor & Destructor Documentation

◆ smt1_dect()

smt1_dect::smt1_dect ( const namespacet _ns,
const std::string &  _benchmark,
const std::string &  _source,
const std::string &  _logic,
solvert  _solver 
)
inline

Definition at line 33 of file smt1_dec.h.

Member Function Documentation

◆ dec_solve()

◆ decision_procedure_text()

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

Reimplemented from smt1_convt.

Definition at line 29 of file smt1_dec.cpp.

References logic, and smt1_convt::solver.

◆ mathsat_value()

std::string smt1_dect::mathsat_value ( const std::string &  src)
protected

Definition at line 290 of file smt1_dec.cpp.

References integer2binary(), pos(), safe_string2unsigned(), and string2integer().

Referenced by read_result_mathsat().

◆ read_result_boolector()

◆ read_result_cvc3()

◆ read_result_mathsat()

◆ read_result_opensmt()

decision_proceduret::resultt smt1_dect::read_result_opensmt ( std::istream &  in)
protected

Definition at line 265 of file smt1_dec.cpp.

References decision_proceduret::D_ERROR.

Referenced by dec_solve().

◆ read_result_yices()

decision_proceduret::resultt smt1_dect::read_result_yices ( std::istream &  in)
protected

◆ read_result_z3()

◆ string_to_expr_z3()

Member Data Documentation

◆ dec_solve_was_called

bool smt1_dect::dec_solve_was_called
protected

Definition at line 51 of file smt1_dec.h.

Referenced by dec_solve().

◆ logic

std::string smt1_dect::logic
protected

Definition at line 50 of file smt1_dec.h.

Referenced by decision_procedure_text().


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