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 <solvers/prop/minimize.h>
12 
14  prop_minimizet &prop_minimize,
15  const exprt &objective)
16 {
17  // build bit-wise objective function
18 
19  const typet &type=objective.type();
20 
21  if(type.id()==ID_bool ||
22  type.id()==ID_unsignedbv ||
23  type.id()==ID_c_enum ||
24  type.id()==ID_c_enum_tag ||
25  type.id()==ID_signedbv ||
26  type.id()==ID_fixedbv)
27  {
28  // convert it
29  bvt bv=boolbv.convert_bv(objective);
30 
31  for(std::size_t i=0; i<bv.size(); i++)
32  {
33  literalt lit=bv[i];
34 
35  if(lit.is_constant()) // fixed already, ignore
36  continue;
37 
38  prop_minimizet::weightt weight=(1LL<<i);
39 
40  if(type.id()==ID_signedbv ||
41  type.id()==ID_fixedbv ||
42  type.id()==ID_floatbv)
43  {
44  // The top bit is the sign bit, and makes things _smaller_,
45  // and thus needs to be maximized.
46  if(i==bv.size()-1)
47  weight=-weight;
48  }
49 
50  prop_minimize.objective(lit, weight);
51  }
52  }
53 }
54 
56 {
57  // build bit-wise objective function
58 
59  prop_minimizet prop_minimize(boolbv);
61 
62  for(minimization_listt::const_iterator
63  l_it=symbols.begin();
64  l_it!=symbols.end();
65  l_it++)
66  {
67  add_objective(prop_minimize, *l_it);
68  }
69 
70  // now solve
71  prop_minimize();
72 }
void operator()(const minimization_listt &objectives)
Definition: bv_minimize.cpp:55
The type of an expression, extends irept.
Definition: type.h:27
void objective(const literalt condition, const weightt weight=1)
Add an objective.
Definition: minimize.cpp:19
SAT Minimizer.
typet & type()
Return the type of the expression.
Definition: expr.h:68
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
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
SAT-optimizer for minimizing expressions.
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
std::set< exprt > minimization_listt
Definition: bv_minimize.h:23
message_handlert & get_message_handler()
Definition: message.h:174
bool is_constant() const
Definition: literal.h:165
Base class for all expressions.
Definition: expr.h:54
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:13
std::vector< literalt > bvt
Definition: literal.h:200