#include <cbmc_dimacs.h>

Inheritance diagram for cbmc_dimacst:

Collaboration diagram for cbmc_dimacst:

Public Member Functions
	cbmc_dimacst (const namespacet &_ns, propt &_prop, const std::string &_filename)

virtual	~cbmc_dimacst ()

Public Member Functions inherited from bv_cbmct
	bv_cbmct (const namespacet &_ns, propt &_prop)

virtual	~bv_cbmct ()

Public Member Functions inherited from bv_pointerst
	bv_pointerst (const namespacet &_ns, propt &_prop)

void	post_process () override

Public Member Functions inherited from boolbvt
	boolbvt (const namespacet &_ns, propt &_prop)

virtual const bvt &	convert_bv (const exprt &expr)

exprt	get (const exprt &expr) const override

void	set_to (const exprt &expr, bool value) override

void	print_assignment (std::ostream &out) const override

void	clear_cache () override

virtual bool	literal (const exprt &expr, std::size_t bit, literalt &literal) const

mp_integer	get_value (const bvt &bv)

mp_integer	get_value (const bvt &bv, std::size_t offset, std::size_t width)

const boolbv_mapt &	get_map () const

Public Member Functions inherited from arrayst
	arrayst (const namespacet &_ns, propt &_prop)

literalt	record_array_equality (const equal_exprt &expr)

void	record_array_index (const index_exprt &expr)

Public Member Functions inherited from equalityt
	equalityt (const namespacet &_ns, propt &_prop)

virtual literalt	equality (const exprt &e1, const exprt &e2)

void	post_process () override

Public Member Functions inherited from prop_conv_solvert
	prop_conv_solvert (const namespacet &_ns, propt &_prop)

virtual	~prop_conv_solvert ()

virtual decision_proceduret::resultt	dec_solve () override

virtual std::string	decision_procedure_text () const override

virtual tvt	l_get (literalt a) const override

virtual void	set_frozen (literalt a) override

virtual void	set_assumptions (const bvt &_assumptions) override

virtual bool	has_set_assumptions () const override

virtual void	set_all_frozen () override

virtual literalt	convert (const exprt &expr) override

virtual bool	is_in_conflict (literalt l) const override
	determine whether a variable is in the final conflict More...

virtual bool	has_is_in_conflict () const override

virtual bool	literal (const exprt &expr, literalt &literal) const

const cachet &	get_cache () const

const symbolst &	get_symbols () const

virtual void	set_frozen (literalt a)

virtual void	set_frozen (const bvt &)

Public Member Functions inherited from prop_convt
	prop_convt (const namespacet &_ns)

virtual	~prop_convt ()

literalt	operator() (const exprt &expr)

virtual void	set_frozen (const bvt &)

Public Member Functions inherited from decision_proceduret
	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)

Public Member Functions inherited from messaget
virtual void	set_message_handler (message_handlert &_message_handler)

message_handlert &	get_message_handler ()

	messaget ()

	messaget (const messaget &other)

	messaget (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level)

mstreamt &	error ()

mstreamt &	warning ()

mstreamt &	result ()

mstreamt &	status ()

mstreamt &	statistics ()

mstreamt &	progress ()

mstreamt &	debug ()

Protected Member Functions
bool	write_dimacs (const std::string &filename)

bool	write_dimacs (std::ostream &)

Protected Member Functions inherited from bv_cbmct
virtual bvt	convert_bitvector (const exprt &expr)

virtual bvt	convert_waitfor (const exprt &expr)

virtual bvt	convert_waitfor_symbol (const exprt &expr)

Protected Member Functions inherited from bv_pointerst
void	encode (std::size_t object, bvt &bv)

virtual bvt	convert_pointer_type (const exprt &expr)

virtual void	add_addr (const exprt &expr, bvt &bv)

literalt	convert_rest (const exprt &expr) override

bvt	convert_bitvector (const exprt &expr) override

