cprover
prop_minimize.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Minimize some target function incrementally
4 
5 Author: 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 
19  prop_convt &_prop_conv,
20  message_handlert &message_handler)
21  : prop_conv(_prop_conv), log(message_handler)
22 {
23 }
24 
26 void prop_minimizet::objective(const literalt condition, const weightt weight)
27 {
28  if(weight > 0)
29  {
30  objectives[weight].push_back(objectivet(condition));
32  }
33  else if(weight < 0)
34  {
35  objectives[-weight].push_back(objectivet(!condition));
37  }
38 }
39 
42 {
43  std::vector<objectivet> &entry = current->second;
44  bool found = false;
45 
46  for(std::vector<objectivet>::iterator o_it = entry.begin();
47  o_it != entry.end();
48  ++o_it)
49  {
50  if(!o_it->fixed && prop_conv.l_get(o_it->condition).is_false())
51  {
53  _value += current->first;
54  prop_conv.set_to(literal_exprt(o_it->condition), false); // fix it
55  o_it->fixed = true;
56  found = true;
57  }
58  }
59 
60  POSTCONDITION(found);
61 }
62 
65 {
66  std::vector<objectivet> &entry = current->second;
67 
68  bvt or_clause;
69 
70  for(std::vector<objectivet>::iterator o_it = entry.begin();
71  o_it != entry.end();
72  ++o_it)
73  {
74  if(!o_it->fixed)
75  or_clause.push_back(!o_it->condition);
76  }
77 
78  // This returns false if the clause is empty,
79  // i.e., no further improvement possible.
80  if(or_clause.empty())
81  return const_literal(false);
82  else if(or_clause.size() == 1)
83  return or_clause.front();
84  else
85  {
86  exprt::operandst disjuncts;
87  disjuncts.reserve(or_clause.size());
88  forall_literals(it, or_clause)
89  disjuncts.push_back(literal_exprt(*it));
90 
91  return prop_conv.convert(disjunction(disjuncts));
92  }
93 }
94 
97 {
98  _iterations = 0;
100  _value = 0;
101  bool last_was_SAT = false;
102 
103  // go from high weights to low ones
104  for(current = objectives.rbegin(); current != objectives.rend(); current++)
105  {
106  log.status() << "weight " << current->first << messaget::eom;
107 
108  decision_proceduret::resultt dec_result;
109  do
110  {
111  // We want to improve on one of the objectives, please!
112  literalt c = constraint();
113 
114  if(c.is_false())
116  else
117  {
118  _iterations++;
119 
121  dec_result = prop_conv();
122 
123  switch(dec_result)
124  {
126  last_was_SAT = false;
127  break;
128 
130  last_was_SAT = true;
131  fix_objectives(); // fix the ones we got
132  break;
133 
135  log.error() << "decision procedure failed" << messaget::eom;
136  last_was_SAT = false;
137  return;
138  }
139  }
140  } while(dec_result != decision_proceduret::resultt::D_UNSATISFIABLE);
141  }
142 
143  if(!last_was_SAT)
144  {
145  // We don't have a satisfying assignment to work with.
146  // Run solver again to get one.
147 
148  prop_conv.pop();
149  (void)prop_conv();
150  }
151 }
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_convt
Definition: prop_conv.h:22
bvt
std::vector< literalt > bvt
Definition: literal.h:201
stack_decision_proceduret::push
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.
threeval.h
messaget::status
mstreamt & status() const
Definition: message.h:414
decision_proceduret::resultt::D_UNSATISFIABLE
@ D_UNSATISFIABLE
prop_minimizet::log
messaget log
Definition: prop_minimize.h:76
prop_minimizet::prop_conv
prop_convt & prop_conv
Definition: prop_minimize.h:75
messaget::eom
static eomt eom
Definition: message.h:297
prop_minimizet::objectivet
Definition: prop_minimize.h:56
forall_literals
#define forall_literals(it, bv)
Definition: literal.h:203
prop_minimizet::_iterations
unsigned _iterations
Definition: prop_minimize.h:71
decision_proceduret::resultt::D_SATISFIABLE
@ D_SATISFIABLE
decision_proceduret::set_to
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'.
disjunction
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:29
messaget::error
mstreamt & error() const
Definition: message.h:399
prop_convt::convert
virtual literalt convert(const exprt &expr)=0
Convert a Boolean expression and return the corresponding literal.
prop_minimizet::_number_objectives
std::size_t _number_objectives
Definition: prop_minimize.h:73
literal_exprt
Definition: literal_expr.h:18
prop_minimize.h
SAT Minimizer.
prop_minimizet::prop_minimizet
prop_minimizet(prop_convt &_prop_conv, message_handlert &message_handler)
Definition: prop_minimize.cpp:18
literalt::is_false
bool is_false() const
Definition: literal.h:161
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
decision_proceduret::resultt::D_ERROR
@ D_ERROR
message_handlert
Definition: message.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
tvt::is_false
bool is_false() const
Definition: threeval.h:26
prop_minimizet::_number_satisfied
std::size_t _number_satisfied
Definition: prop_minimize.h:72
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:44
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
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:480
prop_minimizet::objectives
objectivest objectives
Definition: prop_minimize.h:68
literalt
Definition: literal.h:26
stack_decision_proceduret::pop
virtual void pop()=0
Pop whatever is on top of the stack.
prop_minimizet::constraint
literalt constraint()
Build constraints that require us to improve on at least one goal, greedily.
Definition: prop_minimize.cpp:64
prop_convt::l_get
virtual tvt l_get(literalt l) const =0
Return value of literal l from satisfying assignment.
literal_expr.h