cprover
|
Decision procedure interface for various SMT 1.x solvers. More...
#include <smt1_dec.h>
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 |
![]() | |
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 |
![]() | |
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 |
![]() | |
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 | |
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) |
![]() | |
smt1_temp_filet () | |
~smt1_temp_filet () | |
![]() | |
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 |
![]() | |
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 |
![]() | |
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 Attributes | |
std::string | logic |
bool | dec_solve_was_called |
![]() | |
std::ofstream | temp_out |
std::string | temp_out_filename |
std::string | temp_result_filename |
![]() | |
std::string | benchmark |
std::string | source |
std::string | logic |
solvert | solver |
std::ostream & | out |
boolbv_widtht | boolbv_width |
std::set< irep_idt > | quantified_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 |
![]() | |
const namespacet & | ns |
Additional Inherited Members | |
![]() | |
enum | solvert { solvert::GENERIC, solvert::BOOLECTOR, solvert::CVC3, solvert::CVC4, solvert::MATHSAT, solvert::OPENSMT, solvert::YICES, solvert::Z3 } |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
![]() | |
typedef std::unordered_map< irep_idt, identifiert, irep_id_hash > | identifier_mapt |
typedef std::map< exprt, irep_idt > | array_of_mapt |
typedef std::map< exprt, irep_idt > | array_expr_mapt |
typedef std::map< exprt, exprt > | string2array_mapt |
enum | solvert { solvert::GENERIC, solvert::BOOLECTOR, solvert::CVC3, solvert::CVC4, solvert::MATHSAT, solvert::OPENSMT, solvert::YICES, solvert::Z3 } |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
Decision procedure interface for various SMT 1.x solvers.
Definition at line 30 of file smt1_dec.h.
|
inline |
Definition at line 33 of file smt1_dec.h.
|
virtual |
Reimplemented from smt1_convt.
Definition at line 63 of file smt1_dec.cpp.
References decision_proceduret::D_ERROR, dec_solve_was_called, messaget::eom(), messaget::error(), get_temporary_file(), read_result_boolector(), read_result_cvc3(), read_result_mathsat(), read_result_opensmt(), read_result_yices(), read_result_z3(), smt1_convt::solver, smt1_temp_filet::temp_out, smt1_temp_filet::temp_out_filename, smt1_temp_filet::temp_result_filename, and smt1_convt::write_footer().
|
virtual |
Reimplemented from smt1_convt.
Definition at line 29 of file smt1_dec.cpp.
References logic, and smt1_convt::solver.
|
protected |
Definition at line 290 of file smt1_dec.cpp.
References integer2binary(), pos(), safe_string2unsigned(), and string2integer().
Referenced by read_result_mathsat().
|
protected |
read model produced by Boolector
Definition at line 182 of file smt1_dec.cpp.
References smt1_convt::boolean_assignment, smt1_convt::convert_identifier(), decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, messaget::eom(), messaget::error(), smt1_convt::identifier_map, smt1_dect::valuet::index_value_map, smt1_convt::no_boolean_variables, pos(), smt1_convt::set_value(), and smt1_dect::valuet::value.
Referenced by dec_solve().
|
protected |
Definition at line 549 of file smt1_dec.cpp.
References smt1_convt::array_of_map, smt1_convt::boolean_assignment, smt1_convt::convert_identifier(), decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, smt1_convt::identifier_map, integer2binary(), integer2unsigned(), smt1_convt::no_boolean_variables, pos(), smt1_convt::set_value(), and string2integer().
Referenced by dec_solve().
|
protected |
Definition at line 307 of file smt1_dec.cpp.
References smt1_convt::boolean_assignment, smt1_convt::convert_identifier(), decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, has_prefix(), smt1_convt::identifier_map, mathsat_value(), smt1_convt::no_boolean_variables, and smt1_convt::set_value().
Referenced by dec_solve().
|
protected |
Definition at line 265 of file smt1_dec.cpp.
References decision_proceduret::D_ERROR.
Referenced by dec_solve().
|
protected |
Definition at line 270 of file smt1_dec.cpp.
References decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, messaget::eom(), and messaget::error().
Referenced by dec_solve().
|
protected |
Definition at line 377 of file smt1_dec.cpp.
References smt1_convt::boolean_assignment, smt1_convt::convert_identifier(), decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, smt1_convt::identifier_map, smt1_convt::no_boolean_variables, pos(), smt1_convt::set_value(), and string_to_expr_z3().
Referenced by dec_solve().
|
protected |
Definition at line 433 of file smt1_dec.cpp.
References smt1_convt::array_index_type(), smt1_convt::array_of_map, smt1_convt::binary2struct(), smt1_convt::binary2union(), irept::id(), integer2binary(), integer2unsigned(), messaget::result(), constant_exprt::set_value(), string2integer(), typet::subtype(), to_struct_type(), to_union_type(), exprt::type(), and array_of_exprt::what().
Referenced by read_result_z3().
|
protected |
Definition at line 51 of file smt1_dec.h.
Referenced by dec_solve().
|
protected |
Definition at line 50 of file smt1_dec.h.
Referenced by decision_procedure_text().