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()
|
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()
|
protected |
Fix objectives that are satisfied.
Definition at line 42 of file prop_minimize.cpp.
◆ iterations()
|
inline |
Definition at line 39 of file prop_minimize.h.
◆ number_satisfied()
|
inline |
Definition at line 34 of file prop_minimize.h.
◆ objective()
Add an objective.
Definition at line 27 of file prop_minimize.cpp.
◆ operator()()
| void prop_minimizet::operator() | ( | void | ) |
Try to cover all objectives.
Definition at line 97 of file prop_minimize.cpp.
◆ size()
|
inline |
Definition at line 44 of file prop_minimize.h.
Member Data Documentation
◆ _iterations
|
protected |
Definition at line 72 of file prop_minimize.h.
◆ _number_objectives
|
protected |
Definition at line 74 of file prop_minimize.h.
◆ _number_satisfied
|
protected |
Definition at line 73 of file prop_minimize.h.
◆ _value
|
protected |
Definition at line 75 of file prop_minimize.h.
◆ current
|
protected |
Definition at line 82 of file prop_minimize.h.
◆ 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
|
protected |
Definition at line 76 of file prop_minimize.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/prop/prop_minimize.h
- /home/runner/work/cbmc/cbmc/src/solvers/prop/prop_minimize.cpp
