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
void objective(const literalt condition, const weightt weight=1)
Add an objective.
Definition: minimize.cpp:19
std::size_t size() const
Definition: minimize.h:49
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT.
Definition: minimize.h:23
weightt _value
Definition: minimize.h:81
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
unsigned iterations() const
Definition: minimize.h:44
prop_convt & prop_conv
Definition: minimize.h:82
objectivet(const literalt _condition)
Definition: minimize.h:68
objectivest::reverse_iterator current
Definition: minimize.h:87
unsigned _iterations
Definition: minimize.h:79
objectivest objectives
Definition: minimize.h:76
long long signed int weightt
Definition: minimize.h:56
std::map< weightt, std::vector< objectivet > > objectivest
Definition: minimize.h:75
literalt constraint()
Build constraints that require us to improve on at least one goal, greedily.
Definition: minimize.cpp:61
std::size_t _number_satisfied
Definition: minimize.h:80
std::size_t _number_objectives
Definition: minimize.h:80
void fix_objectives()
Fix objectives that are satisfied.
Definition: minimize.cpp:36
std::size_t number_satisfied() const
Definition: minimize.h:39
prop_minimizet(prop_convt &_prop_conv)
Definition: minimize.h:26
void operator()()
Try to cover all objectives.
Definition: minimize.cpp:93