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.

virtual void clear_cache ()

const cachet & get_cache () const

const symbolst & get_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_collectort * get_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 Types

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

Protected Member Functions

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_rest (const exprt &expr)

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

typemapt typemap

- Protected Attributes inherited from prop_conv_solvert

bool post_processing_done = false

symbolst symbols

cachet cache

propt & prop

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 Attributes inherited from prop_conv_solvert

bool use_cache = true

bool equality_propagation = true

bool freeze_all = false

- Static Protected Attributes inherited from prop_conv_solvert

static const char * context_prefix = "prop_conv::context$"

Detailed Description

Definition at line 19 of file equality.h.

Member Typedef Documentation

◆ elements_revt

typedef std::map<unsigned, exprt> equalityt::elements_revt

protected

Definition at line 41 of file equality.h.

◆ elementst

typedef std::unordered_map<const exprt, unsigned, irep_hash> equalityt::elementst

protected

Definition at line 39 of file equality.h.

◆ equalitiest

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

protected

Definition at line 40 of file equality.h.

◆ SUB

using equalityt::SUB = prop_conv_solvert

Definition at line 29 of file equality.h.

◆ typemapt

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

protected

Definition at line 50 of file equality.h.

Constructor & Destructor Documentation

◆ equalityt()

equalityt::equalityt ( propt & _prop,

message_handlert & message_handler

)

inline

Definition at line 22 of file equality.h.

Member Function Documentation

◆ add_equality_constraints() [1/2]

void equalityt::add_equality_constraints ( )

protectedvirtual

Definition at line 89 of file equality.cpp.

◆ add_equality_constraints() [2/2]

void equalityt::add_equality_constraints ( const typestructt & typestruct )

protectedvirtual

Definition at line 96 of file equality.cpp.

◆ equality()

literalt equalityt::equality ( const exprt & e1,

const exprt & e2

)

virtual

Definition at line 17 of file equality.cpp.

◆ equality2()

literalt equalityt::equality2 ( const exprt & e1,

const exprt & e2

)

protectedvirtual

Definition at line 25 of file equality.cpp.

◆ finish_eager_conversion()

void equalityt::finish_eager_conversion ( )

inlineoverridevirtual

Reimplemented from prop_conv_solvert.

Definition at line 31 of file equality.h.

Member Data Documentation

◆ typemap

typemapt equalityt::typemap

protected

Definition at line 52 of file equality.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/flattening/equality.h
/home/runner/work/cbmc/cbmc/src/solvers/flattening/equality.cpp