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:
[legend]
Collaboration diagram for prop_minimizet:
[legend]

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 mstream using output_generator if the configured verbosity is at least as high as that of mstream. 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 mstreamteom (mstreamt &m)
 
static mstreamtendl (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 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.

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(), POSTCONDITION, prop_conv, and decision_proceduret::set_to().

Referenced by operator()().

◆ iterations()

unsigned prop_minimizet::iterations ( ) const
inline

Definition at line 44 of file minimize.h.

References _iterations.

◆ number_satisfied()

std::size_t prop_minimizet::number_satisfied ( ) const
inline

Definition at line 39 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()()

◆ size()

std::size_t prop_minimizet::size ( ) const
inline

Definition at line 49 of file minimize.h.

References _number_objectives.

Member Data Documentation

◆ _iterations

unsigned prop_minimizet::_iterations
protected

Definition at line 79 of file minimize.h.

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

◆ _number_objectives

std::size_t prop_minimizet::_number_objectives
protected

Definition at line 80 of file minimize.h.

Referenced by objective(), and size().

◆ _number_satisfied

std::size_t prop_minimizet::_number_satisfied
protected

Definition at line 80 of file minimize.h.

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

◆ _value

weightt prop_minimizet::_value
protected

Definition at line 81 of file minimize.h.

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

◆ current

objectivest::reverse_iterator prop_minimizet::current
protected

Definition at line 87 of file minimize.h.

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

◆ objectives

objectivest prop_minimizet::objectives

Definition at line 76 of file minimize.h.

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

◆ prop_conv

prop_convt& prop_minimizet::prop_conv
protected

Definition at line 82 of file minimize.h.

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


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