cprover
minimize.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: SAT Minimizer
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_PROP_MINIMIZE_H
13 #define CPROVER_SOLVERS_PROP_MINIMIZE_H
14 
15 #include <map>
16 
17 #include <util/message.h>
18 
19 #include "prop_conv.h"
20 
24 {
25 public:
26  explicit prop_minimizet(prop_convt &_prop_conv):
27  _iterations(0),
30  _value(0),
31  prop_conv(_prop_conv)
32  {
33  }
34 
35  void operator()();
36 
37  // statistics
38 
39  std::size_t number_satisfied() const
40  {
41  return _number_satisfied;
42  }
43 
44  unsigned iterations() const
45  {
46  return _iterations;
47  }
48 
49  std::size_t size() const
50  {
51  return _number_objectives;
52  }
53 
54  // managing the objectives
55 
56  typedef long long signed int weightt;
57 
58  // adds an objective with given weight
59  void objective(
60  const literalt condition,
61  const weightt weight=1);
62 
63  struct objectivet
64  {
66  bool fixed;
67 
68  explicit objectivet(const literalt _condition):
69  condition(_condition), fixed(false)
70  {
71  }
72  };
73 
74  // the map of objectives, sorted by weight
75  typedef std::map<weightt, std::vector<objectivet> > objectivest;
77 
78 protected:
79  unsigned _iterations;
83 
85  void fix_objectives();
86 
87  objectivest::reverse_iterator current;
88 };
89 
90 #endif // CPROVER_SOLVERS_PROP_MINIMIZE_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
prop_minimizet::weightt
long long signed int weightt
Definition: minimize.h:56
prop_minimizet::operator()
void operator()()
Try to cover all objectives.
Definition: minimize.cpp:93
prop_minimizet::objective
void objective(const literalt condition, const weightt weight=1)
Add an objective.
Definition: minimize.cpp:19
prop_minimizet::current
objectivest::reverse_iterator current
Definition: minimize.h:87
prop_minimizet
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT.
Definition: minimize.h:23
prop_minimizet::size
std::size_t size() const
Definition: minimize.h:49
prop_convt
Definition: prop_conv.h:27
prop_minimizet::objectivet::fixed
bool fixed
Definition: minimize.h:66
prop_minimizet::prop_conv
prop_convt & prop_conv
Definition: minimize.h:82
prop_minimizet::iterations
unsigned iterations() const
Definition: minimize.h:44
prop_minimizet::objectivet
Definition: minimize.h:63
prop_minimizet::_iterations
unsigned _iterations
Definition: minimize.h:79
prop_conv.h
prop_minimizet::_number_objectives
std::size_t _number_objectives
Definition: minimize.h:80
prop_minimizet::prop_minimizet
prop_minimizet(prop_convt &_prop_conv)
Definition: minimize.h:26
prop_minimizet::_number_satisfied
std::size_t _number_satisfied
Definition: minimize.h:80
prop_minimizet::fix_objectives
void fix_objectives()
Fix objectives that are satisfied.
Definition: minimize.cpp:36
prop_minimizet::_value
weightt _value
Definition: minimize.h:81
prop_minimizet::objectivest
std::map< weightt, std::vector< objectivet > > objectivest
Definition: minimize.h:75
prop_minimizet::objectives
objectivest objectives
Definition: minimize.h:76
prop_minimizet::objectivet::condition
literalt condition
Definition: minimize.h:65
literalt
Definition: literal.h:24
prop_minimizet::number_satisfied
std::size_t number_satisfied() const
Definition: minimize.h:39
prop_minimizet::constraint
literalt constraint()
Build constraints that require us to improve on at least one goal, greedily.
Definition: minimize.cpp:61
message.h
prop_minimizet::objectivet::objectivet
objectivet(const literalt _condition)
Definition: minimize.h:68