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 &	operator= (const messaget &other)

	messaget (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level) const

mstreamt &	error () const

mstreamt &	warning () const

mstreamt &	result () const

mstreamt &	status () const

mstreamt &	statistics () const

mstreamt &	progress () const

mstreamt &	debug () const

void	conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
	Generate output to `message_stream` using `output_generator` if the configured verbosity is at least as high as that of `message_stream`. More...

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 unsigned	eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
	Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...

static commandt	command (unsigned c)
	Create an ECMA-48 SGR (Select Graphic Rendition) command. More...

Static Public Attributes inherited from messaget
static eomt	eom

static const commandt	reset
	return to default formatting, as defined by the terminal More...

static const commandt	red
	render text with red foreground color More...

static const commandt	green
	render text with green foreground color More...

static const commandt	yellow
	render text with yellow foreground color More...

static const commandt	blue
	render text with blue foreground color More...

static const commandt	magenta
	render text with magenta foreground color More...

static const commandt	cyan
	render text with cyan foreground color More...

static const commandt	bright_red
	render text with bright red foreground color More...

static const commandt	bright_green
	render text with bright green foreground color More...

static const commandt	bright_yellow
	render text with bright yellow foreground color More...

static const commandt	bright_blue
	render text with bright blue foreground color More...

static const commandt	bright_magenta
	render text with bright magenta foreground color More...

static const commandt	bright_cyan
	render text with bright cyan foreground color More...

static const commandt	bold
	render text with bold font More...

static const commandt	faint
	render text with faint font More...

static const commandt	italic
	render italic text More...

static const commandt	underline
	render underlined text More...

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 75 of file minimize.h.

◆ weightt

typedef long long signed int prop_minimizet::weightt

Definition at line 56 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.

◆ fix_objectives()

void prop_minimizet::fix_objectives ( )

protected

Fix objectives that are satisfied.

Definition at line 36 of file minimize.cpp.

◆ iterations()

unsigned prop_minimizet::iterations ( ) const

inline

Definition at line 44 of file minimize.h.

◆ number_satisfied()

std::size_t prop_minimizet::number_satisfied ( ) const

inline

Definition at line 39 of file minimize.h.

◆ objective()

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

Add an objective.

Definition at line 19 of file minimize.cpp.

◆ operator()()

void prop_minimizet::operator() ( void )

Try to cover all objectives.

Definition at line 93 of file minimize.cpp.

◆ size()

std::size_t prop_minimizet::size ( ) const

inline

Definition at line 49 of file minimize.h.

Member Data Documentation

◆ _iterations

unsigned prop_minimizet::_iterations

protected

Definition at line 79 of file minimize.h.

◆ _number_objectives

std::size_t prop_minimizet::_number_objectives

protected

Definition at line 80 of file minimize.h.

◆ _number_satisfied

std::size_t prop_minimizet::_number_satisfied

protected

Definition at line 80 of file minimize.h.

◆ _value

weightt prop_minimizet::_value

protected

Definition at line 81 of file minimize.h.

◆ current

objectivest::reverse_iterator prop_minimizet::current

protected

Definition at line 87 of file minimize.h.

◆ objectives

objectivest prop_minimizet::objectives

Definition at line 76 of file minimize.h.

◆ prop_conv

prop_convt& prop_minimizet::prop_conv

protected

Definition at line 82 of file minimize.h.

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

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

Classes

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ objectivest

◆ weightt

Constructor & Destructor Documentation

◆ prop_minimizet()

Member Function Documentation

◆ constraint()

◆ fix_objectives()

◆ iterations()

◆ number_satisfied()

◆ objective()

◆ operator()()

◆ size()

Member Data Documentation

◆ _iterations

◆ _number_objectives

◆ _number_satisfied

◆ _value

◆ current

◆ objectives

◆ prop_conv