#include <prop_conv_solver.h>

Inheritance diagram for prop_conv_solvert:

Collaboration diagram for prop_conv_solvert:

Public Types
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
	prop_conv_solvert (propt &_prop, message_handlert &message_handler)

virtual	~prop_conv_solvert ()=default

virtual void	finish_eager_conversion ()

decision_proceduret::resultt	dec_solve (const exprt &) override
	Implementation of the decision procedure. 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	~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'. More...

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

resultt	operator() ()
	Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat. More...

resultt	operator() (const exprt &assumption)
	Run the decision procedure to solve the problem under the given assumption. More...

virtual	~decision_proceduret ()

Public Member Functions inherited from solver_resource_limitst
virtual	~solver_resource_limitst ()=default

Public Attributes
bool	use_cache = true

bool	equality_propagation = true

bool	freeze_all = false

Protected Member Functions
virtual std::optional< 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)

Protected Attributes
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...

Static Protected Attributes
static const char *	context_prefix = "prop_conv::context$"

Private Member Functions
void	add_constraints_to_prop (const exprt &expr, bool value)
	Helper method used by `set_to` for adding the constraints to `prop`. More...

Detailed Description

Definition at line 27 of file prop_conv_solver.h.

Member Typedef Documentation

◆ cachet

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

Definition at line 84 of file prop_conv_solver.h.

◆ symbolst

typedef std::map<irep_idt, literalt> prop_conv_solvert::symbolst

Definition at line 83 of file prop_conv_solver.h.

Constructor & Destructor Documentation

◆ prop_conv_solvert()

prop_conv_solvert::prop_conv_solvert	(	propt &	_prop,
		message_handlert &	message_handler
	)

inline

Definition at line 32 of file prop_conv_solver.h.

◆ ~prop_conv_solvert()

virtual prop_conv_solvert::~prop_conv_solvert ( )

virtualdefault

Member Function Documentation

◆ add_constraints_to_prop()

void prop_conv_solvert::add_constraints_to_prop	(	const exprt &	expr,
		bool	value
	)

private

Helper method used by set_to for adding the constraints to prop.

This method is private because it must not be used by derived classes.

Definition at line 346 of file prop_conv_solver.cpp.

◆ clear_cache()

virtual void prop_conv_solvert::clear_cache ( )

inlinevirtual

Reimplemented in boolbvt.

Definition at line 78 of file prop_conv_solver.h.

◆ convert()

literalt prop_conv_solvert::convert ( const exprt & expr )

overridevirtual

Convert a Boolean expression and return the corresponding literal.

Implements prop_convt.

Definition at line 154 of file prop_conv_solver.cpp.

◆ convert_bool()

literalt prop_conv_solvert::convert_bool ( const exprt & expr )

protectedvirtual

Definition at line 190 of file prop_conv_solver.cpp.

◆ convert_rest()

literalt prop_conv_solvert::convert_rest ( const exprt & expr )

protectedvirtual

Reimplemented in boolbvt, bv_pointerst, and bv_pointers_widet.

Definition at line 313 of file prop_conv_solver.cpp.

◆ dec_solve()

decision_proceduret::resultt prop_conv_solvert::dec_solve ( const exprt & assumption )

overridevirtual

Implementation of the decision procedure.

Implements decision_proceduret.

Reimplemented in string_refinementt, and bv_refinementt.

Definition at line 443 of file prop_conv_solver.cpp.

◆ decision_procedure_text()

std::string prop_conv_solvert::decision_procedure_text ( ) const

overridevirtual

Return a textual description of the decision procedure.

Implements decision_proceduret.

Reimplemented in string_refinementt, and bv_refinementt.

Definition at line 573 of file prop_conv_solver.cpp.

◆ finish_eager_conversion()

void prop_conv_solvert::finish_eager_conversion ( )

virtual

Reimplemented in equalityt, bv_pointerst, boolbvt, arrayst, and bv_pointers_widet.

Definition at line 438 of file prop_conv_solver.cpp.

◆ get()

