cprover
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_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () 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_convtprop_conv
 
objectivest::reverse_iterator current
 
- Protected Attributes inherited from messaget
message_handlertmessage_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: