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 72 of file minimize.h.
typedef long long signed int prop_minimizet::weightt |
Definition at line 53 of file minimize.h.
|
inlineexplicit |
Definition at line 26 of file minimize.h.
References operator()().
|
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()().
|
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()().
|
inline |
Definition at line 41 of file minimize.h.
References _iterations.
|
inline |
Definition at line 36 of file minimize.h.
References _number_satisfied.
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()().
void prop_minimizet::operator() | ( | void | ) |
Try to cover all objectives.
Definition at line 93 of file minimize.cpp.
References _iterations, _number_satisfied, _value, constraint(), current, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, decision_proceduret::dec_solve(), messaget::eom(), messaget::error(), fix_objectives(), prop_convt::has_set_assumptions(), literalt::is_false(), objectives, prop_conv, prop_convt::set_assumptions(), and messaget::status().
Referenced by prop_minimizet().
|
inline |
Definition at line 46 of file minimize.h.
References _number_objectives.
|
protected |
Definition at line 76 of file minimize.h.
Referenced by iterations(), and operator()().
|
protected |
Definition at line 77 of file minimize.h.
Referenced by objective(), and size().
|
protected |
Definition at line 77 of file minimize.h.
Referenced by fix_objectives(), number_satisfied(), and operator()().
|
protected |
Definition at line 78 of file minimize.h.
Referenced by fix_objectives(), and operator()().
|
protected |
Definition at line 84 of file minimize.h.
Referenced by constraint(), fix_objectives(), and operator()().
objectivest prop_minimizet::objectives |
Definition at line 73 of file minimize.h.
Referenced by objective(), and operator()().
|
protected |
Definition at line 79 of file minimize.h.
Referenced by constraint(), fix_objectives(), and operator()().