exprt	bv_get_rec (const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override

bool	convert_address_of_rec (const exprt &expr, bvt &bv)

void	offset_arithmetic (bvt &bv, const mp_integer &x)

void	offset_arithmetic (bvt &bv, const mp_integer &factor, const exprt &index)

void	offset_arithmetic (bvt &bv, const mp_integer &factor, const bvt &index_bv)

void	do_postponed (const postponedt &postponed)

Protected Member Functions inherited from boolbvt
virtual bool	boolbv_set_equality_to_true (const equal_exprt &expr)

void	conversion_failed (const exprt &expr, bvt &bv)

bvt	conversion_failed (const exprt &expr)

bool	type_conversion (const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)

virtual literalt	convert_bv_rel (const exprt &expr)

virtual literalt	convert_typecast (const typecast_exprt &expr)
	conversion from bitvector types to boolean More...

virtual literalt	convert_reduction (const unary_exprt &expr)

virtual literalt	convert_onehot (const unary_exprt &expr)

virtual literalt	convert_extractbit (const extractbit_exprt &expr)

virtual literalt	convert_overflow (const exprt &expr)

virtual literalt	convert_equality (const equal_exprt &expr)

virtual literalt	convert_verilog_case_equality (const binary_relation_exprt &expr)

virtual literalt	convert_ieee_float_rel (const exprt &expr)

virtual literalt	convert_quantifier (const exprt &expr)

virtual bvt	convert_index (const exprt &array, const mp_integer &index)
	index operator with constant index More...

virtual bvt	convert_index (const index_exprt &expr)

virtual bvt	convert_byte_extract (const byte_extract_exprt &expr)

virtual bvt	convert_byte_update (const byte_update_exprt &expr)

virtual bvt	convert_constraint_select_one (const exprt &expr)

virtual bvt	convert_if (const if_exprt &expr)

virtual bvt	convert_struct (const struct_exprt &expr)

virtual bvt	convert_array (const exprt &expr)

virtual bvt	convert_vector (const exprt &expr)

virtual bvt	convert_complex (const exprt &expr)

virtual bvt	convert_complex_real (const exprt &expr)

virtual bvt	convert_complex_imag (const exprt &expr)

virtual bvt	convert_lambda (const exprt &expr)

virtual bvt	convert_array_of (const array_of_exprt &expr)

virtual bvt	convert_union (const union_exprt &expr)

virtual bvt	convert_bv_typecast (const typecast_exprt &expr)

virtual bvt	convert_add_sub (const exprt &expr)

virtual bvt	convert_mult (const exprt &expr)

virtual bvt	convert_div (const div_exprt &expr)

virtual bvt	convert_mod (const mod_exprt &expr)

virtual bvt	convert_floatbv_op (const exprt &expr)

virtual bvt	convert_floatbv_typecast (const floatbv_typecast_exprt &expr)

virtual bvt	convert_member (const member_exprt &expr)

virtual bvt	convert_with (const exprt &expr)

virtual bvt	convert_update (const exprt &expr)

virtual bvt	convert_case (const exprt &expr)

virtual bvt	convert_cond (const exprt &expr)

virtual bvt	convert_shift (const binary_exprt &expr)

virtual bvt	convert_bitwise (const exprt &expr)

virtual bvt	convert_unary_minus (const unary_exprt &expr)

virtual bvt	convert_abs (const exprt &expr)

virtual bvt	convert_concatenation (const exprt &expr)

virtual bvt	convert_replication (const replication_exprt &expr)

virtual bvt	convert_bv_literals (const exprt &expr)

virtual bvt	convert_constant (const constant_exprt &expr)

virtual bvt	convert_extractbits (const extractbits_exprt &expr)

virtual bvt	convert_symbol (const exprt &expr)

virtual bvt	convert_bv_reduction (const unary_exprt &expr)

virtual bvt	convert_not (const not_exprt &expr)

virtual bvt	convert_power (const binary_exprt &expr)

virtual bvt	convert_function_application (const function_application_exprt &expr)

virtual void	make_bv_expr (const typet &type, const bvt &bv, exprt &dest)

virtual void	make_free_bv_expr (const typet &type, exprt &dest)

void	convert_with (const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)

void	convert_with_bv (const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)

void	convert_with_array (const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)

void	convert_with_union (const union_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)

void	convert_with_struct (const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)

void	convert_update_rec (const exprt::operandst &designator, std::size_t d, const typet &type, std::size_t offset, const exprt &new_value, bvt &bv)

virtual exprt	bv_get_unbounded_array (const exprt &) const

exprt	bv_get (const bvt &bv, const typet &type) const

exprt	bv_get_cache (const exprt &expr) const

bool	is_unbounded_array (const typet &type) const override

void	post_process_quantifiers ()

void	build_offset_map (const struct_typet &src, offset_mapt &dest)

Protected Member Functions inherited from arrayst
virtual void	post_process_arrays ()

void	add_array_constraint (const lazy_constraintt &lazy, bool refine=true)
	adds array constraints (refine=true...lazily for the refinement loop) More...

void	add_array_constraints ()

void	add_array_Ackermann_constraints ()

void	add_array_constraints_equality (const index_sett &index_set, const array_equalityt &array_equality)

void	add_array_constraints (const index_sett &index_set, const exprt &expr)

void	add_array_constraints_if (const index_sett &index_set, const if_exprt &exprt)

void	add_array_constraints_with (const index_sett &index_set, const with_exprt &expr)

void	add_array_constraints_update (const index_sett &index_set, const update_exprt &expr)

void	add_array_constraints_array_of (const index_sett &index_set, const array_of_exprt &exprt)

void	update_index_map (bool update_all)

void	update_index_map (std::size_t i)
	merge the indices into the root More...

void	collect_arrays (const exprt &a)

void	collect_indices ()

void	collect_indices (const exprt &a)

Protected Member Functions inherited from equalityt
virtual literalt	equality2 (const exprt &e1, const exprt &e2)

virtual void	add_equality_constraints ()

virtual void	add_equality_constraints (const typestructt &typestruct)

Protected Member Functions inherited from prop_conv_solvert
virtual bool	get_bool (const exprt &expr, tvt &value) const
	get a boolean value from counter example if not valid More...

virtual literalt	convert_bool (const exprt &expr)

virtual bool	set_equality_to_true (const equal_exprt &expr)

virtual literalt	get_literal (const irep_idt &symbol)

virtual void	ignoring (const exprt &expr)

Protected Attributes
std::string	filename

Protected Attributes inherited from bv_pointerst
pointer_logict	pointer_logic

unsigned	object_bits

unsigned	offset_bits

unsigned	bits

postponed_listt	postponed_list

Protected Attributes inherited from boolbvt
bv_utilst	bv_utils

functionst	functions

boolbv_mapt	map

bv_cachet	bv_cache

quantifier_listt	quantifier_list

numbering< irep_idt >	string_numbering

Protected Attributes inherited from arrayst
array_equalitiest	array_equalities

union_find< exprt >	arrays

index_mapt	index_map

bool	lazy_arrays

bool	incremental_cache

std::list< lazy_constraintt >	lazy_array_constraints

std::map< exprt, bool >	expr_map

std::set< std::size_t >	update_indices

Protected Attributes inherited from equalityt
typemapt	typemap

Protected Attributes inherited from prop_conv_solvert
bool	post_processing_done

symbolst	symbols

cachet	cache

propt &	prop

Protected Attributes inherited from decision_proceduret
const namespacet &	ns

Protected Attributes inherited from messaget
message_handlert *	message_handler

mstreamt	mstream

Additional Inherited Members
Public Types inherited from boolbvt
enum	unbounded_arrayt { unbounded_arrayt::U_NONE, unbounded_arrayt::U_ALL, unbounded_arrayt::U_AUTO }

Public Types inherited from arrayst
typedef equalityt	SUB

Public Types inherited from prop_conv_solvert
typedef std::map< irep_idt, literalt >	symbolst

typedef std::unordered_map< exprt, literalt, irep_hash >	cachet

Public Types inherited from decision_proceduret
enum	resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR }

