cprover
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 "minimize.h"
13 
14 #include <util/threeval.h>
15 
16 #include "literal_expr.h"
17 
20  const literalt condition,
21  const weightt weight)
22 {
23  if(weight>0)
24  {
25  objectives[weight].push_back(objectivet(condition));
27  }
28  else if(weight<0)
29  {
30  objectives[-weight].push_back(objectivet(!condition));
32  }
33 }
34 
37 {
38  std::vector<objectivet> &entry=current->second;
39  bool found=false;
40 
41  for(std::vector<objectivet>::iterator
42  o_it=entry.begin();
43  o_it!=entry.end();
44  ++o_it)
45  {
46  if(!o_it->fixed &&
47  prop_conv.l_get(o_it->condition).is_false())
48  {
50  _value+=current->first;
51  prop_conv.set_to(literal_exprt(o_it->condition), false); // fix it
52  o_it->fixed=true;
53  found=true;
54  }
55  }
56 
57  POSTCONDITION(found);
58 }
59 
62 {
63  std::vector<objectivet> &entry=current->second;
64 
65  bvt or_clause;
66 
67  for(std::vector<objectivet>::iterator
68  o_it=entry.begin();
69  o_it!=entry.end();
70  ++o_it)
71  {
72  if(!o_it->fixed)
73  or_clause.push_back(!o_it->condition);
74  }
75 
76  // This returns false if the clause is empty,
77  // i.e., no further improvement possible.
78  if(or_clause.empty())
79  return const_literal(false);
80  else if(or_clause.size()==1)
81  return or_clause.front();
82  else
83  {
84  or_exprt or_expr;
85  forall_literals(it, or_clause)
86  or_expr.copy_to_operands(literal_exprt(*it));
87 
88  return prop_conv.convert(or_expr);
89  }
90 }
91 
94 {
95  // we need to use assumptions
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();
105  current!=objectives.rend();
106  current++)
107  {
108  status() << "weight " << current->first << eom;
109 
110  decision_proceduret::resultt dec_result;
111  do
112  {
113  // We want to improve on one of the objectives, please!
114  literalt c=constraint();
115 
116  if(c.is_false())
118  else
119  {
120  _iterations++;
121 
122  bvt assumptions;
123  assumptions.push_back(c);
124  prop_conv.set_assumptions(assumptions);
125  dec_result=prop_conv.dec_solve();
126 
127  switch(dec_result)
128  {
130  last_was_SAT=false;
131  break;
132 
134  last_was_SAT=true;
135  fix_objectives(); // fix the ones we got
136  break;
137 
138  default:
139  error() << "decision procedure failed" << eom;
140  last_was_SAT=false;
141  return;
142  }
143  }
144  }
146  }
147 
148  if(!last_was_SAT)
149  {
150  // We don't have a satisfying assignment to work with.
151  // Run solver again to get one.
152 
153  bvt assumptions; // no assumptions
154  prop_conv.set_assumptions(assumptions);
156  }
157 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
prop_minimizet::weightt
long long signed int weightt
Definition: minimize.h:56
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
prop_convt::set_assumptions
virtual void set_assumptions(const bvt &_assumptions)
Definition: prop_conv.cpp:19
prop_minimizet::operator()
void operator()()
Try to cover all objectives.
Definition: minimize.cpp:93
prop_minimizet::objective
void objective(const literalt condition, const weightt weight=1)
Add an objective.
Definition: minimize.cpp:19
prop_minimizet::current
objectivest::reverse_iterator current
Definition: minimize.h:87
bvt
std::vector< literalt > bvt
Definition: literal.h:200
threeval.h
messaget::status
mstreamt & status() const
Definition: message.h:401
decision_proceduret::resultt::D_UNSATISFIABLE
minimize.h
prop_minimizet::prop_conv
prop_convt & prop_conv
Definition: minimize.h:82
messaget::eom
static eomt eom
Definition: message.h:284
prop_minimizet::objectivet
Definition: minimize.h:63
forall_literals
#define forall_literals(it, bv)
Definition: literal.h:202
prop_minimizet::_iterations
unsigned _iterations
Definition: minimize.h:79
decision_proceduret::resultt::D_SATISFIABLE
decision_proceduret::set_to
virtual void set_to(const exprt &expr, bool value)=0
messaget::error
mstreamt & error() const
Definition: message.h:386
or_exprt
Boolean OR.
Definition: std_expr.h:2531
prop_convt::convert
virtual literalt convert(const exprt &expr)=0
prop_minimizet::_number_objectives
std::size_t _number_objectives
Definition: minimize.h:80
literal_exprt
Definition: literal_expr.h:17
decision_proceduret::dec_solve
virtual resultt dec_solve()=0
literalt::is_false
bool is_false() const
Definition: literal.h:160
const_literal
literalt const_literal(bool value)
Definition: literal.h:187
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:454
tvt::is_false
bool is_false() const
Definition: threeval.h:26
prop_minimizet::_number_satisfied
std::size_t _number_satisfied
Definition: minimize.h:80
prop_convt::l_get
virtual tvt l_get(literalt a) const =0
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
prop_minimizet::fix_objectives
void fix_objectives()
Fix objectives that are satisfied.
Definition: minimize.cpp:36
prop_minimizet::_value
weightt _value
Definition: minimize.h:81
prop_convt::has_set_assumptions
virtual bool has_set_assumptions() const
Definition: prop_conv.h:52
prop_minimizet::objectives
objectivest objectives
Definition: minimize.h:76
literalt
Definition: literal.h:24
prop_minimizet::constraint
literalt constraint()
Build constraints that require us to improve on at least one goal, greedily.
Definition: minimize.cpp:61
literal_expr.h