cprover
Loading...
Searching...
No Matches
bv_dimacst Class Reference

#include <bv_dimacs.h>

Inheritance diagram for bv_dimacst:
Collaboration diagram for bv_dimacst:

Public Member Functions

 bv_dimacst (const namespacet &_ns, dimacs_cnft &_prop, message_handlert &message_handler, const std::string &_filename)
virtual ~bv_dimacst ()
Public Member Functions inherited from bv_pointerst
 bv_pointerst (const namespacet &, propt &, message_handlert &, bool get_array_constraints=false)
void finish_eager_conversion () override
endianness_mapt endianness_map (const typet &, bool little_endian) const override
Public Member Functions inherited from boolbvt
 boolbvt (const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
virtual const bvtconvert_bv (const exprt &expr, const std::optional< std::size_t > expected_width={})
 Convert expression to vector of literalts, using an internal cache to speed up conversion if available.
exprt get (const exprt &expr) const override
 Return expr with variables replaced by values from satisfying assignment if available.
void set_to (const exprt &expr, bool value) override
 For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
void print_assignment (std::ostream &out) const override
 Print satisfying assignment to out.
exprt handle (const exprt &) override
 Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.
void clear_cache () override
mp_integer get_value (const bvt &bv)
mp_integer get_value (const bvt &bv, std::size_t offset, std::size_t width)
const boolbv_maptget_map () const
virtual std::size_t boolbv_width (const typet &type) const
virtual endianness_mapt endianness_map (const typet &type) const
Public Member Functions inherited from arrayst
 arrayst (const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
literalt record_array_equality (const equal_exprt &expr)
void record_array_index (const index_exprt &expr)
Public Member Functions inherited from equalityt
 equalityt (propt &_prop, message_handlert &message_handler)
virtual literalt equality (const exprt &e1, const exprt &e2)
void finish_eager_conversion () override
Public Member Functions inherited from prop_conv_solvert
 prop_conv_solvert (propt &_prop, message_handlert &message_handler)
virtual ~prop_conv_solvert ()=default
decision_proceduret::resultt dec_solve (const exprt &) override
 Implementation of the decision procedure.
void print_assignment (std::ostream &out) const override
 Print satisfying assignment to out.
std::string decision_procedure_text () const override
 Return a textual description of the decision procedure.
exprt get (const exprt &expr) const override
 Return expr with variables replaced by values from satisfying assignment if available.
tvt l_get (literalt a) const override
 Return value of literal l from satisfying assignment.
exprt handle (const exprt &expr) override
 Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.
void set_frozen (literalt)
void set_frozen (const bvt &)
void set_all_frozen ()
literalt convert (const exprt &expr) override
 Convert a Boolean expression and return the corresponding literal.
bool is_in_conflict (const exprt &expr) const override
 Returns true if an expression is in the final conflict leading to UNSAT.
void set_to (const exprt &expr, bool value) override
 For a Boolean expression expr, add the constraint 'current_context => expr' if value is true, otherwise add 'current_context => not expr'.
void push () override
 Push a new context on the stack This context becomes a child context nested in the current context.
void push (const std::vector< exprt > &assumptions) override
 Push assumptions in form of literal_exprt
void pop () override
 Pop whatever is on top of the stack.
const cachetget_cache () const
const symbolstget_symbols () const
void set_time_limit_seconds (uint32_t lim) override
 Set the limit for the solver to time out in seconds.
std::size_t get_number_of_solver_calls () const override
 Return the number of incremental solver calls.
hardness_collectortget_hardness_collector ()
Public Member Functions inherited from conflict_providert
virtual ~conflict_providert ()=default
Public Member Functions inherited from prop_convt
virtual ~prop_convt ()
Public Member Functions inherited from stack_decision_proceduret
virtual ~stack_decision_proceduret ()=default
Public Member Functions inherited from decision_proceduret
void set_to_true (const exprt &)
 For a Boolean expression expr, add the constraint 'expr'.
void set_to_false (const exprt &)
 For a Boolean expression expr, add the constraint 'not expr'.
resultt operator() ()
 Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.
resultt operator() (const exprt &assumption)
 Run the decision procedure to solve the problem under the given assumption.
virtual ~decision_proceduret ()
Public Member Functions inherited from solver_resource_limitst
virtual ~solver_resource_limitst ()=default

Protected Member Functions

bool write_dimacs ()
bool write_dimacs (std::ostream &)
Protected Member Functions inherited from bv_pointerst
std::size_t get_object_width (const pointer_typet &) const
std::size_t get_offset_width (const pointer_typet &) const
std::size_t get_address_width (const pointer_typet &) const
bvt encode (const mp_integer &object, const pointer_typet &) const
virtual bvt convert_pointer_type (const exprt &)
virtual bvt add_addr (const exprt &)
literalt convert_rest (const exprt &) override
bvt convert_bitvector (const exprt &) override
 Converts an expression into its gate-level representation and returns a vector of literals corresponding to the outputs of the Boolean circuit.
exprt bv_get_rec (const exprt &, const bvt &, std::size_t offset) const override
std::optional< bvtconvert_address_of_rec (const exprt &)
bvt offset_arithmetic (const pointer_typet &, const bvt &, const mp_integer &)
bvt offset_arithmetic (const pointer_typet &, const bvt &, const mp_integer &factor, const exprt &index)
bvt offset_arithmetic (const pointer_typet &type, const bvt &bv, const exprt &factor, const exprt &index)
bvt offset_arithmetic (const pointer_typet &, const bvt &, const mp_integer &factor, const bvt &index_bv)
std::pair< exprt, exprtprepare_postponed_is_dynamic_object (std::vector< symbol_exprt > &placeholders) const
 Create Boolean functions describing all dynamic and all not-dynamic object encodings over placeholders as input Boolean variables representing object bits.
std::unordered_map< exprt, exprt, irep_hashprepare_postponed_object_size (std::vector< symbol_exprt > &placeholders) const
 Create Boolean functions describing all objects of each known object size over placeholders as input Boolean variables representing object bits.
bvt object_literals (const bvt &bv, const pointer_typet &type) const
 Given a pointer encoded in bv, extract the literals identifying the object that the pointer points to.
bvt offset_literals (const bvt &bv, const pointer_typet &type) const
 Given a pointer encoded in bv, extract the literals representing the offset into an object that the pointer points to.
Protected Member Functions inherited from boolbvt
virtual bool boolbv_set_equality_to_true (const equal_exprt &expr)
bvt conversion_failed (const exprt &expr)
 Print that the expression of x has failed conversion, then return a vector of x's width.
bool type_conversion (const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
virtual literalt convert_bv_rel (const binary_relation_exprt &)
 Flatten <, >, <= and >= expressions.
virtual literalt convert_typecast (const typecast_exprt &expr)
 conversion from bitvector types to boolean
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_binary_overflow (const binary_overflow_exprt &expr)
virtual literalt convert_unary_overflow (const unary_overflow_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 binary_relation_exprt &)
virtual literalt convert_quantifier (const quantifier_exprt &expr)
virtual bvt convert_index (const exprt &array, const mp_integer &index)
 index operator with constant index
virtual bvt convert_index (const index_exprt &expr)
virtual bvt convert_bswap (const bswap_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)
 Flatten array.
virtual bvt convert_complex (const complex_exprt &expr)
virtual bvt convert_complex_real (const complex_real_exprt &expr)
virtual bvt convert_complex_imag (const complex_imag_exprt &expr)
virtual bvt convert_array_comprehension (const array_comprehension_exprt &)
virtual bvt convert_let (const let_exprt &)
virtual bvt convert_array_of (const array_of_exprt &expr)
 Flatten arrays constructed from a single element.
virtual bvt convert_union (const union_exprt &expr)
virtual bvt convert_empty_union (const empty_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 mult_exprt &expr)
virtual bvt convert_div (const div_exprt &expr)
virtual bvt convert_mod (const mod_exprt &expr)
virtual bvt convert_floatbv_op (const ieee_float_op_exprt &)
virtual bvt convert_floatbv_mod_rem (const binary_exprt &)
virtual bvt convert_floatbv_typecast (const floatbv_typecast_exprt &expr)
virtual bvt convert_floatbv_round_to_integral (const floatbv_round_to_integral_exprt &)
virtual bvt convert_member (const member_exprt &expr)
virtual bvt convert_with (const with_exprt &expr)
virtual bvt convert_update (const update_exprt &)
virtual bvt convert_update_bit (const update_bit_exprt &)
virtual bvt convert_update_bits (const update_bits_exprt &)
virtual bvt convert_case (const exprt &expr)
virtual bvt convert_cond (const cond_exprt &)
virtual bvt convert_shift (const binary_exprt &expr)
virtual bvt convert_bitwise (const exprt &expr)
virtual bvt convert_unary_minus (const unary_minus_exprt &expr)
virtual bvt convert_abs (const abs_exprt &expr)
virtual bvt convert_concatenation (const concatenation_exprt &expr)
virtual bvt convert_replication (const replication_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 bvt convert_bitreverse (const bitreverse_exprt &expr)
virtual bvt convert_saturating_add_sub (const binary_exprt &expr)
virtual bvt convert_overflow_result (const overflow_result_exprt &expr)
bvt convert_update_bits (bvt src, const exprt &index, const bvt &new_value)
void convert_with (const typet &type, const exprt &where, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)
void convert_with_bv (const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)
void convert_with_array (const array_typet &type, const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)
void convert_with_union (const union_typet &type, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)
void convert_with_struct (const struct_typet &type, const exprt &where, const exprt &new_value, 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 finish_eager_conversion_quantifiers ()
offset_mapt build_offset_map (const struct_typet &src)
binding_exprt::variablest fresh_binding (const binding_exprt &)
 create new, unique variables for the given binding
Protected Member Functions inherited from arrayst
virtual void finish_eager_conversion_arrays ()
void add_array_constraint (const lazy_constraintt &lazy, bool refine=true)
 adds array constraints (refine=true...lazily for the refinement loop)
void display_array_constraint_count ()
std::string enum_to_string (constraint_typet)
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 add_array_constraints_array_constant (const index_sett &index_set, const array_exprt &exprt)
void add_array_constraints_comprehension (const index_sett &index_set, const array_comprehension_exprt &expr)
void update_index_map (bool update_all)
void update_index_map (std::size_t i)
 merge the indices into the root
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 std::optional< bool > get_bool (const exprt &expr) const
 Get a boolean value from the model if the formula is satisfiable.
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

const std::string filename
const dimacs_cnftdimacs_cnf_prop
Protected Attributes inherited from bv_pointerst
pointer_logict pointer_logic
postponed_listt postponed_list
Protected Attributes inherited from boolbvt
boolbv_widtht bv_width
bv_utilst bv_utils
functionst functions
boolbv_mapt map
bv_cachet bv_cache
quantifier_listt quantifier_list
numberingt< irep_idtstring_numbering
std::size_t scope_counter = 0
Protected Attributes inherited from arrayst
const namespacetns
messaget log
message_handlertmessage_handler
array_equalitiest array_equalities
union_find< exprt, irep_hasharrays
index_mapt index_map
bool lazy_arrays
bool incremental_cache
bool get_array_constraints
std::list< lazy_constrainttlazy_array_constraints
std::map< exprt, bool > expr_map
array_constraint_countt array_constraint_count
std::set< std::size_t > update_indices
std::unordered_set< irep_idtarray_comprehension_args
Protected Attributes inherited from equalityt
typemapt typemap
Protected Attributes inherited from prop_conv_solvert
bool post_processing_done = false
symbolst symbols
cachet cache
proptprop
messaget log
bvt assumption_stack
 Assumptions on the stack.
std::size_t context_literal_counter = 0
 To generate unique literal names for contexts.
std::vector< size_t > context_size_stack
 assumption_stack is segmented in contexts; Number of assumptions in each context on the stack

Additional Inherited Members

Public Types inherited from boolbvt
enum class  unbounded_arrayt { U_NONE , U_ALL , U_AUTO }
Public Types inherited from arrayst
typedef equalityt SUB
Public Types inherited from equalityt
using SUB = prop_conv_solvert
Public Types inherited from prop_conv_solvert
typedef std::map< irep_idt, literaltsymbolst
typedef std::unordered_map< exprt, literalt, irep_hashcachet
Public Types inherited from decision_proceduret
enum class  resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR }
 Result of running the decision procedure. More...
Public Attributes inherited from boolbvt
unbounded_arrayt unbounded_array
Public Attributes inherited from prop_conv_solvert
bool use_cache = true
bool equality_propagation = true
bool freeze_all = false
Protected Types inherited from bv_pointerst
typedef boolbvt SUB
typedef std::list< postponedtpostponed_listt
Protected Types inherited from boolbvt
typedef arrayst SUB
typedef std::unordered_map< const exprt, bvt, irep_hashbv_cachet
typedef std::list< quantifiertquantifier_listt
typedef std::vector< std::size_t > offset_mapt
Protected Types inherited from arrayst
enum class  lazy_typet {
  ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF ,
  ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_LET
}
enum class  constraint_typet {
  ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF ,
  ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_EQUALITY ,
  ARRAY_LET
}
typedef std::list< array_equalitytarray_equalitiest
typedef std::set< exprtindex_sett
typedef std::map< std::size_t, index_settindex_mapt
typedef std::map< constraint_typet, size_t > array_constraint_countt
Protected Types inherited from equalityt
typedef std::unordered_map< const exprt, unsigned, irep_hashelementst
typedef std::map< std::pair< unsigned, unsigned >, literaltequalitiest
typedef std::map< unsigned, exprtelements_revt
typedef std::unordered_map< const typet, typestructt, irep_hashtypemapt
Static Protected Member Functions inherited from bv_pointerst
static bvt object_offset_encoding (const bvt &object, const bvt &offset)
 Construct a pointer encoding from given encodings of object and offset.
Static Protected Attributes inherited from prop_conv_solvert
static const char * context_prefix = "prop_conv::context$"

Detailed Description

Definition at line 19 of file bv_dimacs.h.

Constructor & Destructor Documentation

◆ bv_dimacst()

bv_dimacst::bv_dimacst ( const namespacet & _ns,
dimacs_cnft & _prop,
message_handlert & message_handler,
const std::string & _filename )

Definition at line 19 of file bv_dimacs.cpp.

◆ ~bv_dimacst()

virtual bv_dimacst::~bv_dimacst ( )
inlinevirtual

Definition at line 28 of file bv_dimacs.h.

Member Function Documentation

◆ write_dimacs() [1/2]

bool bv_dimacst::write_dimacs ( )
protected

Definition at line 30 of file bv_dimacs.cpp.

◆ write_dimacs() [2/2]

bool bv_dimacst::write_dimacs ( std::ostream & out)
protected

Definition at line 46 of file bv_dimacs.cpp.

Member Data Documentation

◆ dimacs_cnf_prop

const dimacs_cnft& bv_dimacst::dimacs_cnf_prop
protected

Definition at line 35 of file bv_dimacs.h.

◆ filename

const std::string bv_dimacst::filename
protected

Definition at line 34 of file bv_dimacs.h.


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