picasso/ModelChecker.h at master · lorensipro/picasso · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
/****************************************************************************************
 *
 * This file is part of Graph Coloring
 *
 * Graph Coloring is free software: you can redistribute it and/or modify it
 * under the terms of the GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Graph Coloring is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY;
 * without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
 * See the GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License along with Graph Coloring.
 * If not, see http://www.gnu.org/licenses/.
 *
 * Contributors:
 *       - Valentin Montmirail (valentin.montmirail@univ-cotedazur.fr)
 ***************************************************************************************************/

#ifndef MODEL_CHECKER_H
#define MODEL_CHECKER_H

#include "Graph.h"
#include "SimpSolver.h"
#include "SolverTypes.h"
#include "Encoder.h"
#include "Enc_Totalizer.h"
#include "SAT_Encoding.h"

using namespace std;
using namespace msp;

class ModelChecker {

private:

	Solver* solver;
	Graph* graph;
	SAT_Encoding* encoding;
	unsigned int k;

	vector<bool> model;

	vector<string> colors = {
	  "red",
	  "blue",
	  "green",
	  "purple",
	  "orange",
	  "yellow",
	  "salmon",
	  "paleturquoise",
	  "lightsteelblue",
	  "palegreen",
	  "palegoldenrod",
	  "aliceblue",
	  "crimson",
	  "darksalmon",
	  "pink",
	  "deeppink",
	  "gold",
	  "firebrick",
	  "dimgrey",
	  "darkorange",
	  "cyan",
	  "beige",
	  "darkgreen",
	  "orchid",
	  "turquoise",
	  "tomato",
	  "tan",
	  "royalblue"
	};

public:

	ModelChecker(Solver * s, Graph* g, SAT_Encoding* e, unsigned int _k) { solver = s; graph = g; encoding = e; k = _k; }

	void setSolver(vector<bool> & copy) { model = copy; }

	void toDOT_color(FILE* file=stdout);

	unsigned int obtainNbColors();

};

#endif