cprover
bv_minimize.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: SAT-optimizer for minimizing expressions
4
5Author: Georg Weissenbacher
6
7Date: July 2006
8
9Purpose: 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
22
23typedef std::set<exprt> minimization_listt;
24
26{
27public:
28 bv_minimizet(boolbvt &_boolbv, message_handlert &message_handler)
29 : boolbv(_boolbv), log(message_handler)
30 {
31 }
32
33 void operator()(const minimization_listt &objectives);
34
35protected:
38
39 void add_objective(
40 class prop_minimizet &prop_minimize,
41 const exprt &objective);
42};
43
45{
46public:
47 virtual const std::string description()
48 {
49 return "Bit vector minimizing SAT";
50 }
51
56 {
57 }
58
59 void minimize(const minimization_listt &objectives)
60 {
61 bv_minimizet bv_minimize{*this, log.get_message_handler()};
62 bv_minimize(objectives);
63 }
64
65 satcheckt satcheck;
67};
68
69#endif // CPROVER_SOLVERS_FLATTENING_BV_MINIMIZE_H
std::set< exprt > minimization_listt
Definition: bv_minimize.h:23
message_handlert & message_handler
Definition: arrays.h:58
Definition: boolbv.h:44
bv_minimizet(boolbvt &_boolbv, message_handlert &message_handler)
Definition: bv_minimize.h:28
messaget log
Definition: bv_minimize.h:37
void operator()(const minimization_listt &objectives)
Definition: bv_minimize.cpp:55
void add_objective(class prop_minimizet &prop_minimize, const exprt &objective)
Definition: bv_minimize.cpp:13
boolbvt & boolbv
Definition: bv_minimize.h:36
void minimize(const minimization_listt &objectives)
Definition: bv_minimize.h:59
virtual const std::string description()
Definition: bv_minimize.h:47
bv_minimizing_dect(const namespacet &_ns, message_handlert &message_handler)
Definition: bv_minimize.h:52
satcheckt satcheck
Definition: bv_minimize.h:65
Base class for all expressions.
Definition: expr.h:54
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
message_handlert & get_message_handler()
Definition: message.h:184
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT.
Definition: prop_minimize.h:26