CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
prop_minimize.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Minimize some target function incrementally
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "prop_minimize.h"
13
14#include <util/threeval.h>
15
16#include "literal_expr.h"
17#include "prop_conv.h"
18
21 message_handlert &message_handler)
22 : prop_conv(_prop_conv), log(message_handler)
23{
24}
25
28{
29 if(weight > 0)
30 {
31 objectives[weight].push_back(objectivet(condition));
33 }
34 else if(weight < 0)
35 {
36 objectives[-weight].push_back(objectivet(!condition));
38 }
39}
40
43{
44 std::vector<objectivet> &entry = current->second;
45 bool found = false;
46
47 for(std::vector<objectivet>::iterator o_it = entry.begin();
48 o_it != entry.end();
49 ++o_it)
50 {
51 if(!o_it->fixed && prop_conv.l_get(o_it->condition).is_false())
52 {
54 _value += current->first;
55 prop_conv.set_to(literal_exprt(o_it->condition), false); // fix it
56 o_it->fixed = true;
57 found = true;
58 }
59 }
60
62}
63
66{
67 std::vector<objectivet> &entry = current->second;
68
70
71 for(std::vector<objectivet>::iterator o_it = entry.begin();
72 o_it != entry.end();
73 ++o_it)
74 {
75 if(!o_it->fixed)
76 or_clause.push_back(!o_it->condition);
77 }
78
79 // This returns false if the clause is empty,
80 // i.e., no further improvement possible.
81 if(or_clause.empty())
82 return const_literal(false);
83 else if(or_clause.size() == 1)
84 return or_clause.front();
85 else
86 {
88 disjuncts.reserve(or_clause.size());
89 for(const auto &literal : or_clause)
91
93 }
94}
95
98{
99 _iterations = 0;
101 _value = 0;
102 bool last_was_SAT = false;
103
104 // go from high weights to low ones
105 for(current = objectives.rbegin(); current != objectives.rend(); current++)
106 {
107 log.status() << "weight " << current->first << messaget::eom;
108
110 do
111 {
112 // We want to improve on one of the objectives, please!
114
115 if(c.is_false())
117 else
118 {
119 _iterations++;
120
123
124 switch(dec_result)
125 {
127 last_was_SAT = false;
128 break;
129
131 last_was_SAT = true;
132 fix_objectives(); // fix the ones we got
133 break;
134
136 log.error() << "decision procedure failed" << messaget::eom;
137 last_was_SAT = false;
138 return;
139 }
140 }
142 }
143
144 if(!last_was_SAT)
145 {
146 // We don't have a satisfying assignment to work with.
147 // Run solver again to get one.
148
149 prop_conv.pop();
150 (void)prop_conv();
151 }
152}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
resultt
Result of running the decision procedure.
virtual void set_to(const exprt &, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
std::vector< exprt > operandst
Definition expr.h:58
mstreamt & error() const
Definition message.h:391
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
virtual tvt l_get(literalt l) const =0
Return value of literal l from satisfying assignment.
virtual literalt convert(const exprt &expr)=0
Convert a Boolean expression and return the corresponding literal.
objectivest objectives
prop_minimizet(prop_convt &_prop_conv, message_handlert &message_handler)
void fix_objectives()
Fix objectives that are satisfied.
prop_convt & prop_conv
std::size_t _number_objectives
unsigned _iterations
std::size_t _number_satisfied
long long signed int weightt
literalt constraint()
Build constraints that require us to improve on at least one goal, greedily.
void operator()()
Try to cover all objectives.
void objective(const literalt condition, const weightt weight=1)
Add an objective.
objectivest::reverse_iterator current
virtual void pop()=0
Pop whatever is on top of the stack.
virtual void push(const std::vector< exprt > &assumptions)=0
Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions.
std::vector< literalt > bvt
Definition literal.h:201
literalt const_literal(bool value)
Definition literal.h:188
double log(double x)
Definition math.c:2449
SAT Minimizer.
#define POSTCONDITION(CONDITION)
Definition invariant.h:479
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:71