cprover
Loading...
Searching...
No Matches
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
20 prop_convt &_prop_conv,
21 message_handlert &message_handler)
22 : prop_conv(_prop_conv), log(message_handler)
23{
24}
25
27void prop_minimizet::objective(const literalt condition, const weightt weight)
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
61 POSTCONDITION(found);
62}
63
66{
67 std::vector<objectivet> &entry = current->second;
68
69 bvt or_clause;
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 {
87 exprt::operandst disjuncts;
88 disjuncts.reserve(or_clause.size());
89 for(const auto &literal : or_clause)
90 disjuncts.push_back(literal_exprt(literal));
91
92 return prop_conv.convert(disjunction(disjuncts));
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!
113 literalt c = constraint();
114
115 if(c.is_false())
117 else
118 {
119 _iterations++;
120
121 prop_conv.push({literal_exprt{c}});
122 dec_result = prop_conv();
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}
resultt
Result of running the decision procedure.
std::vector< exprt > operandst
Definition expr.h:58
bool is_false() const
Definition literal.h:161
static eomt eom
Definition message.h:289
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
std::vector< literalt > bvt
Definition literal.h:201
literalt const_literal(bool value)
Definition literal.h:188
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