solver/Optimizer.h
```00001 /*
00002  * Optimizer.h
00003  *
00004  *  Created on: Nov 15, 2011
00005  *      Author: isil
00006  */
00007
00008 #ifndef OPTIMIZER_H_
00009 #define OPTIMIZER_H_
00010
00011 #include "SatValue.h"
00012 #include <map>
00013 using namespace std;
00014
00015 class CNode;
00016 class Term;
00017
00018 class Optimizer {
00019
00020 private:
00021         CNode* c;
00022         Term* cost_fn;
00023         long int upper_bound;
00024         int opt_cost;
00025         map<Term*, SatValue> assignments;
00026         bool min;
00027         int num_iterations;
00028
00029         int num_solves;
00030         int ticks;
00031
00032
00033
00034 public:
00035         /*
00036          * Optimizes the value of cost_fn subject to constraint c.
00037          * The boolean min specifies whether we want to minimize cost_fn
00038          * (min = true), or whether we want to maximize it (min = false).
00039          * The integer bound specifies an upper bound for maximization
00040          * problems, and a lower bound for minimization problems.
00041          */
00042         Optimizer(CNode* c, Term* cost_fn, bool min, long int bound,
00043                         int num_iterations = -1);
00044
00045         /*
00046          * If c is unsatisfiable, the optimal cost will be higher than max cost
00047          * for maximization problems and lower than min cost for minimization
00048          * problems.
00049          */
00050         long int get_optimal_cost();
00051
00052         const map<Term*, SatValue>& get_assignment();
00053         ~Optimizer();
00054
00055         string get_stats();
00056
00057 private:
00058         void maximize();
00059 };
00060
00061 #endif /* OPTIMIZER_H_ */
```