cprover
prop_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_PROP_MINIMIZE_H
13 #define CPROVER_SOLVERS_PROP_PROP_MINIMIZE_H
14 
15 #include <map>
16 
17 #include <util/message.h>
18 
19 #include "literal.h"
20 #include "prop_conv.h"
21 
25 {
26 public:
27  prop_minimizet(prop_convt &_prop_conv, message_handlert &message_handler);
28 
29  void operator()();
30 
31  // statistics
32 
33  std::size_t number_satisfied() const
34  {
35  return _number_satisfied;
36  }
37 
38  unsigned iterations() const
39  {
40  return _iterations;
41  }
42 
43  std::size_t size() const
44  {
45  return _number_objectives;
46  }
47 
48  // managing the objectives
49 
50  typedef long long signed int weightt;
51 
52  // adds an objective with given weight
53  void objective(const literalt condition, const weightt weight = 1);
54 
55  struct objectivet
56  {
58  bool fixed;
59 
60  explicit objectivet(const literalt _condition)
61  : condition(_condition), fixed(false)
62  {
63  }
64  };
65 
66  // the map of objectives, sorted by weight
67  typedef std::map<weightt, std::vector<objectivet>> objectivest;
69 
70 protected:
71  unsigned _iterations = 0;
72  std::size_t _number_satisfied = 0;
73  std::size_t _number_objectives = 0;
77 
79  void fix_objectives();
80 
81  objectivest::reverse_iterator current;
82 };
83 
84 #endif // CPROVER_SOLVERS_PROP_PROP_MINIMIZE_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
prop_minimizet::weightt
long long signed int weightt
Definition: prop_minimize.h:50
prop_minimizet::operator()
void operator()()
Try to cover all objectives.
Definition: prop_minimize.cpp:96
prop_minimizet::objective
void objective(const literalt condition, const weightt weight=1)
Add an objective.
Definition: prop_minimize.cpp:26
prop_minimizet::current
objectivest::reverse_iterator current
Definition: prop_minimize.h:81
prop_minimizet
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT.
Definition: prop_minimize.h:25
prop_minimizet::size
std::size_t size() const
Definition: prop_minimize.h:43
prop_convt
Definition: prop_conv.h:22
prop_minimizet::objectivet::fixed
bool fixed
Definition: prop_minimize.h:58
prop_minimizet::log
messaget log
Definition: prop_minimize.h:76
prop_minimizet::prop_conv
prop_convt & prop_conv
Definition: prop_minimize.h:75
prop_minimizet::iterations
unsigned iterations() const
Definition: prop_minimize.h:38
prop_minimizet::objectivet
Definition: prop_minimize.h:56
prop_minimizet::_iterations
unsigned _iterations
Definition: prop_minimize.h:71
prop_conv.h
prop_minimizet::_number_objectives
std::size_t _number_objectives
Definition: prop_minimize.h:73
prop_minimizet::prop_minimizet
prop_minimizet(prop_convt &_prop_conv, message_handlert &message_handler)
Definition: prop_minimize.cpp:18
message_handlert
Definition: message.h:28
prop_minimizet::_number_satisfied
std::size_t _number_satisfied
Definition: prop_minimize.h:72
prop_minimizet::fix_objectives
void fix_objectives()
Fix objectives that are satisfied.
Definition: prop_minimize.cpp:41
prop_minimizet::_value
weightt _value
Definition: prop_minimize.h:74
literal.h
prop_minimizet::objectivest
std::map< weightt, std::vector< objectivet > > objectivest
Definition: prop_minimize.h:67
prop_minimizet::objectives
objectivest objectives
Definition: prop_minimize.h:68
prop_minimizet::objectivet::condition
literalt condition
Definition: prop_minimize.h:57
literalt
Definition: literal.h:26
prop_minimizet::number_satisfied
std::size_t number_satisfied() const
Definition: prop_minimize.h:33
prop_minimizet::constraint
literalt constraint()
Build constraints that require us to improve on at least one goal, greedily.
Definition: prop_minimize.cpp:64
message.h
prop_minimizet::objectivet::objectivet
objectivet(const literalt _condition)
Definition: prop_minimize.h:60