Public Types inherited from messaget
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 Public Member Functions inherited from messaget
static mstreamt &	eom (mstreamt &m)

static mstreamt &	endl (mstreamt &m)

Public Attributes inherited from boolbvt
unbounded_arrayt	unbounded_array

boolbv_widtht	boolbv_width

Public Attributes inherited from prop_conv_solvert
bool	use_cache

bool	equality_propagation

bool	freeze_all

Protected Types inherited from bv_pointerst
typedef boolbvt	SUB

typedef std::list< postponedt >	postponed_listt

Protected Types inherited from boolbvt
typedef arrayst	SUB

typedef std::unordered_map< const exprt, bvt, irep_hash >	bv_cachet

typedef std::list< quantifiert >	quantifier_listt

typedef std::vector< std::size_t >	offset_mapt

Protected Types inherited from arrayst
enum	lazy_typet { lazy_typet::ARRAY_ACKERMANN, lazy_typet::ARRAY_WITH, lazy_typet::ARRAY_IF, lazy_typet::ARRAY_OF, lazy_typet::ARRAY_TYPECAST }

typedef std::list< array_equalityt >	array_equalitiest

typedef std::set< exprt >	index_sett

typedef std::map< std::size_t, index_sett >	index_mapt

Protected Types inherited from equalityt
typedef std::unordered_map< const exprt, unsigned, irep_hash >	elementst

