cprover
|
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT. More...
#include <minimize.h>
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) | |
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 |
std::size_t | _number_satisfied |
std::size_t | _number_objectives |
weightt | _value |
prop_convt & | prop_conv |
objectivest::reverse_iterator | current |
Additional Inherited Members |
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT.
Definition at line 23 of file minimize.h.
typedef std::map<weightt, std::vector<objectivet> > prop_minimizet::objectivest |
Definition at line 75 of file minimize.h.
typedef long long signed int prop_minimizet::weightt |
Definition at line 56 of file minimize.h.
|
inlineexplicit |
Definition at line 26 of file minimize.h.
|
protected |
Build constraints that require us to improve on at least one goal, greedily.
Definition at line 61 of file minimize.cpp.
|
protected |
Fix objectives that are satisfied.
Definition at line 36 of file minimize.cpp.
|
inline |
Definition at line 44 of file minimize.h.
|
inline |
Definition at line 39 of file minimize.h.
Add an objective.
Definition at line 19 of file minimize.cpp.
void prop_minimizet::operator() | ( | ) |
Try to cover all objectives.
Definition at line 93 of file minimize.cpp.
|
inline |
Definition at line 49 of file minimize.h.
|
protected |
Definition at line 79 of file minimize.h.
|
protected |
Definition at line 80 of file minimize.h.
|
protected |
Definition at line 80 of file minimize.h.
|
protected |
Definition at line 81 of file minimize.h.
|
protected |
Definition at line 87 of file minimize.h.
objectivest prop_minimizet::objectives |
Definition at line 76 of file minimize.h.
|
protected |
Definition at line 82 of file minimize.h.