CBMC
Classes | Public Types | Public Member Functions | Public Attributes | Protected Member Functions | Protected Attributes | List of all members
prop_minimizet Class Reference

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

#include <prop_minimize.h>

+ 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 Member Functions

 prop_minimizet (prop_convt &_prop_conv, message_handlert &message_handler)
 
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 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 = 0
 
std::size_t _number_satisfied = 0
 
std::size_t _number_objectives = 0
 
weightt _value = 0
 
prop_convt & prop_conv
 
messaget log
 
objectivest::reverse_iterator current
 

Detailed Description

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

Definition at line 25 of file prop_minimize.h.

Member Typedef Documentation

◆ objectivest

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

Definition at line 68 of file prop_minimize.h.

◆ weightt

typedef long long signed int prop_minimizet::weightt

Definition at line 51 of file prop_minimize.h.

Constructor & Destructor Documentation

◆ prop_minimizet()

prop_minimizet::prop_minimizet ( prop_convt &  _prop_conv,
message_handlert &  message_handler 
)

Definition at line 19 of file prop_minimize.cpp.

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 65 of file prop_minimize.cpp.

◆ fix_objectives()

void prop_minimizet::fix_objectives ( )
protected

Fix objectives that are satisfied.

Definition at line 42 of file prop_minimize.cpp.

◆ iterations()

unsigned prop_minimizet::iterations ( ) const
inline

Definition at line 39 of file prop_minimize.h.

◆ number_satisfied()

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

Definition at line 34 of file prop_minimize.h.

◆ objective()

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

Add an objective.

Definition at line 27 of file prop_minimize.cpp.

◆ operator()()

void prop_minimizet::operator() ( )

Try to cover all objectives.

Definition at line 97 of file prop_minimize.cpp.

◆ size()

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

Definition at line 44 of file prop_minimize.h.

Member Data Documentation

◆ _iterations

unsigned prop_minimizet::_iterations = 0
protected

Definition at line 72 of file prop_minimize.h.

◆ _number_objectives

std::size_t prop_minimizet::_number_objectives = 0
protected

Definition at line 74 of file prop_minimize.h.

◆ _number_satisfied

std::size_t prop_minimizet::_number_satisfied = 0
protected

Definition at line 73 of file prop_minimize.h.

◆ _value

weightt prop_minimizet::_value = 0
protected

Definition at line 75 of file prop_minimize.h.

◆ current

objectivest::reverse_iterator prop_minimizet::current
protected

Definition at line 82 of file prop_minimize.h.

◆ log

messaget prop_minimizet::log
protected

Definition at line 77 of file prop_minimize.h.

◆ objectives

objectivest prop_minimizet::objectives

Definition at line 69 of file prop_minimize.h.

◆ prop_conv

prop_convt& prop_minimizet::prop_conv
protected

Definition at line 76 of file prop_minimize.h.

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