cprover
|
#include <smt2_conv.h>
Classes | |
struct | identifiert |
struct | let_count_idt |
class | let_visitort |
class | smt2_symbolt |
Public Types | |
enum | solvert { solvert::GENERIC, solvert::BOOLECTOR, solvert::CPROVER_SMT2, solvert::CVC3, solvert::CVC4, solvert::MATHSAT, solvert::YICES, solvert::Z3 } |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
Public Member Functions | |
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 resultt | dec_solve () |
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 std::string | decision_procedure_text () 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 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 |
virtual void | set_time_limit_seconds (uint32_t) |
![]() | |
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 Attributes | |
bool | use_FPA_theory |
bool | use_datatypes |
bool | use_array_of_bool |
bool | emit_set_logic |
Protected Types | |
enum | wheret { wheret::BEGIN, wheret::END } |
typedef irep_hash_mapt< exprt, let_count_idt > | seen_expressionst |
typedef std::unordered_map< irep_idt, identifiert > | identifier_mapt |
typedef std::map< typet, std::string > | datatype_mapt |
typedef std::map< exprt, irep_idt > | defined_expressionst |
typedef std::set< std::string > | smt2_identifierst |
Protected Member Functions | |
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_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) |
Protected Attributes | |
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_idt > | bvfp_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 |
![]() | |
const namespacet & | ns |
Static Protected Attributes | |
static const std::size_t | LET_COUNT = 2 |
Additional Inherited Members |
Definition at line 32 of file smt2_conv.h.
|
protected |
Definition at line 303 of file smt2_conv.h.
|
protected |
Definition at line 312 of file smt2_conv.h.
|
protected |
Definition at line 297 of file smt2_conv.h.
|
protected |
Definition at line 197 of file smt2_conv.h.
|
protected |
Definition at line 317 of file smt2_conv.h.
|
strong |
Enumerator | |
---|---|
GENERIC | |
BOOLECTOR | |
CPROVER_SMT2 | |
CVC3 | |
CVC4 | |
MATHSAT | |
YICES | |
Z3 |
Definition at line 35 of file smt2_conv.h.
|
strongprotected |
Enumerator | |
---|---|
BEGIN | |
END |
Definition at line 273 of file smt2_conv.h.
|
inline |
Definition at line 47 of file smt2_conv.h.
|
inlinevirtual |
Definition at line 107 of file smt2_conv.h.
|
protected |
Definition at line 4767 of file smt2_conv.cpp.
Implements prop_convt.
Definition at line 705 of file smt2_conv.cpp.
|
protected |
Definition at line 501 of file smt2_conv.cpp.
|
protected |
Definition at line 596 of file smt2_conv.cpp.
|
protected |
Definition at line 605 of file smt2_conv.cpp.
|
protected |
Definition at line 2700 of file smt2_conv.cpp.
|
protected |
Definition at line 3312 of file smt2_conv.cpp.
void smt2_convt::convert_expr | ( | const exprt & | expr | ) |
Definition at line 862 of file smt2_conv.cpp.
|
protected |
Definition at line 828 of file smt2_conv.cpp.
|
protected |
Definition at line 3356 of file smt2_conv.cpp.
|
protected |
Definition at line 3292 of file smt2_conv.cpp.
|
protected |
Definition at line 3451 of file smt2_conv.cpp.
|
protected |
Definition at line 3156 of file smt2_conv.cpp.
|
protected |
Definition at line 2425 of file smt2_conv.cpp.
|
protected |
Definition at line 757 of file smt2_conv.cpp.
|
protected |
Definition at line 3725 of file smt2_conv.cpp.
|
protected |
Definition at line 2851 of file smt2_conv.cpp.
void smt2_convt::convert_literal | ( | const literalt | l | ) |
Definition at line 737 of file smt2_conv.cpp.
|
protected |
Definition at line 3823 of file smt2_conv.cpp.
|
protected |
Definition at line 3195 of file smt2_conv.cpp.
|
protected |
Definition at line 2832 of file smt2_conv.cpp.
|
protected |
Definition at line 3376 of file smt2_conv.cpp.
|
protected |
Definition at line 4080 of file smt2_conv.cpp.
|
protected |
Definition at line 2977 of file smt2_conv.cpp.
|
protected |
Definition at line 2892 of file smt2_conv.cpp.
|
protected |
Converting a constant or symbolic rounding mode to SMT-LIB.
Only called when use_FPA_theory is enabled
Definition at line 3099 of file smt2_conv.cpp.
|
protected |
Definition at line 2571 of file smt2_conv.cpp.
void smt2_convt::convert_type | ( | const typet & | type | ) |
Definition at line 4389 of file smt2_conv.cpp.
|
protected |
Definition at line 1915 of file smt2_conv.cpp.
|
protected |
Definition at line 2665 of file smt2_conv.cpp.
|
protected |
Definition at line 3718 of file smt2_conv.cpp.
|
protected |
Definition at line 3471 of file smt2_conv.cpp.
|
virtual |
Implements decision_proceduret.
Reimplemented in smt2_dect.
Definition at line 171 of file smt2_conv.cpp.
|
inlinevirtual |
Implements decision_proceduret.
Reimplemented in smt2_dect.
Definition at line 120 of file smt2_conv.h.
Definition at line 133 of file smt2_conv.cpp.
|
protected |
Definition at line 4171 of file smt2_conv.cpp.
|
protected |
Definition at line 4532 of file smt2_conv.cpp.
Definition at line 4538 of file smt2_conv.cpp.
|
protected |
Definition at line 3884 of file smt2_conv.cpp.
|
protected |
produce a flat bit-vector for a given array of fixed size
Definition at line 2635 of file smt2_conv.cpp.
|
protected |
Definition at line 822 of file smt2_conv.cpp.
Implements decision_proceduret.
Definition at line 178 of file smt2_conv.cpp.
Implements prop_convt.
Definition at line 53 of file smt2_conv.cpp.
Definition at line 4735 of file smt2_conv.cpp.
|
protected |
Definition at line 4745 of file smt2_conv.cpp.
|
protected |
Definition at line 340 of file smt2_conv.cpp.
|
protected |
Definition at line 210 of file smt2_conv.cpp.
Definition at line 449 of file smt2_conv.cpp.
|
protected |
Definition at line 385 of file smt2_conv.cpp.
|
protected |
Definition at line 370 of file smt2_conv.cpp.
|
virtual |
Implements decision_proceduret.
Definition at line 43 of file smt2_conv.cpp.
|
inlinevirtual |
Reimplemented from prop_convt.
Definition at line 123 of file smt2_conv.h.
|
inlinevirtual |
Reimplemented from prop_convt.
Definition at line 117 of file smt2_conv.h.
|
virtual |
Implements decision_proceduret.
Definition at line 4085 of file smt2_conv.cpp.
|
protected |
Definition at line 4799 of file smt2_conv.cpp.
|
inlineprotected |
Definition at line 263 of file smt2_conv.h.
|
protected |
Definition at line 788 of file smt2_conv.cpp.
Definition at line 3973 of file smt2_conv.cpp.
|
protected |
|
protected |
Definition at line 4367 of file smt2_conv.cpp.
|
protected |
Definition at line 96 of file smt2_conv.cpp.
|
protected |
Definition at line 66 of file smt2_conv.cpp.
|
protected |
Definition at line 135 of file smt2_conv.h.
|
protected |
Definition at line 132 of file smt2_conv.h.
|
protected |
Definition at line 136 of file smt2_conv.h.
|
protected |
Definition at line 322 of file smt2_conv.h.
|
protected |
Definition at line 248 of file smt2_conv.h.
|
protected |
Definition at line 304 of file smt2_conv.h.
|
protected |
Definition at line 313 of file smt2_conv.h.
bool smt2_convt::emit_set_logic |
Definition at line 113 of file smt2_conv.h.
|
protected |
Definition at line 299 of file smt2_conv.h.
|
staticprotected |
Definition at line 201 of file smt2_conv.h.
|
protected |
Definition at line 200 of file smt2_conv.h.
|
protected |
Definition at line 132 of file smt2_conv.h.
|
protected |
Definition at line 321 of file smt2_conv.h.
|
protected |
Definition at line 132 of file smt2_conv.h.
|
protected |
Definition at line 315 of file smt2_conv.h.
|
protected |
Definition at line 131 of file smt2_conv.h.
|
protected |
Definition at line 278 of file smt2_conv.h.
|
protected |
Definition at line 318 of file smt2_conv.h.
|
protected |
Definition at line 133 of file smt2_conv.h.
bool smt2_convt::use_array_of_bool |
Definition at line 112 of file smt2_conv.h.
bool smt2_convt::use_datatypes |
Definition at line 111 of file smt2_conv.h.
bool smt2_convt::use_FPA_theory |
Definition at line 110 of file smt2_conv.h.