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):
28  prop_conv(_prop_conv)
29  {
30  }
31 
32  void operator()();
33 
34  // statistics
35 
36  std::size_t number_satisfied() const
37  {
38  return _number_satisfied;
39  }
40 
41  unsigned iterations() const
42  {
43  return _iterations;
44  }
45 
46  std::size_t size() const
47  {
48  return _number_objectives;
49  }
50 
51  // managing the objectives
52 
53  typedef long long signed int weightt;
54 
55  // adds an objective with given weight
56  void objective(
57  const literalt condition,
58  const weightt weight=1);
59 
60  struct objectivet
61  {
63  bool fixed;
64 
65  explicit objectivet(const literalt _condition):
66  condition(_condition), fixed(false)
67  {
68  }
69  };
70 
71  // the map of objectives, sorted by weight
72  typedef std::map<weightt, std::vector<objectivet> > objectivest;
74 
75 protected:
76  unsigned _iterations;
80 
82  void fix_objectives();
83 
84  objectivest::reverse_iterator current;
85 };
86 
87 #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:46
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT...
Definition: minimize.h:23
weightt _value
Definition: minimize.h:78
unsigned iterations() const
Definition: minimize.h:41
prop_convt & prop_conv
Definition: minimize.h:79
objectivet(const literalt _condition)
Definition: minimize.h:65
objectivest::reverse_iterator current
Definition: minimize.h:84
unsigned _iterations
Definition: minimize.h:76
objectivest objectives
Definition: minimize.h:73
long long signed int weightt
Definition: minimize.h:53
std::map< weightt, std::vector< objectivet > > objectivest
Definition: minimize.h:72
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:77
std::size_t _number_objectives
Definition: minimize.h:77
void fix_objectives()
Fix objectives that are satisfied.
Definition: minimize.cpp:36
std::size_t number_satisfied() const
Definition: minimize.h:36
prop_minimizet(prop_convt &_prop_conv)
Definition: minimize.h:26
void operator()()
Try to cover all objectives.
Definition: minimize.cpp:93