#include <equality.h>

Inheritance diagram for equalityt:

Collaboration diagram for equalityt:

Classes
struct	typestructt

Public Types
using	SUB = prop_conv_solvert

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 class	resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR }
	Result of running the decision procedure. More...

Public Member Functions
	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

virtual void	finish_eager_conversion ()

decision_proceduret::resultt	dec_solve () override
	Run the decision procedure to solve the problem. More...

void	print_assignment (std::ostream &out) const override
	Print satisfying assignment to `out`. More...

std::string	decision_procedure_text () const override
	Return a textual description of the decision procedure. More...

exprt	get (const exprt &expr) const override
	Return `expr` with variables replaced by values from satisfying assignment if available. More...

tvt	l_get (literalt a) const override
	Return value of literal `l` from satisfying assignment. More...

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. More...

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. More...

bool	is_in_conflict (const exprt &expr) const override
	Returns true if an expression is in the final conflict leading to UNSAT. More...

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'. More...

void	push () override
	Push a new context on the stack This context becomes a child context nested in the current context. More...

void	push (const std::vector< exprt > &assumptions) override
	Push `assumptions` in form of `literal_exprt` More...

void	pop () override
	Pop whatever is on top of the stack. More...

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. More...

std::size_t	get_number_of_solver_calls () const override
	Return the number of incremental solver calls. More...

hardness_collectort *	get_hardness_collector ()

Public Member Functions inherited from conflict_providert
virtual bool	is_in_conflict (const exprt &) const =0
	Returns true if an expression is in the final conflict leading to UNSAT. More...

virtual	~conflict_providert ()=default

Public Member Functions inherited from prop_convt
virtual	~prop_convt ()

virtual literalt	convert (const exprt &expr)=0
	Convert a Boolean expression and return the corresponding literal. More...

virtual tvt	l_get (literalt l) const =0
	Return value of literal `l` from satisfying assignment. More...

Public Member Functions inherited from stack_decision_proceduret
virtual void	push (const std::vector< exprt > &assumptions)=0
	Pushes a new context on the stack that consists of the given (possibly empty vector of) `assumptions`. More...

virtual void	push ()=0
	Push a new context on the stack This context becomes a child context nested in the current context. More...

virtual void	pop ()=0
	Pop whatever is on top of the stack. More...

virtual	~stack_decision_proceduret ()=default

Public Member Functions inherited from decision_proceduret
virtual void	set_to (const exprt &expr, bool value)=0
	For a Boolean expression `expr`, add the constraint 'expr' if `value` is `true`, otherwise add 'not expr'. More...

void	set_to_true (const exprt &expr)
	For a Boolean expression `expr`, add the constraint 'expr'. More...

void	set_to_false (const exprt &expr)
	For a Boolean expression `expr`, add the constraint 'not expr'. More...

virtual exprt	handle (const exprt &expr)=0
	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. More...

resultt	operator() ()
	Run the decision procedure to solve the problem. More...

virtual exprt	get (const exprt &expr) const =0
	Return `expr` with variables replaced by values from satisfying assignment if available. More...

virtual void	print_assignment (std::ostream &out) const =0
	Print satisfying assignment to `out`. More...

virtual std::string	decision_procedure_text () const =0
	Return a textual description of the decision procedure. More...

virtual std::size_t	get_number_of_solver_calls () const =0
	Return the number of incremental solver calls. More...

virtual	~decision_proceduret ()

Public Member Functions inherited from solver_resource_limitst
virtual void	set_time_limit_seconds (uint32_t)=0
	Set the limit for the solver to time out in seconds. More...

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 optionalt< bool >	get_bool (const exprt &expr) const
	Get a boolean value from the model if the formula is satisfiable. More...

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)

virtual resultt	dec_solve ()=0
	Run the decision procedure to solve the problem. More...

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. More...

std::size_t	context_literal_counter = 0
	To generate unique literal names for contexts. More...

std::vector< size_t >	context_size_stack
	`assumption_stack` is segmented in contexts; Number of assumptions in each context on the stack More...

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:

solvers/flattening/equality.h
solvers/flattening/equality.cpp

Classes

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ elements_revt

◆ elementst

◆ equalitiest

◆ SUB

◆ typemapt

Constructor & Destructor Documentation

◆ equalityt()

Member Function Documentation

◆ add_equality_constraints() [1/2]

◆ add_equality_constraints() [2/2]

◆ equality()

◆ equality2()

◆ finish_eager_conversion()

Member Data Documentation

◆ typemap