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