cprover
bv_minimize.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Georg Weissenbacher, georg.weissenbacher@inf.ethz.ch
6 
7 \*******************************************************************/
8 
9 #include "bv_minimize.h"
10 
11 #include <cassert>
12 
13 #include <solvers/prop/minimize.h>
14 
16  prop_minimizet &prop_minimize,
17  const exprt &objective)
18 {
19  // build bit-wise objective function
20 
21  const typet &type=objective.type();
22 
23  if(type.id()==ID_bool ||
24  type.id()==ID_unsignedbv ||
25  type.id()==ID_c_enum ||
26  type.id()==ID_c_enum_tag ||
27  type.id()==ID_signedbv ||
28  type.id()==ID_fixedbv)
29  {
30  // convert it
31  bvt bv=boolbv.convert_bv(objective);
32 
33  for(std::size_t i=0; i<bv.size(); i++)
34  {
35  literalt lit=bv[i];
36 
37  if(lit.is_constant()) // fixed already, ignore
38  continue;
39 
40  prop_minimizet::weightt weight=(1LL<<i);
41 
42  if(type.id()==ID_signedbv ||
43  type.id()==ID_fixedbv ||
44  type.id()==ID_floatbv)
45  {
46  // The top bit is the sign bit, and makes things _smaller_,
47  // and thus needs to be maximized.
48  if(i==bv.size()-1)
49  weight=-weight;
50  }
51 
52  prop_minimize.objective(lit, weight);
53  }
54  }
55 }
56 
58 {
59  // build bit-wise objective function
60 
61  prop_minimizet prop_minimize(boolbv);
63 
64  for(minimization_listt::const_iterator
65  l_it=symbols.begin();
66  l_it!=symbols.end();
67  l_it++)
68  {
69  add_objective(prop_minimize, *l_it);
70  }
71 
72  // now solve
73  prop_minimize();
74 }
void operator()(const minimization_listt &objectives)
Definition: bv_minimize.cpp:57
The type of an expression.
Definition: type.h:22
void objective(const literalt condition, const weightt weight=1)
Add an objective.
Definition: minimize.cpp:19
SAT Minimizer.
typet & type()
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:259
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT...
Definition: minimize.h:23
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
SAT-optimizer for minimizing expressions.
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
std::set< exprt > minimization_listt
Definition: bv_minimize.h:23
message_handlert & get_message_handler()
Definition: message.h:153
bool is_constant() const
Definition: literal.h:165
Base class for all expressions.
Definition: expr.h:42
long long signed int weightt
Definition: minimize.h:56
boolbvt & boolbv
Definition: bv_minimize.h:36
void add_objective(class prop_minimizet &prop_minimize, const exprt &objective)
Definition: bv_minimize.cpp:15
std::vector< literalt > bvt
Definition: literal.h:200