cprover
bv_minimize.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: SAT-optimizer for minimizing expressions
4 
5 Author: Georg Weissenbacher
6 
7 Date: July 2006
8 
9 Purpose: Find a satisfying assignment that minimizes a given set
10  of symbols
11 
12 \*******************************************************************/
13 
16 
17 #ifndef CPROVER_SOLVERS_FLATTENING_BV_MINIMIZE_H
18 #define CPROVER_SOLVERS_FLATTENING_BV_MINIMIZE_H
19 
21 #include <solvers/sat/satcheck.h>
22 
23 typedef std::set<exprt> minimization_listt;
24 
25 class bv_minimizet:public messaget
26 {
27 public:
28  explicit bv_minimizet(boolbvt &_boolbv):
29  boolbv(_boolbv)
30  {
31  }
32 
33  void operator()(const minimization_listt &objectives);
34 
35 protected:
37 
38  void add_objective(
39  class prop_minimizet &prop_minimize,
40  const exprt &objective);
41 };
42 
44 {
45 public:
46  virtual const std::string description()
47  {
48  return "Bit vector minimizing SAT";
49  }
50 
51  explicit bv_minimizing_dect(const namespacet &_ns):
53  {
54  }
55 
56  void minimize(const minimization_listt &objectives)
57  {
58  bv_minimizet bv_minimize(*this);
60  bv_minimize(objectives);
61  }
62 
64 };
65 
66 #endif // CPROVER_SOLVERS_FLATTENING_BV_MINIMIZE_H
void operator()(const minimization_listt &objectives)
Definition: bv_minimize.cpp:57
Definition: boolbv.h:31
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT...
Definition: minimize.h:23
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
virtual const std::string description()
Definition: bv_minimize.h:46
std::set< exprt > minimization_listt
Definition: bv_minimize.h:23
satcheckt satcheck
Definition: bv_minimize.h:63
bv_minimizing_dect(const namespacet &_ns)
Definition: bv_minimize.h:51
message_handlert & get_message_handler()
Definition: message.h:127
Base class for all expressions.
Definition: expr.h:46
bv_minimizet(boolbvt &_boolbv)
Definition: bv_minimize.h:28
boolbvt & boolbv
Definition: bv_minimize.h:36
void add_objective(class prop_minimizet &prop_minimize, const exprt &objective)
Definition: bv_minimize.cpp:15
void minimize(const minimization_listt &objectives)
Definition: bv_minimize.h:56