CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
bv_minimize.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Georg Weissenbacher, georg.weissenbacher@inf.ethz.ch
6
7\*******************************************************************/
8
9#include "bv_minimize.h"
10
12
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
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)
48 }
49
50 prop_minimize.objective(lit, weight);
51 }
52 }
53}
54
56{
57 // build bit-wise objective function
58
60
61 for(minimization_listt::const_iterator
62 l_it=symbols.begin();
63 l_it!=symbols.end();
64 l_it++)
65 {
67 }
68
69 // now solve
71}
SAT-optimizer for minimizing expressions.
std::set< exprt > minimization_listt
Definition bv_minimize.h:23
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:39
messaget log
Definition bv_minimize.h:37
void operator()(const minimization_listt &objectives)
void add_objective(class prop_minimizet &prop_minimize, const exprt &objective)
boolbvt & boolbv
Definition bv_minimize.h:36
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
const irep_idt & id() const
Definition irep.h:388
message_handlert & get_message_handler()
Definition message.h:183
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT.
The type of an expression, extends irept.
Definition type.h:29
std::vector< literalt > bvt
Definition literal.h:201
SAT Minimizer.