typedef std::map< std::pair< unsigned, unsigned >, literalt >	equalitiest

typedef std::map< unsigned, exprt >	elements_revt

typedef std::unordered_map< const typet, typestructt, irep_hash >	typemapt

Static Protected Member Functions inherited from bv_pointerst
static bool	is_ptr (const typet &type)

Detailed Description

Definition at line 17 of file cbmc_dimacs.h.

Constructor & Destructor Documentation

◆ cbmc_dimacst()

cbmc_dimacst::cbmc_dimacst	(	const namespacet &	_ns,
		propt &	_prop,
		const std::string &	_filename
	)

inline

Definition at line 20 of file cbmc_dimacs.h.

◆ ~cbmc_dimacst()

virtual cbmc_dimacst::~cbmc_dimacst ( )

inlinevirtual

Definition at line 29 of file cbmc_dimacs.h.

References filename, and write_dimacs().

Member Function Documentation

◆ write_dimacs() [1/2]

bool cbmc_dimacst::write_dimacs ( const std::string & filename )

protected

Definition at line 19 of file cbmc_dimacs.cpp.

References messaget::eom(), messaget::error(), and filename.

Referenced by ~cbmc_dimacst().

◆ write_dimacs() [2/2]

bool cbmc_dimacst::write_dimacs ( std::ostream & out )

protected

Definition at line 35 of file cbmc_dimacs.cpp.

References boolbvt::get_map(), prop_conv_solvert::get_symbols(), and prop_conv_solvert::prop.

Member Data Documentation

◆ filename

std::string cbmc_dimacst::filename

protected

Definition at line 35 of file cbmc_dimacs.h.

Referenced by write_dimacs(), and ~cbmc_dimacst().

The documentation for this class was generated from the following files:

cbmc/cbmc_dimacs.h
cbmc/cbmc_dimacs.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ cbmc_dimacst()

◆ ~cbmc_dimacst()

Member Function Documentation

◆ write_dimacs() [1/2]

◆ write_dimacs() [2/2]

Member Data Documentation

◆ filename