|
| 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) |
|
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 |
|
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() () |
|
virtual void | set_message_handler (message_handlert &_message_handler) |
|
message_handlert & | get_message_handler () |
|
| messaget () |
|
| messaget (const messaget &other) |
|
messaget & | operator= (const messaget &other) |
|
| messaget (message_handlert &_message_handler) |
|
virtual | ~messaget () |
|
mstreamt & | get_mstream (unsigned message_level) const |
|
mstreamt & | error () const |
|
mstreamt & | warning () const |
|
mstreamt & | result () const |
|
mstreamt & | status () const |
|
mstreamt & | statistics () const |
|
mstreamt & | progress () const |
|
mstreamt & | debug () const |
|
void | conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const |
| Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream . More...
|
|
|
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, 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) |
|
| 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) |
|
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 |
|
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() () |
|
virtual void | set_message_handler (message_handlert &_message_handler) |
|
message_handlert & | get_message_handler () |
|
| messaget () |
|
| messaget (const messaget &other) |
|
messaget & | operator= (const messaget &other) |
|
| messaget (message_handlert &_message_handler) |
|
virtual | ~messaget () |
|
mstreamt & | get_mstream (unsigned message_level) const |
|
mstreamt & | error () const |
|
mstreamt & | warning () const |
|
mstreamt & | result () const |
|
mstreamt & | status () const |
|
mstreamt & | statistics () const |
|
mstreamt & | progress () const |
|
mstreamt & | debug () const |
|
void | conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const |
| Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream . More...
|
|
|
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
} |
|
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 unsigned | eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest) |
| Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
|
|
static commandt | command (unsigned c) |
| Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
|
|
bool | use_FPA_theory |
|
bool | use_datatypes |
|
bool | use_array_of_bool |
|
bool | emit_set_logic |
|
static eomt | eom |
|
static const commandt | reset |
| return to default formatting, as defined by the terminal More...
|
|
static const commandt | red |
| render text with red foreground color More...
|
|
static const commandt | green |
| render text with green foreground color More...
|
|
static const commandt | yellow |
| render text with yellow foreground color More...
|
|
static const commandt | blue |
| render text with blue foreground color More...
|
|
static const commandt | magenta |
| render text with magenta foreground color More...
|
|
static const commandt | cyan |
| render text with cyan foreground color More...
|
|
static const commandt | bright_red |
| render text with bright red foreground color More...
|
|
static const commandt | bright_green |
| render text with bright green foreground color More...
|
|
static const commandt | bright_yellow |
| render text with bright yellow foreground color More...
|
|
static const commandt | bright_blue |
| render text with bright blue foreground color More...
|
|
static const commandt | bright_magenta |
| render text with bright magenta foreground color More...
|
|
static const commandt | bright_cyan |
| render text with bright cyan foreground color More...
|
|
static const commandt | bold |
| render text with bold font More...
|
|
static const commandt | faint |
| render text with faint font More...
|
|
static const commandt | italic |
| render italic text More...
|
|
static const commandt | underline |
| render underlined text More...
|
|
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 |
|
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
} |
|
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 unsigned | eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest) |
| Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
|
|
static commandt | command (unsigned c) |
| Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
|
|
std::stringstream | stringstream |
|
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 |
|
bool | use_FPA_theory |
|
bool | use_datatypes |
|
bool | use_array_of_bool |
|
bool | emit_set_logic |
|
const namespacet & | ns |
|
message_handlert * | message_handler |
|
mstreamt | mstream |
|
static const std::size_t | LET_COUNT = 2 |
|
static eomt | eom |
|
static const commandt | reset |
| return to default formatting, as defined by the terminal More...
|
|
static const commandt | red |
| render text with red foreground color More...
|
|
static const commandt | green |
| render text with green foreground color More...
|
|
static const commandt | yellow |
| render text with yellow foreground color More...
|
|
static const commandt | blue |
| render text with blue foreground color More...
|
|
static const commandt | magenta |
| render text with magenta foreground color More...
|
|
static const commandt | cyan |
| render text with cyan foreground color More...
|
|
static const commandt | bright_red |
| render text with bright red foreground color More...
|
|
static const commandt | bright_green |
| render text with bright green foreground color More...
|
|
static const commandt | bright_yellow |
| render text with bright yellow foreground color More...
|
|
static const commandt | bright_blue |
| render text with bright blue foreground color More...
|
|
static const commandt | bright_magenta |
| render text with bright magenta foreground color More...
|
|
static const commandt | bright_cyan |
| render text with bright cyan foreground color More...
|
|
static const commandt | bold |
| render text with bold font More...
|
|
static const commandt | faint |
| render text with faint font More...
|
|
static const commandt | italic |
| render italic text More...
|
|
static const commandt | underline |
| render underlined text More...
|
|
Decision procedure interface for various SMT 2.x solvers.
Definition at line 25 of file smt2_dec.h.