exprt prop_conv_solvert::get ( const exprt & ) const

overridevirtual

Return expr with variables replaced by values from satisfying assignment if available.

Return nil if not available

Implements decision_proceduret.

Reimplemented in string_refinementt.

Definition at line 485 of file prop_conv_solver.cpp.

◆ get_bool()

std::optional< bool > prop_conv_solvert::get_bool ( const exprt & expr ) const

protectedvirtual

Get a boolean value from the model if the formula is satisfiable.

If the argument is not a boolean expression from the formula, {} is returned.

Definition at line 77 of file prop_conv_solver.cpp.

◆ get_cache()

const cachet& prop_conv_solvert::get_cache ( ) const

inline

Definition at line 86 of file prop_conv_solver.h.

◆ get_hardness_collector()

hardness_collectort* prop_conv_solvert::get_hardness_collector ( )

inline

Definition at line 102 of file prop_conv_solver.h.

◆ get_literal()

literalt prop_conv_solvert::get_literal ( const irep_idt & symbol )

protectedvirtual

Definition at line 60 of file prop_conv_solver.cpp.

◆ get_number_of_solver_calls()

std::size_t prop_conv_solvert::get_number_of_solver_calls ( ) const

overridevirtual

Return the number of incremental solver calls.

Implements decision_proceduret.

Definition at line 515 of file prop_conv_solver.cpp.

◆ get_symbols()

const symbolst& prop_conv_solvert::get_symbols ( ) const

inline

Definition at line 90 of file prop_conv_solver.h.

◆ handle()

exprt prop_conv_solvert::handle ( const exprt & )

overridevirtual

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.

The returned expression may be the expression itself or a more compact but solver-specific representation.

Implements decision_proceduret.

Definition at line 38 of file prop_conv_solver.cpp.

◆ ignoring()

void prop_conv_solvert::ignoring ( const exprt & expr )

protectedvirtual

Definition at line 431 of file prop_conv_solver.cpp.

◆ is_in_conflict()

bool prop_conv_solvert::is_in_conflict ( const exprt & ) const

overridevirtual

Returns true if an expression is in the final conflict leading to UNSAT.

The argument can be a Boolean expression or something more solver-specific, e.g. a literal_exprt.

Implements conflict_providert.

Definition at line 16 of file prop_conv_solver.cpp.

◆ l_get()

tvt prop_conv_solvert::l_get ( literalt l ) const

inlineoverridevirtual

Return value of literal l from satisfying assignment.

Return tvt::UNKNOWN if not available

Implements prop_convt.

Definition at line 48 of file prop_conv_solver.h.

◆ pop()

void prop_conv_solvert::pop ( )

overridevirtual

Pop whatever is on top of the stack.

Popping from the empty stack results in an invariant violation.

Implements stack_decision_proceduret.

Definition at line 561 of file prop_conv_solver.cpp.

◆ print_assignment()

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

overridevirtual

Print satisfying assignment to out.

Implements decision_proceduret.

Definition at line 509 of file prop_conv_solver.cpp.

◆ push() [1/2]

void prop_conv_solvert::push ( )

overridevirtual

Push a new context on the stack This context becomes a child context nested in the current context.

Implements stack_decision_proceduret.

Definition at line 551 of file prop_conv_solver.cpp.

◆ push() [2/2]

void prop_conv_solvert::push ( const std::vector< exprt > & assumptions )

overridevirtual

Push assumptions in form of literal_exprt

Implements stack_decision_proceduret.

Definition at line 537 of file prop_conv_solver.cpp.

◆ set_all_frozen()

void prop_conv_solvert::set_all_frozen ( )

Definition at line 33 of file prop_conv_solver.cpp.

◆ set_equality_to_true()

bool prop_conv_solvert::set_equality_to_true ( const equal_exprt & expr )

protectedvirtual

Definition at line 320 of file prop_conv_solver.cpp.

◆ set_frozen() [1/2]

void prop_conv_solvert::set_frozen ( const bvt & bv )

Definition at line 21 of file prop_conv_solver.cpp.

