1 /* ReadLatteStyle.cpp -- Read input data in the LattE style
2
3 Copyright 2006 Matthias Koeppe
4
5 This file is part of LattE.
6
7 LattE is free software; you can redistribute it and/or modify it
8 under the terms of the version 2 of the GNU General Public License
9 as published by the Free Software Foundation.
10
11 LattE is distributed in the hope that it will be useful, but
12 WITHOUT ANY WARRANTY; without even the implied warranty of
13 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14 General Public License for more details.
15
16 You should have received a copy of the GNU General Public License
17 along with LattE; if not, write to the Free Software Foundation,
18 Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
19 */
20
21 #include <cstdio>
22 #include <cstdlib>
23 #include <cassert>
24 #include <cctype>
25 #include "ReadLatteStyle.h"
26 #include "latte_gmp.h"
27 #include "latte_cddlib.h"
28 #include "vertices/cdd.h"
29 #include "LattException.h"
30 #include <vector>
31
32 using namespace std;
33
check_stream(const istream & f,const char * fileName,const char * proc)34 static void check_stream(const istream &f, const char *fileName,
35 const char *proc) {
36 if (f.bad() || f.fail()) {
37 cerr << "Read error on input file " << fileName << " in " << proc
38 << "." << endl;
39 THROW_LATTE(LattException::fe_Open, 0);
40 }
41 }
42 ;
43
ReadLatteStyleMatrix(const char * fileName,bool vrep,bool homogenize,bool nonnegativity)44 dd_MatrixPtr ReadLatteStyleMatrix(const char *fileName, bool vrep,
45 bool homogenize, bool nonnegativity) {
46 ifstream f(fileName);
47 if (!f) {
48 cerr << "Cannot open input file " << fileName
49 << " in ReadLatteStyleMatrix." << endl;
50 THROW_LATTE(LattException::fe_Open, 0);
51 }
52 return ReadLatteStyleMatrix(f, vrep, homogenize, fileName, nonnegativity);
53 }
54
55 /* NONNEGATIVITY contains 1-based variable indices.
56 Add corrresponding non-negativity constraints and return a new
57 matrix.
58 */
add_nonnegativity(dd_MatrixPtr matrix,const vector<int> & nonnegatives,int num_homog)59 static dd_MatrixPtr add_nonnegativity(dd_MatrixPtr matrix,
60 const vector<int> &nonnegatives, int num_homog) {
61 int num_nonnegative = nonnegatives.size();
62 int numOfVectors = matrix->rowsize;
63 int numOfVars_hom = matrix->colsize;
64 int numOfVars = numOfVars_hom - num_homog;
65 dd_MatrixPtr new_matrix = dd_CreateMatrix(numOfVectors + num_nonnegative,
66 numOfVars_hom);
67 new_matrix->numbtype = dd_Rational;
68 new_matrix->representation = dd_Inequality;
69 int i, j;
70 for (i = 0; i < numOfVectors; i++) {
71 for (j = 0; j < numOfVars_hom; j++)
72 dd_set(new_matrix->matrix[i][j], matrix->matrix[i][j]);
73 if (set_member(i + 1, matrix->linset))
74 set_addelem(new_matrix->linset, i + 1);
75 }
76 int k;
77 for (k = 0; k < num_nonnegative; k++, i++) {
78 int index = nonnegatives[k]; /* 1-based */
79 for (j = 0; j < numOfVars; j++)
80 dd_set_si(new_matrix->matrix[i][j + num_homog], 0);
81 dd_set_si(new_matrix->matrix[i][index + num_homog], 1);
82 }
83 return new_matrix;
84 }
85
ReadLatteStyleMatrix(istream & f,bool vrep,bool homogenize,const char * fileName,bool nonnegativity)86 dd_MatrixPtr ReadLatteStyleMatrix(istream &f, bool vrep, bool homogenize,
87 const char *fileName, bool nonnegativity) {
88 dd_set_global_constants();
89 int numOfVectors, numOfVars;
90 f >> numOfVectors >> numOfVars;
91 int num_homog = homogenize ? 1 : 0;
92 int numOfVars_hom = numOfVars + num_homog;
93 check_stream(f, fileName, "ReadLatteStyleMatrix");
94 dd_MatrixPtr matrix = dd_CreateMatrix(numOfVectors, numOfVars_hom);
95 matrix->numbtype = dd_Rational;
96 if (vrep)
97 matrix->representation = dd_Generator;
98 else
99 matrix->representation = dd_Inequality;
100 int i, j;
101 mpq_class x;
102 for (i = 0; i < numOfVectors; i++) {
103 for (j = 0; j < numOfVars; j++) {
104 f >> x;
105 check_stream(f, fileName, "ReadLatteStyleMatrix");
106 dd_set(matrix->matrix[i][j + num_homog], x.get_mpq_t());
107 }
108 }
109 // Skip whitespace
110 while (isspace(f.peek())) {
111 char c;
112 f.get(c);
113 }
114 while (!f.eof()) {
115 // Interpret keywords
116 char buffer[20];
117 f.get(buffer, 20, ' ');
118 if (strcmp(buffer, "linearity") == 0) {
119 int num_linearity;
120 f >> num_linearity;
121 check_stream(f, fileName, "ReadLatteStyleMatrix");
122 int i;
123 for (i = 0; i < num_linearity; i++) {
124 int index; /* 1-based */
125 f >> index;
126 check_stream(f, fileName, "ReadLatteStyleMatrix");
127 set_addelem(matrix->linset, index /* 1-based */);
128 }
129 } else if (strcmp(buffer, "nonnegative") == 0) {
130 if (vrep) {
131 cerr << "Keyword `" << buffer << "' not valid in vrep mode."
132 << endl;
133 THROW_LATTE(LattException::ue_BadFileOption, 0);
134 }
135 int num_nonnegative;
136 f >> num_nonnegative;
137 check_stream(f, fileName, "ReadLatteStyleMatrix");
138 vector<int> nonnegatives(num_nonnegative);
139 int k;
140 for (k = 0; k < num_nonnegative; k++) {
141 int index; /* 1-based */
142 f >> index;
143 check_stream(f, fileName, "ReadLatteStyleMatrix");
144 nonnegatives[k] = index;
145 }
146 // Create a new matrix that includes non-negativity
147 // inequalities.
148 dd_MatrixPtr new_matrix = add_nonnegativity(matrix, nonnegatives,
149 num_homog);
150 dd_FreeMatrix(matrix);
151 matrix = new_matrix;
152 } else {
153 cerr << "Unknown keyword `" << buffer << "' in input file "
154 << fileName << " in ReadLatteStyleMatrix." << endl;
155 THROW_LATTE(LattException::ue_BadFileOption, 0);
156 }
157 // Skip whitespace
158 while (!f.eof() && isspace(f.peek())) {
159 char c;
160 f.get(c);
161 }
162 }
163 if (nonnegativity) {
164 vector<int> nonnegatives(numOfVars);
165 int k;
166 for (k = 0; k < numOfVars; k++)
167 nonnegatives[k] = k + 1; /* 1-based indices */
168 dd_MatrixPtr new_matrix = add_nonnegativity(matrix, nonnegatives,
169 num_homog);
170 dd_FreeMatrix(matrix);
171 matrix = new_matrix;
172 }
173 return matrix;
174 }
175
WriteLatteStyleMatrix(const char * fileName,dd_MatrixPtr matrix)176 void WriteLatteStyleMatrix(const char *fileName, dd_MatrixPtr matrix) {
177 ofstream f(fileName);
178 WriteLatteStyleMatrix(f, matrix);
179 }
180
WriteLatteStyleMatrix(ostream & f,dd_MatrixPtr matrix)181 void WriteLatteStyleMatrix(ostream &f, dd_MatrixPtr matrix) {
182 f << matrix->rowsize << " " << matrix->colsize << endl;
183 int i;
184 for (i = 0; i < matrix->rowsize; i++) {
185 int j;
186 for (j = 0; j < matrix->colsize; j++)
187 f << matrix->matrix[i][j] << " ";
188 f << endl;
189 }
190 int num_linearity = set_card(matrix->linset);
191 if (num_linearity > 0) {
192 f << "linearity " << num_linearity << " ";
193 for (i = 1; i <= matrix->rowsize; i++)
194 if (set_member(i, matrix->linset))
195 f << i << " ";
196 f << endl;
197 }
198 }
199
200