cprover
|
Decision procedure interface for various SMT 2.x solvers. More...
#include <smt2_dec.h>
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 |
![]() | |
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) |
![]() | |
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 |
![]() | |
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 (std::istream &in) |
![]() | |
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_symbolt & | to_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) |
![]() | |
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 |
![]() | |
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) |
Decision procedure interface for various SMT 2.x solvers.
Definition at line 35 of file smt2_dec.h.
|
inline |
Definition at line 38 of file smt2_dec.h.
|
virtual |
Reimplemented from smt2_convt.
Definition at line 66 of file smt2_dec.cpp.
References smt2_convt::BOOLECTOR, smt2_convt::CVC3, smt2_convt::CVC4, decision_proceduret::D_ERROR, messaget::eom(), messaget::error(), get_temporary_file(), smt2_convt::MATHSAT, smt2_convt::OPENSMT, read_result(), smt2_convt::solver, smt2_stringstreamt::stringstream, smt2_temp_filet::temp_out, smt2_temp_filet::temp_out_filename, smt2_temp_filet::temp_result_filename, smt2_convt::write_footer(), smt2_convt::YICES, and smt2_convt::Z3.
|
virtual |
Reimplemented from smt2_convt.
Definition at line 30 of file smt2_dec.cpp.
References smt2_convt::BOOLECTOR, smt2_convt::CVC3, smt2_convt::CVC4, smt2_convt::GENERIC, smt2_convt::logic, smt2_convt::MATHSAT, smt2_convt::OPENSMT, smt2_convt::solver, smt2_convt::use_FPA_theory, smt2_convt::YICES, and smt2_convt::Z3.
|
inlinevirtual |
Reimplemented from prop_convt.
Definition at line 52 of file smt2_dec.h.
|
protected |
Definition at line 172 of file smt2_dec.cpp.
References smt2_convt::boolean_assignment, smt2_convt::convert_identifier(), decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, messaget::eom(), messaget::error(), irept::get_sub(), irept::id(), smt2_convt::identifier_map, smt2_convt::no_boolean_variables, smt2_convt::parse_rec(), and smt2irep().
Referenced by dec_solve().