◆ set_frozen() [2/2]

void prop_conv_solvert::set_frozen ( literalt a )

Definition at line 28 of file prop_conv_solver.cpp.

◆ set_time_limit_seconds()

void prop_conv_solvert::set_time_limit_seconds ( uint32_t )

inlineoverridevirtual

Set the limit for the solver to time out in seconds.

Implements solver_resource_limitst.

Definition at line 95 of file prop_conv_solver.h.

◆ set_to()

void prop_conv_solvert::set_to	(	const exprt &	expr,
		bool	value
	)

overridevirtual

For a Boolean expression expr, add the constraint 'current_context => expr' if value is true, otherwise add 'current_context => not expr'.

Implements decision_proceduret.

Reimplemented in string_refinementt.

Definition at line 522 of file prop_conv_solver.cpp.

Member Data Documentation

◆ assumption_stack

bvt prop_conv_solvert::assumption_stack

protected

Assumptions on the stack.

Definition at line 137 of file prop_conv_solver.h.

◆ cache

cachet prop_conv_solvert::cache

protected

Definition at line 126 of file prop_conv_solver.h.

◆ context_literal_counter

std::size_t prop_conv_solvert::context_literal_counter = 0

protected

To generate unique literal names for contexts.

Definition at line 140 of file prop_conv_solver.h.

◆ context_prefix

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

staticprotected

Definition at line 134 of file prop_conv_solver.h.

◆ context_size_stack

std::vector<size_t> prop_conv_solvert::context_size_stack

protected

assumption_stack is segmented in contexts; Number of assumptions in each context on the stack

Definition at line 144 of file prop_conv_solver.h.

◆ equality_propagation

bool prop_conv_solvert::equality_propagation = true

Definition at line 75 of file prop_conv_solver.h.

◆ freeze_all

bool prop_conv_solvert::freeze_all = false

Definition at line 76 of file prop_conv_solver.h.

◆ log

messaget prop_conv_solvert::log

protected

Definition at line 132 of file prop_conv_solver.h.

◆ post_processing_done

bool prop_conv_solvert::post_processing_done = false

protected

Definition at line 108 of file prop_conv_solver.h.

◆ prop

propt& prop_conv_solvert::prop

protected

Definition at line 130 of file prop_conv_solver.h.

◆ symbols

symbolst prop_conv_solvert::symbols

protected

Definition at line 121 of file prop_conv_solver.h.

◆ use_cache

bool prop_conv_solvert::use_cache = true

Definition at line 74 of file prop_conv_solver.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/prop/prop_conv_solver.h
/home/runner/work/cbmc/cbmc/src/solvers/prop/prop_conv_solver.cpp

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Static Protected Attributes

Private Member Functions

Detailed Description

Member Typedef Documentation

◆ cachet

◆ symbolst

Constructor & Destructor Documentation

◆ prop_conv_solvert()

◆ ~prop_conv_solvert()

Member Function Documentation

◆ add_constraints_to_prop()

◆ clear_cache()

◆ convert()

◆ convert_bool()

◆ convert_rest()

◆ dec_solve()

◆ decision_procedure_text()

◆ finish_eager_conversion()

◆ get()

◆ get_bool()

◆ get_cache()

◆ get_hardness_collector()

◆ get_literal()

◆ get_number_of_solver_calls()

◆ get_symbols()

◆ handle()

◆ ignoring()

◆ is_in_conflict()

◆ l_get()

◆ pop()

◆ print_assignment()

◆ push() [1/2]

◆ push() [2/2]

◆ set_all_frozen()

◆ set_equality_to_true()

◆ set_frozen() [1/2]

◆ set_frozen() [2/2]

◆ set_time_limit_seconds()

◆ set_to()

Member Data Documentation

◆ assumption_stack

◆ cache

◆ context_literal_counter

◆ context_prefix

◆ context_size_stack

◆ equality_propagation

◆ freeze_all

◆ log

◆ post_processing_done

◆ prop

◆ symbols

◆ use_cache