1 /*++
2 Copyright (c) 2015 Microsoft Corporation
3
4 --*/
5
6 #include "muz/ddnf/ddnf.h"
7 #include "muz/rel/tbv.h"
8 #include <iostream>
9 #include <fstream>
10 #include <list>
11 #include <vector>
12 #include <string>
13 #include <cstring>
14 #include <cstdlib>
15 #include <map>
16
17 /*
18 TBD: count number of nodes, number of operations across all insertions
19 */
20
read_nums(std::istream & is,unsigned & x,unsigned & y)21 void read_nums(std::istream& is, unsigned & x, unsigned& y) {
22 x = 0; y = 0;
23 is >> x;
24 is >> y;
25 std::string line;
26 std::getline(is, line);
27 }
28
29 static char const* g_file = nullptr;
30
31
create_forwarding(char const * file,datalog::ddnf_core & ddnf,ptr_vector<tbv> & tbvs,vector<unsigned_vector> & fwd_indices)32 void create_forwarding(
33 char const* file,
34 datalog::ddnf_core& ddnf,
35 ptr_vector<tbv>& tbvs,
36 vector<unsigned_vector>& fwd_indices) {
37
38 IF_VERBOSE(1, verbose_stream() << "creating (and forgetting) forwarding index\n";);
39 std::ifstream is(file);
40 if (is.bad() || is.fail()) {
41 std::cout << "could not load " << file << "\n";
42 exit(0);
43 }
44
45 std::string line;
46 unsigned W, M;
47 read_nums(is, W, M);
48 tbv_manager& tbvm = ddnf.get_tbv_manager();
49 tbv* tX = tbvm.allocateX();
50 unsigned_vector forwarding_set;
51 for (unsigned r = 0; r < M; ++r) {
52 unsigned P, K;
53 read_nums(is, K, P);
54 ddnf.reset_accumulate();
55 unsigned p;
56 fwd_indices.push_back(unsigned_vector());
57 unsigned_vector& forwarding_index = fwd_indices.back();
58 forwarding_index.resize(ddnf.size());
59 for (unsigned g = 0; g < K; ++g) {
60 is >> p;
61 std::getline(is, line);
62 tbv* t = tbvm.allocate(line.c_str());
63 if (p > P) {
64 std::cout << "port number " << p << " too big " << P << "\n";
65 tbvm.display(std::cout, *t) << " " << line << "\n";
66 exit(0);
67 }
68 forwarding_set.reset();
69 ddnf.accumulate(*t, forwarding_set);
70 for (unsigned i = 0; i < forwarding_set.size(); ++i) {
71 forwarding_index[forwarding_set[i]] = p;
72 }
73 tbvs.push_back(t);
74 if (p == 0 && tbvm.equals(*t, *tX)) break;
75 }
76 }
77 tbvm.deallocate(tX);
78 }
79
populate_ddnf(char const * file,ptr_vector<tbv> & tbvs)80 datalog::ddnf_core* populate_ddnf(char const* file, ptr_vector<tbv>& tbvs) {
81
82 IF_VERBOSE(1, verbose_stream() << "populate ddnf\n";);
83
84 std::ifstream is(file);
85 if (is.bad() || is.fail()) {
86 std::cout << "could not load " << file << "\n";
87 exit(0);
88 }
89
90 std::string line;
91 unsigned W, M;
92 read_nums(is, W, M);
93 datalog::ddnf_core* ddnf = alloc(datalog::ddnf_core, W);
94 tbv_manager& tbvm = ddnf->get_tbv_manager();
95 tbv* tX = tbvm.allocateX();
96 for (unsigned r = 0; r < M; ++r) {
97 unsigned P, K;
98 read_nums(is, K, P);
99 IF_VERBOSE(1, verbose_stream() << K << " " << P << "\n";);
100 unsigned p;
101 for (unsigned g = 0; g < K; ++g) {
102 is >> p;
103 std::getline(is, line);
104 tbv* t = tbvm.allocate(line.c_str());
105 ddnf->insert(*t);
106 IF_VERBOSE(2, tbvm.display(verbose_stream() << line << " ", *t) << "\n";);
107 tbvs.push_back(t);
108 if (p > P) {
109 std::cout << "port number " << p << " too big " << P << "\n";
110 tbvm.display(std::cout, *t) << " " << line << "\n";
111 exit(0);
112 }
113 if (p == 0 && tbvm.equals(*t, *tX)) break;
114 // std::cout << ddnf->well_formed() << "\n";
115 }
116 }
117
118 tbvm.deallocate(tX);
119
120 return ddnf;
121 }
122
123
read_args(char ** argv,int argc,int & i)124 static void read_args(char ** argv, int argc, int& i) {
125 if (argc == i + 2) {
126 g_file = argv[i + 1];
127 ++i;
128 return;
129 }
130
131 if (!g_file) {
132 std::cout << "Need routing table file as argument. Arguments provided: ";
133 for (int j = i; j < argc; ++j) {
134 std::cout << argv[j] << " ";
135 }
136 std::cout << "\n";
137 exit(0);
138 }
139
140 }
141
142 typedef std::pair<unsigned, unsigned> u_pair;
143
operator ()uu_eq144 struct uu_eq { bool operator()(u_pair u1, u_pair u2) const { return u1 == u2; } };
145
146 typedef map<u_pair, unsigned, pair_hash<unsigned_hash, unsigned_hash>, uu_eq > pair_table;
147
refine_forwarding(unsigned_vector & p,unsigned_vector const & q)148 static unsigned refine_forwarding(
149 unsigned_vector& p,
150 unsigned_vector const& q) {
151 unsigned sz = p.size();
152 unsigned n = 0, m = 0;
153 pair_table tbl;
154 for (unsigned i = 0; i < sz; ++i) {
155 u_pair pr = std::make_pair(p[i], q[i]);
156 if (tbl.find(pr, m)) {
157 p[i] = m;
158 }
159 else {
160 p[i] = n;
161 tbl.insert(pr, n++);
162 }
163 }
164 return n;
165 }
166
refine_forwarding(datalog::ddnf_core & ddnf,vector<unsigned_vector> const & fwd_indices)167 static void refine_forwarding(
168 datalog::ddnf_core& ddnf,
169 vector<unsigned_vector> const& fwd_indices) {
170 unsigned_vector roots;
171 roots.resize(ddnf.size());
172 for (unsigned i = 0; i < roots.size(); ++i) {
173 roots[i] = 0;
174 }
175 unsigned max_class = 1;
176 for (unsigned i = 0; i < fwd_indices.size(); ++i) {
177 unsigned_vector const& fwd = fwd_indices[i];
178 max_class = refine_forwarding(roots, fwd);
179 }
180 std::cout << "num classes: " << max_class << "\n";
181 }
182
tst_ddnf(char ** argv,int argc,int & i)183 void tst_ddnf(char ** argv, int argc, int& i) {
184 read_args(argv, argc, i);
185 ptr_vector<tbv> tbvs;
186 datalog::ddnf_core* ddnf = populate_ddnf(g_file, tbvs);
187 IF_VERBOSE(1, ddnf->display(verbose_stream()););
188 vector<unsigned_vector> fwd_indices;
189 create_forwarding(g_file, *ddnf, tbvs, fwd_indices);
190 refine_forwarding(*ddnf, fwd_indices);
191 std::cout << "resulting size: " << ddnf->size() << "\n";
192 ddnf->display_statistics(std::cout);
193 IF_VERBOSE(1, ddnf->display(verbose_stream());
194 verbose_stream() << ddnf->well_formed() << "\n";);
195
196 tbv_manager& tbvm = ddnf->get_tbv_manager();
197 for (unsigned i = 0; i < tbvs.size(); ++i) {
198 tbvm.deallocate(tbvs[i]);
199 }
200 dealloc(ddnf);
201 }
202
tst_ddnf1()203 void tst_ddnf1() {
204 enable_trace("ddnf");
205 unsigned W = 2;
206 datalog::ddnf_core ddnf(W);
207 tbv_manager& tbvm = ddnf.get_tbv_manager();
208 tbv* tXX = tbvm.allocate("xx");
209 tbv* t1X = tbvm.allocate("1x");
210 tbv* tX1 = tbvm.allocate("x1");
211 tbv* t11 = tbvm.allocate("11");
212 ddnf.insert(*tXX);
213 ddnf.insert(*t11);
214 ddnf.insert(*tX1);
215 ddnf.insert(*t1X);
216 ddnf.display(std::cout);
217 tbvm.deallocate(tXX);
218 tbvm.deallocate(t1X);
219 tbvm.deallocate(tX1);
220 tbvm.deallocate(t11);
221 }
222
223
224