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)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

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 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 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()()

◆ 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: