prop_minimizet Class Reference

Computes a satisfying assignment of minimal cost according to a const function using incremental SAT. More...

#include <minimize.h>

Inheritance diagram for prop_minimizet:

Collaboration diagram for prop_minimizet:

Classes
struct	objectivet

Public Types
typedef long long signed int	weightt
typedef std::map< weightt, std::vector< objectivet > >	objectivest
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 }

Public Member Functions
	prop_minimizet (prop_convt &_prop_conv)
void	operator() ()
	Try to cover all objectives. More...
std::size_t	number_satisfied () const
unsigned	iterations () const
std::size_t	size () const
void	objective (const literalt condition, const weightt weight=1)
	Add an objective. More...
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 ()

Public Attributes
objectivest	objectives

Protected Member Functions
literalt	constraint ()
	Build constraints that require us to improve on at least one goal, greedily. More...
void	fix_objectives ()
	Fix objectives that are satisfied. More...

Protected Attributes
unsigned	_iterations
std::size_t	_number_satisfied
std::size_t	_number_objectives
weightt	_value
prop_convt &	prop_conv
objectivest::reverse_iterator	current
Protected Attributes inherited from messaget
message_handlert *	message_handler
mstreamt	mstream

Additional Inherited Members
Static Public Member Functions inherited from messaget
static mstreamt &	eom (mstreamt &m)
static mstreamt &	endl (mstreamt &m)

Detailed Description

Computes a satisfying assignment of minimal cost according to a const function using incremental SAT.

Definition at line 23 of file minimize.h.

Member Typedef Documentation

objectivest

typedef std::map<weightt, std::vector<objectivet> > prop_minimizet::objectivest

Definition at line 72 of file minimize.h.

weightt

typedef long long signed int prop_minimizet::weightt

Definition at line 53 of file minimize.h.

Constructor & Destructor Documentation

prop_minimizet()

prop_minimizet::prop_minimizet ( prop_convt &  _prop_conv )

inlineexplicit

Definition at line 26 of file minimize.h.

Member Function Documentation

constraint()

literalt prop_minimizet::constraint ( )

protected

Build constraints that require us to improve on at least one goal, greedily.

Definition at line 61 of file minimize.cpp.

References const_literal(), prop_convt::convert(), exprt::copy_to_operands(), current, forall_literals, and prop_conv.

Referenced by operator()().

fix_objectives()

void prop_minimizet::fix_objectives ( )

protected

Fix objectives that are satisfied.

Definition at line 36 of file minimize.cpp.

References _number_satisfied, _value, current, tvt::is_false(), prop_convt::l_get(), prop_conv, and decision_proceduret::set_to().

Referenced by operator()().

iterations()

unsigned prop_minimizet::iterations ( ) const

inline

Definition at line 41 of file minimize.h.

References _iterations.

number_satisfied()

std::size_t prop_minimizet::number_satisfied ( ) const

inline

Definition at line 36 of file minimize.h.

References _number_satisfied.

objective()

void prop_minimizet::objective	(	const literalt	condition,
		const weightt	weight = 1
	)

Add an objective.

Definition at line 19 of file minimize.cpp.

References _number_objectives, and objectives.

Referenced by bv_minimizet::add_objective(), and counterexample_beautificationt::operator()().

operator()()

void prop_minimizet::operator()

(

void

)

Try to cover all objectives.

Definition at line 93 of file minimize.cpp.

References _iterations, _number_satisfied, _value, constraint(), current, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, decision_proceduret::dec_solve(), messaget::eom(), messaget::error(), fix_objectives(), prop_convt::has_set_assumptions(), literalt::is_false(), objectives, prop_conv, prop_convt::set_assumptions(), and messaget::status().

size()

std::size_t prop_minimizet::size ( ) const

inline

Definition at line 46 of file minimize.h.

References _number_objectives.

Member Data Documentation

_iterations

unsigned prop_minimizet::_iterations

protected

Definition at line 76 of file minimize.h.

Referenced by iterations(), and operator()().

_number_objectives

std::size_t prop_minimizet::_number_objectives

protected

Definition at line 77 of file minimize.h.

Referenced by objective(), and size().

_number_satisfied

std::size_t prop_minimizet::_number_satisfied

protected

Definition at line 77 of file minimize.h.

Referenced by fix_objectives(), number_satisfied(), and operator()().

_value

weightt prop_minimizet::_value

protected

Definition at line 78 of file minimize.h.

Referenced by fix_objectives(), and operator()().

current

objectivest::reverse_iterator prop_minimizet::current

protected

Definition at line 84 of file minimize.h.

Referenced by constraint(), fix_objectives(), and operator()().

objectives

objectivest prop_minimizet::objectives

Definition at line 73 of file minimize.h.

Referenced by objective(), and operator()().

prop_conv

prop_convt& prop_minimizet::prop_conv

protected

Definition at line 79 of file minimize.h.

Referenced by constraint(), fix_objectives(), and operator()().

---

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

• solvers/prop/minimize.h
• solvers/prop/minimize.cpp