CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
prop_minimize.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: SAT Minimizer
4
5Author: 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
21class prop_convt;
22
26{
27public:
29
30 void operator()();
31
32 // statistics
33
34 std::size_t number_satisfied() const
35 {
36 return _number_satisfied;
37 }
38
39 unsigned iterations() const
40 {
41 return _iterations;
42 }
43
44 std::size_t size() const
45 {
46 return _number_objectives;
47 }
48
49 // managing the objectives
50
51 typedef long long signed int weightt;
52
53 // adds an objective with given weight
54 void objective(const literalt condition, const weightt weight = 1);
55
57 {
59 bool fixed;
60
63 {
64 }
65 };
66
67 // the map of objectives, sorted by weight
68 typedef std::map<weightt, std::vector<objectivet>> objectivest;
70
71protected:
72 unsigned _iterations = 0;
73 std::size_t _number_satisfied = 0;
74 std::size_t _number_objectives = 0;
78
80 void fix_objectives();
81
82 objectivest::reverse_iterator current;
83};
84
85#endif // CPROVER_SOLVERS_PROP_PROP_MINIMIZE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT.
objectivest objectives
void fix_objectives()
Fix objectives that are satisfied.
prop_convt & prop_conv
std::size_t number_satisfied() const
std::size_t _number_objectives
unsigned _iterations
std::size_t _number_satisfied
std::size_t size() const
long long signed int weightt
literalt constraint()
Build constraints that require us to improve on at least one goal, greedily.
std::map< weightt, std::vector< objectivet > > objectivest
void operator()()
Try to cover all objectives.
unsigned iterations() const
void objective(const literalt condition, const weightt weight=1)
Add an objective.
objectivest::reverse_iterator current
objectivet(const literalt _condition)