cprover
|
#include <cvc_conv.h>
Classes | |
struct | identifiert |
Public Member Functions | |
cvc_convt (const namespacet &_ns, std::ostream &_out) | |
virtual | ~cvc_convt () |
virtual void | set_to (const exprt &expr, bool value) |
virtual literalt | convert (const exprt &expr) |
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) | |
virtual exprt | get (const exprt &expr) const =0 |
void | set_to_true (const exprt &expr) |
void | set_to_false (const exprt &expr) |
virtual resultt | dec_solve ()=0 |
resultt | operator() () |
virtual bool | in_core (const exprt &expr) |
virtual std::string | decision_procedure_text () const =0 |
Protected Types | |
typedef std::unordered_map< irep_idt, identifiert, irep_id_hash > | identifier_mapt |
Protected Member Functions | |
virtual void | convert_expr (const exprt &expr) |
virtual void | convert_type (const typet &type) |
virtual void | convert_address_of_rec (const exprt &expr) |
Protected Attributes | |
std::ostream & | out |
pointer_logict | pointer_logic |
unsigned | no_boolean_variables |
identifier_mapt | identifier_map |
std::vector< bool > | boolean_assignment |
![]() | |
const namespacet & | ns |
Private Member Functions | |
void | convert_identifier (const std::string &identifier) |
void | convert_typecast_expr (const exprt &expr) |
void | convert_binary_expr (const exprt &expr, const exprt &op) |
void | convert_struct_expr (const exprt &expr) |
void | convert_constant_expr (const exprt &expr) |
void | convert_equality_expr (const exprt &expr) |
void | convert_comparison_expr (const exprt &expr) |
void | convert_plus_expr (const exprt &expr) |
void | convert_minus_expr (const exprt &expr) |
void | convert_with_expr (const exprt &expr) |
void | convert_literal (const literalt l) |
void | find_symbols (const exprt &expr) |
void | find_symbols (const typet &type) |
void | convert_array_value (const exprt &expr) |
void | convert_as_bv (const exprt &expr) |
void | convert_array_index (const exprt &expr) |
Static Private Member Functions | |
static typet | gen_array_index_type () |
static std::string | bin_zero (unsigned bits) |
static std::string | array_index_type () |
static std::string | array_index (unsigned i) |
static std::string | cvc_pointer_type () |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
Definition at line 17 of file cvc_conv.h.
|
protected |
Definition at line 59 of file cvc_conv.h.
|
inline |
Definition at line 20 of file cvc_conv.h.
|
inlinevirtual |
Definition at line 28 of file cvc_conv.h.
References convert(), l_get(), out, print_assignment(), and set_to().
|
staticprivate |
Definition at line 522 of file cvc_conv.cpp.
References configt::ansi_c, config, configt::ansi_ct::int_width, and integer2binary().
Referenced by convert_constant_expr().
|
staticprivate |
Definition at line 509 of file cvc_conv.cpp.
Referenced by convert_constant_expr(), convert_expr(), and convert_type().
|
staticprivate |
Definition at line 490 of file cvc_conv.cpp.
References messaget::result().
Referenced by convert_address_of_rec(), and convert_constant_expr().
Implements prop_convt.
Definition at line 627 of file cvc_conv.cpp.
References const_literal(), convert_expr(), convert_literal(), find_symbols(), literal_exprt::get_literal(), irept::id(), exprt::is_false(), exprt::is_true(), no_boolean_variables, out, irept::pretty(), to_literal_expr(), and exprt::type().
Referenced by ~cvc_convt().
|
protectedvirtual |
Definition at line 541 of file cvc_conv.cpp.
References pointer_logict::add_object(), configt::ansi_c, bin_zero(), config, convert_expr(), cvc_pointer_type(), from_integer(), member_exprt::get_component_name(), irept::id(), irept::id_string(), index_type(), exprt::is_zero(), member_offset(), decision_proceduret::ns, exprt::op0(), exprt::op1(), exprt::operands(), out, pointer_logic, configt::ansi_ct::pointer_width, irept::set(), to_member_expr(), to_struct_type(), and exprt::type().
Referenced by convert_expr().
|
private |
Definition at line 527 of file cvc_conv.cpp.
References convert_expr(), exprt::copy_to_operands(), gen_array_index_type(), and exprt::type().
Referenced by convert_expr(), and convert_with_expr().
|
private |
Definition at line 719 of file cvc_conv.cpp.
References convert_as_bv().
Referenced by convert_constant_expr(), convert_expr(), and convert_with_expr().
|
private |
Definition at line 700 of file cvc_conv.cpp.
References convert_expr(), irept::id(), exprt::is_false(), exprt::is_true(), out, and exprt::type().
Referenced by convert_array_value(), and convert_expr().
Definition at line 45 of file cvc_conv.cpp.
References convert_expr(), irept::get(), irept::id(), id2string(), irept::id_string(), out, exprt::type(), and unsafe_string2unsigned().
Referenced by convert_typecast_expr().
|
private |
Definition at line 360 of file cvc_conv.cpp.
References convert_expr(), irept::id(), irept::id_string(), exprt::op0(), exprt::op1(), exprt::operands(), out, and exprt::type().
Referenced by convert_expr().
|
private |
Definition at line 126 of file cvc_conv.cpp.
References configt::ansi_c, array_index(), array_index_type(), bin_zero(), binary2integer(), config, convert_array_value(), convert_expr(), forall_operands, irept::get(), pointer_logict::get_null_object(), irept::id(), id2string(), irept::id_string(), integer2string(), exprt::is_false(), exprt::is_true(), exprt::op0(), exprt::operands(), out, pointer_logic, configt::ansi_ct::pointer_width, dstringt::size(), and exprt::type().
Referenced by convert_expr().
|
private |
Definition at line 330 of file cvc_conv.cpp.
References convert_expr(), irept::id(), exprt::op0(), exprt::op1(), exprt::operands(), out, and exprt::type().
Referenced by convert_expr().
|
protectedvirtual |
Definition at line 724 of file cvc_conv.cpp.
References array_index_type(), convert_address_of_rec(), convert_array_index(), convert_array_value(), convert_as_bv(), convert_comparison_expr(), convert_constant_expr(), convert_equality_expr(), convert_identifier(), convert_minus_expr(), convert_plus_expr(), convert_struct_expr(), convert_typecast_expr(), convert_with_expr(), forall_expr, forall_operands, irept::get(), irept::get_string(), irept::id(), irept::id_string(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), out, to_array_expr(), to_integer(), to_string_constant(), and exprt::type().
Referenced by convert(), convert_address_of_rec(), convert_array_index(), convert_as_bv(), convert_binary_expr(), convert_comparison_expr(), convert_constant_expr(), convert_equality_expr(), convert_minus_expr(), convert_plus_expr(), convert_struct_expr(), convert_typecast_expr(), convert_with_expr(), and set_to().
|
private |
Definition at line 664 of file cvc_conv.cpp.
References out.
Referenced by convert_expr(), find_symbols(), and set_to().
|
private |
Definition at line 474 of file cvc_conv.cpp.
References const_literal(), out, literalt::sign(), and literalt::var_no().
Referenced by convert().
|
private |
Definition at line 407 of file cvc_conv.cpp.
References convert_expr(), irept::get(), irept::id(), irept::id_string(), exprt::op0(), exprt::op1(), exprt::operands(), out, and exprt::type().
Referenced by convert_expr().
|
private |
Definition at line 210 of file cvc_conv.cpp.
References configt::ansi_c, config, convert_expr(), cvc_pointer_type(), forall_operands, irept::get(), irept::id(), irept::id_string(), exprt::op0(), exprt::op1(), exprt::operands(), out, configt::ansi_ct::pointer_width, and exprt::type().
Referenced by convert_expr().
|
private |
Definition at line 304 of file cvc_conv.cpp.
References struct_union_typet::components(), convert_expr(), exprt::operands(), out, to_struct_type(), and exprt::type().
Referenced by convert_expr().
|
protectedvirtual |
Definition at line 1270 of file cvc_conv.cpp.
References array_index_type(), struct_union_typet::components(), cvc_pointer_type(), bitvector_typet::get_width(), irept::id(), irept::id_string(), out, typet::subtype(), to_array_type(), to_signedbv_type(), to_struct_type(), and to_unsignedbv_type().
Referenced by find_symbols(), and set_to().
|
private |
Definition at line 266 of file cvc_conv.cpp.
References convert_binary_expr(), convert_expr(), from_integer(), irept::id(), irept::id_string(), exprt::op0(), exprt::operands(), out, and exprt::type().
Referenced by convert_expr().
|
private |
Definition at line 431 of file cvc_conv.cpp.
References convert_array_index(), convert_array_value(), convert_expr(), irept::id(), irept::id_string(), exprt::op0(), exprt::operands(), out, and exprt::type().
Referenced by convert_expr().
|
staticprivate |
Definition at line 502 of file cvc_conv.cpp.
References configt::ansi_c, config, and configt::ansi_ct::pointer_width.
Referenced by convert_address_of_rec(), convert_plus_expr(), and convert_type().
|
private |
Definition at line 1223 of file cvc_conv.cpp.
References convert_identifier(), convert_type(), forall_operands, irept::get(), irept::get_string(), irept::id(), id2string(), identifier_map, out, and exprt::type().
Referenced by convert(), find_symbols(), and set_to().
|
private |
Definition at line 1342 of file cvc_conv.cpp.
References find_symbols(), irept::id(), array_typet::size(), and to_array_type().
|
staticprivate |
Definition at line 515 of file cvc_conv.cpp.
References irept::set().
Referenced by convert_array_index().
Implements prop_convt.
Definition at line 35 of file cvc_conv.cpp.
References boolean_assignment, literalt::is_false(), literalt::is_true(), literalt::sign(), and literalt::var_no().
Referenced by ~cvc_convt().
|
virtual |
Implements decision_proceduret.
Definition at line 25 of file cvc_conv.cpp.
References boolean_assignment.
Referenced by ~cvc_convt().
|
virtual |
Implements decision_proceduret.
Definition at line 1162 of file cvc_conv.cpp.
References convert_expr(), convert_identifier(), convert_type(), find_symbols(), forall_operands, irept::get(), irept::id(), id2string(), identifier_map, exprt::op0(), exprt::op1(), exprt::operands(), out, and exprt::type().
Referenced by ~cvc_convt().
|
protected |
Definition at line 63 of file cvc_conv.h.
Referenced by l_get(), and print_assignment().
|
protected |
Definition at line 61 of file cvc_conv.h.
Referenced by find_symbols(), and set_to().
|
protected |
Definition at line 44 of file cvc_conv.h.
Referenced by convert().
|
protected |
Definition at line 37 of file cvc_conv.h.
Referenced by convert(), convert_address_of_rec(), convert_as_bv(), convert_binary_expr(), convert_comparison_expr(), convert_constant_expr(), convert_equality_expr(), convert_expr(), convert_identifier(), convert_literal(), convert_minus_expr(), convert_plus_expr(), convert_struct_expr(), convert_type(), convert_typecast_expr(), convert_with_expr(), find_symbols(), set_to(), and ~cvc_convt().
|
protected |
Definition at line 43 of file cvc_conv.h.
Referenced by convert_address_of_rec(), and convert_constant_expr().