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
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.
virtual void set_to(const exprt &expr, 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:56
bool is_false() const
Definition: literal.h:161
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
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
Definition: prop_minimize.h:69
prop_minimizet(prop_convt &_prop_conv, message_handlert &message_handler)
void fix_objectives()
Fix objectives that are satisfied.
prop_convt & prop_conv
Definition: prop_minimize.h:76
std::size_t _number_objectives
Definition: prop_minimize.h:74
unsigned _iterations
Definition: prop_minimize.h:72
std::size_t _number_satisfied
Definition: prop_minimize.h:73
long long signed int weightt
Definition: prop_minimize.h:51
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
Definition: prop_minimize.h:82
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.
bool is_false() const
Definition: threeval.h:26
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:22