CVC3  2.4.1
bryant.cpp
Go to the documentation of this file.
1 #include "vc.h"
2 #include "expr_transform.h"
3 #include "theory_core.h"
4 #include "command_line_flags.h"
5 #include "core_proof_rules.h"
6 
7 
8 using namespace std;
9 using namespace CVC3;
10 
11 
12 const int LIMIT = 55;
13 
14 int ExprTransform::CountSubTerms(const Expr& e, int& counter) {
15  if (e.arity() == 0)
16  return 0;
17  for (int i = 0; i < e.arity(); i++) {
18  int count = CountSubTerms(e[i], counter) + 1;
19  if (count > counter)
20  counter = count;
21  }
22  return counter;
23 }
24 
25 std::string ExprTransform::NewBryantVar(const int a, const int b){
26  std::string S;
27  std::stringstream out1, out2;
28  out1 << a;
29  out2 << b;
30  std::string Tempvar = "A";
31  S = Tempvar + out1.str() + "B" + out2.str();
32  return S;
33 }
34 
35 
36 ExprTransform::B_name_map ExprTransform::BryantNames(T_generator_map& generator_map, B_type_map& type_map) {
37  B_name_map name_map;
38  int VarTotal = 0;
39  for (T_generator_map::iterator f = generator_map.begin(); f != generator_map.end(); f++){
40  VarTotal++;
41  Type TempType = type_map.find((*f).first)->second;
42  int ArgVar = 0;
43  for (set< Expr >::iterator p = (*f).second->begin(); p != (*f).second->end(); p++){
44  ArgVar++;
45  pair< Expr, Expr > key = pair< Expr, Expr >((*f).first, (*p));
46  std::string NewName = NewBryantVar(VarTotal, ArgVar);
47  Expr value = d_core->newVar(NewName, TempType);
48  name_map.insert( *new pair< pair< Expr, Expr>, Expr >(key, value));
49  }
50  }
51 return name_map;
52 }
53 
54 
55 void ExprTransform::PredConstrainer(set<Expr>& Not_replaced_set, const Expr& e, const Expr& Pred, int location, B_name_map& name_map, set<Expr>& SeenBefore, set<Expr>& Constrained_set, T_generator_map& Constrained_map, set<Expr>& P_constrained_set) {
56  if (!SeenBefore.insert(e).second)
57  return;
58  if (e.isApply() && e.getOpKind() == UFUNC && !e.isTerm())
59  if (e.getOpExpr() == Pred.getOpExpr() && Pred[location] != e[location]) {
60 
61  Expr Temp0, Temp1;
62  if (e[location].isVar() || Not_replaced_set.find(e[location]) != Not_replaced_set.end())
63  Temp0 = e[location];
64  else Temp0 = name_map.find(pair<Expr, Expr>((e[location]).getOpExpr(),(e[location])))->second;
65  if (Pred[location].isVar())
66  Temp1 = Pred[location];
67  else Temp1 = name_map.find(pair<Expr, Expr>((Pred[location]).getOpExpr(),(Pred[location])))->second;
68  if (Constrained_set.find(e[location]) != Constrained_set.end()) {
69  Expr Eq = Temp0.eqExpr(Temp1);
70  Expr Reflexor = Temp1.eqExpr(Temp0);
71  Eq = Eq.notExpr();
72  Reflexor = Reflexor.notExpr();
73  if (P_constrained_set.find(Reflexor) == P_constrained_set.end())
74  P_constrained_set.insert(Eq);
75  }
76 
77 
78 
79  else {
80  if (Constrained_map.find(Pred[location]) == Constrained_map.end())
81  Constrained_map.insert(pair<Expr, set<Expr>*>(Pred[location], new set<Expr>));
82  Constrained_map[Pred[location]]->insert(Temp0);
83 
84  }
85  }
86 
87 
88 
89 
90  for (int l = 0; l < e.arity(); l++)
91  PredConstrainer(Not_replaced_set, e[l], Pred, location, name_map, SeenBefore, Constrained_set, Constrained_map, P_constrained_set);
92 }
93 
94 void ExprTransform::PredConstrainTester(set<Expr>& Not_replaced_set, const Expr& e, B_name_map& name_map, vector<Expr>& Pred_vec, set<Expr>& Constrained_set, set<Expr>& P_constrained_set, T_generator_map& Constrained_map) {
95  for (vector<Expr>::iterator i = Pred_vec.begin(); i != Pred_vec.end(); i++) {
96  for (int k = 0; k < (*i).arity(); k++)
97  if (Constrained_set.find((*i)[k]) != Constrained_set.end()){
98  set<Expr> SeenBefore;
99  PredConstrainer(Not_replaced_set, e, (*i), k, name_map, SeenBefore, Constrained_set, Constrained_map, P_constrained_set);
100  }
101  }
102 
103 }
104 
105 
106 
107 
108 
109 
110 Expr ExprTransform::ITE_generator(Expr& Orig, Expr& Value, B_Term_map& Creation_map, B_name_map& name_map,
111  T_ITE_map& ITE_map) {
112 
113  Expr NewITE;
114  for (vector<Expr>::reverse_iterator f = (Creation_map.find(Orig.getOpExpr())->second->rbegin());
115  f != (Creation_map.find(Orig.getOpExpr())->second->rend()); f++) {
116  if ((*f).getOpExpr() == Orig.getOpExpr()) {
117  Expr TempExpr;
118  for (int i = 0; i < Orig.arity(); i++) {
119  Expr TempEqExpr;
120  if ((*f)[i].isApply()) //(Orig[i].isApply())
121  TempEqExpr = ITE_map.find((*f)[i])->second;
122  else
123  TempEqExpr = (*f)[i]; // TempEqExpr = Orig[i];
124  if (Orig[i].isApply()) // ((*f)[i].isApply())
125  TempEqExpr = TempEqExpr.eqExpr(ITE_map.find(Orig[i])->second);
126  else
127  TempEqExpr = TempEqExpr.eqExpr(Orig[i]);
128  if (TempExpr.isNull() == true)
129  TempExpr = TempEqExpr;
130  else
131  TempExpr = TempExpr.andExpr(TempEqExpr);
132  }
133  if (NewITE.isNull() == true)
134  NewITE = TempExpr.iteExpr(name_map.find(pair<Expr, Expr>((*f).getOpExpr(),(*f)))->second, Value);
135  else {
136  Expr Temp = NewITE;
137  NewITE = TempExpr.iteExpr(name_map.find(pair<Expr, Expr>((*f).getOpExpr(),(*f)))->second, Temp);
138  }
139  }
140 
141  }
142 return NewITE;
143 }
144 
145 
146 
147 
148 
149 void ExprTransform::Get_ITEs(B_formula_map& instance_map, set<Expr>& Not_replaced_set, B_Term_map& P_term_map, T_ITE_vec& ITE_vec, B_Term_map& Creation_map,
150  B_name_map& name_map, T_ITE_map& ITE_map) {
151 
152  for (T_ITE_vec::iterator f = ITE_vec.begin(); f != ITE_vec.end(); f++) {
153  if (!(*f).isVar()) {
154  if (Creation_map.find((*f).getOpExpr()) == Creation_map.end()) {
155  Creation_map.insert(pair<Expr, vector<Expr>*> (
156  (*f).getOpExpr(), new vector<Expr> ()));
157  Creation_map[(*f).getOpExpr()]->push_back((*f));
158  if (instance_map[(*f).getOpExpr()] < LIMIT || !(*f).isTerm())
159  ITE_map.insert(pair<Expr, Expr> ((*f), name_map.find(pair<
160  Expr, Expr> ((*f).getOpExpr(), (*f)))->second));
161  else {
162  ITE_map.insert(pair<Expr, Expr> ((*f), (*f)));
163  Not_replaced_set.insert(*f);
164  }
165  } else {
166  if (instance_map[(*f).getOpExpr()] > LIMIT && (*f).isTerm()) {
167  ITE_map.insert(pair<Expr, Expr> ((*f), (*f)));
168  Creation_map[(*f).getOpExpr()]->push_back((*f));
169  Not_replaced_set.insert(*f);
170  } else {
171  Expr NewValue = name_map.find(pair<Expr, Expr> (
172  (*f).getOpExpr(), (*f)))->second;
173  Expr Add = ITE_generator((*f), NewValue, Creation_map,
174  name_map, ITE_map);
175  ITE_map.insert(pair<Expr, Expr> ((*f), Add));
176  Creation_map[(*f).getOpExpr()]->push_back((*f));
177  }
178  }
179  }
180  }
181 }
182 
183 
184 
185 void ExprTransform::RemoveFunctionApps(const Expr& orig, set<Expr>& Not_replaced_set, vector<Expr>& Old, vector<Expr>& New, T_ITE_map& ITE_map, set<Expr>& SeenBefore) {
186  if (!SeenBefore.insert( orig ).second)
187  return;
188 
189  for (int i = 0; i < orig.arity() ; i++)
190  RemoveFunctionApps(orig[i], Not_replaced_set, Old, New, ITE_map, SeenBefore);
191  if (orig.isApply() && orig.getOpKind() == UFUNC && Not_replaced_set.find(orig) != Not_replaced_set.end()) {
192  Old.push_back(orig);
193  New.push_back(ITE_map.find(orig)->second);
194  }
195 }
196 
197 
198 
199 void ExprTransform::GetSortedOpVec(B_Term_map& X_generator_map, B_Term_map& X_term_map, B_Term_map& P_term_map, set<Expr>& P_terms, set<Expr>& G_terms, set<Expr>& X_terms, vector<Expr>& sortedOps, set<Expr>& SeenBefore) {
200 
201  for (B_Term_map::iterator i = X_generator_map.begin(); i != X_generator_map.end(); i++) {
202 
203  for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++) {
204  if (P_terms.find(*j) != P_terms.end()) {
205  vector<Expr>::iterator k = j;
206  k++;
207  bool added = false;
208  for (; k != (*i).second->end(); k++) {
209  if (G_terms.find(*k) != G_terms.end() && !added) {
210  if (X_term_map.find((*j).getOpExpr()) == X_term_map.end())
211  X_term_map.insert(pair<Expr, vector<Expr>*>((*j).getOpExpr(), new vector<Expr>));
212  X_term_map[(*j).getOpExpr()]->push_back(*j);
213  X_terms.insert(*j);
214  added = true;
215 
216  }
217  }
218  }
219  }
220  }
221 
222 
223  set<int> sorted;
224  map<int, set<Expr>*> Opmap;
225  for (B_Term_map::iterator i = P_term_map.begin(); i != P_term_map.end(); i++) {
226  int count = 0;
227  for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++)
228  count++;
229  if (X_term_map.find((*i).first) != X_term_map.end()) {
230  for (vector<Expr>::iterator j = X_term_map[(*i).first]->begin(); j != X_term_map[(*i).first]->end(); j++)
231  count--;
232  }
233  if (Opmap.find(count) == Opmap.end())
234  Opmap.insert(pair<int, set<Expr>*>(count, new set<Expr>));
235  Opmap[count]->insert((*i).first);
236  sorted.insert(count);
237  }
238  vector<int> sortedvec;
239  for (set<int>::iterator i = sorted.begin(); i != sorted.end(); i++)
240  sortedvec.push_back(*i);
241  sort(sortedvec.begin(), sortedvec.end());
242 
243 
244  for (vector<int>::iterator i = sortedvec.begin(); i != sortedvec.end(); i++) {
245  for (set<Expr>::iterator j = Opmap[*i]->begin(); j != Opmap[*i]->end(); j++)
246  sortedOps.push_back(*j);
247  }
248 
249 
250 }
251 
252 void ExprTransform::GetFormulaMap(const Expr& e, set<Expr>& formula_map, set<Expr>& G_terms, int& size, int negations) {
253  if (e.isEq() && negations % 2 == 1)
254  formula_map.insert(e);
255  if (e.isNot())
256  negations++;
257  size++;
258  for (int i = 0; i < e.arity(); i++)
259  GetFormulaMap(e[i], formula_map, G_terms, size, negations);
260 }
261 
262 void ExprTransform::GetGTerms2(set<Expr>& formula_map, set<Expr>& G_terms) {
263 
264  for (set<Expr>::iterator i = formula_map.begin(); i != formula_map.end(); i++)
265  if ((*i)[0].isTerm())
266  for (int j = 0; j < 2; j++) {
267  G_terms.insert((*i)[j]);
268  }
269 }
270 
271 void ExprTransform::GetSub_vec(T_ITE_vec& ITE_vec, const Expr& e, set<Expr>& ITE_Added) {
272 
273  for (int i = 0; i < e.arity(); i++ )
274  GetSub_vec(ITE_vec, e[i], ITE_Added);
275  if (e.isTerm() && ITE_Added.insert(e).second)
276  ITE_vec.push_back(e);
277 }
278 
279 
280 
281 void ExprTransform::GetOrderedTerms(B_formula_map& instance_map, B_name_map& name_map, B_Term_map& X_term_map, T_ITE_vec& ITE_vec, set<Expr>& G_terms, set<Expr>& X_terms, vector<Expr>& Pred_vec, vector<Expr>& sortedOps, vector<Expr>& Constrained_vec, vector<Expr>& UnConstrained_vec, set<Expr>& Constrained_set, set<Expr>& UnConstrained_set, B_Term_map& G_term_map, B_Term_map& P_term_map, set<Expr>& SeenBefore, set<Expr>& ITE_Added) {
282 
283 
284  for (vector<Expr>::iterator i = sortedOps.begin(); i != sortedOps.end(); i++){
285  if (G_term_map.find(*i) != G_term_map.end()) {
286  for (vector<Expr>::iterator j = G_term_map[*i]->begin(); j != G_term_map[*i]->end(); j++)
287  GetSub_vec(ITE_vec,(*j), ITE_Added);
288  }
289  }
290  for (vector<Expr>::iterator i = sortedOps.begin(); i != sortedOps.end(); i++){
291  if (!P_term_map[*i]->empty()) {
292  for (vector<Expr>::iterator j = P_term_map[*i]->begin(); j != P_term_map[*i]->end(); j++)
293  GetSub_vec(ITE_vec, (*j), ITE_Added);
294  }
295  }
296  for (vector<Expr>::iterator i = ITE_vec.begin(); i != ITE_vec.end(); i++) {
297  if (G_terms.find(*i) != G_terms.end()) {
298  UnConstrained_set.insert(*i);
299  UnConstrained_vec.push_back(*i);
300  }
301  else if ((*i).isApply()) {
302  if (instance_map[(*i).getOpExpr()] > 40){
303  UnConstrained_set.insert(*i);
304  UnConstrained_vec.push_back(*i);
305  }
306  } else if (X_terms.find(*i) == X_terms.end()) {
307  Constrained_set.insert(*i);
308  Constrained_vec.push_back(*i);
309  }
310  else {
311  vector<Expr>::iterator j = i;
312  j = j + 1;
313  bool found = false;
314  for (; j != ITE_vec.end(); j++) {
315  if (!(*j).isVar())
316  if (G_terms.find(*j) != G_terms.end() && (*j).getOpExpr() == (*i).getOpExpr() && !found) {
317  UnConstrained_vec.push_back(*i);
318  UnConstrained_set.insert(*i);
319  j = ITE_vec.end();
320  j--;
321  found = true;
322  }
323  }
324  if (!found) {
325  Constrained_vec.push_back(*i);
326  Constrained_set.insert(*i);
327 
328  }
329 
330  }
331  }
332  for (vector<Expr>::iterator l = Pred_vec.begin(); l != Pred_vec.end(); l++)
333  ITE_vec.push_back(*l);
334 }
335 
336 
337 
338 
339 
340 
341 
342 void ExprTransform::BuildBryantMaps(const Expr& e, T_generator_map& generator_map, B_Term_map& X_generator_map,
343  B_type_map& type_map, vector<Expr>& Pred_vec, set<Expr>& P_terms, set<Expr>& G_terms,
344  B_Term_map& P_term_map, B_Term_map& G_term_map, set< Expr >& SeenBefore, set<Expr>& ITE_Added){
345  if ( !SeenBefore.insert( e ).second )
346  return;
347  if ( e.isApply() && e.getOpKind() == UFUNC){
348  type_map.insert(pair<Expr, Type>(e.getOpExpr(), e.getType()));
349  if ( generator_map.find( e.getOpExpr() ) == generator_map.end() )
350  generator_map.insert(pair< Expr, set<Expr>* >( e.getOpExpr(), new set<Expr>()));
351  generator_map[e.getOpExpr()]->insert(e);
352  }
353  if (e.isApply() && e.getOpKind() == UFUNC && !e.isTerm())
354  Pred_vec.push_back(e);
355  for ( int i = 0; i < e.arity(); i++ )
356  BuildBryantMaps(e[i], generator_map, X_generator_map, type_map, Pred_vec, P_terms, G_terms, P_term_map, G_term_map, SeenBefore, ITE_Added);
357 
358 
359  if (e.isTerm() && G_terms.find(e) == G_terms.end())
360  P_terms.insert(e);
361 
362  if (e.isTerm()) {
363  if (!e.isVar()) {
364  if (X_generator_map.find(e.getOpExpr()) == X_generator_map.end())
365  X_generator_map.insert(pair< Expr, vector<Expr>* >( e.getOpExpr(), new vector<Expr>()));
366  X_generator_map[e.getOpExpr()]->push_back(e);
367  }
368  if (ITE_Added.insert(e).second) {
369  if (G_terms.find(e) != G_terms.end()) {
370  if (e.isVar()) {
371  G_term_map.insert(pair<Expr, vector<Expr>*>(e, new vector<Expr>()));
372  P_term_map.insert(pair<Expr, vector<Expr>*>(e, new vector<Expr>()));
373  G_term_map[e]->push_back(e);
374 
375  }
376  else {
377  if (G_term_map.find(e.getOpExpr()) == G_term_map.end()) {
378  G_term_map.insert(pair<Expr, vector<Expr>*>(e.getOpExpr(), new vector<Expr>()));
379  P_term_map.insert(pair<Expr, vector<Expr>*>(e.getOpExpr(), new vector<Expr>()));
380  }
381  G_term_map[e.getOpExpr()]->push_back(e);
382  }
383  }
384  else {
385  if (e.isVar()) {
386  if (P_term_map.find(e) == P_term_map.end())
387  P_term_map.insert(pair<Expr, vector<Expr>*>(e, new vector<Expr>()));
388  P_term_map[e]->push_back(e);
389  }
390  else {
391  if (P_term_map.find(e.getOpExpr()) == P_term_map.end())
392  P_term_map.insert(pair<Expr, vector<Expr>*>(e.getOpExpr(), new vector<Expr>()));
393  P_term_map[e.getOpExpr()]->push_back(e);
394  }
395  }
396  }
397  }
398 return;
399 }
400 
401 void ExprTransform::GetPEqs(const Expr& e, B_name_map& name_map, set<Expr>& P_constrained_set, set<Expr>& Constrained_set, T_generator_map& Constrained_map, set<Expr>& SeenBefore) {
402  if (!SeenBefore.insert(e).second)
403  return;
404  if (e.isEq()) {
405  if (Constrained_set.find(e[1]) != Constrained_set.end()
406  && Constrained_set.find(e[0]) != Constrained_set.end()) {
407  Expr Temp0, Temp1;
408  if (e[0] != e[1]) {
409  if (e[0].isVar())
410  Temp0 = e[0];
411  else
412  Temp0 = name_map.find(pair<Expr, Expr> ((e[0]).getOpExpr(),
413  (e[0])))->second;
414  if (e[1].isVar())
415  Temp1 = e[1];
416  else
417  Temp1 = name_map.find(pair<Expr, Expr> ((e[1]).getOpExpr(),
418  (e[1])))->second;
419  Expr Eq = Temp0.eqExpr(Temp1);
420  Expr Reflexor = Temp1.eqExpr(Temp0);
421  Eq = Eq.notExpr();
422  Reflexor = Reflexor.notExpr();
423  if (P_constrained_set.find(Reflexor) == P_constrained_set.end())
424  P_constrained_set.insert(Eq);
425  }
426  } else if (Constrained_set.find(e[0]) != Constrained_set.end()) {
427  if (Constrained_map.find(e[0]) == Constrained_map.end())
428  Constrained_map.insert(pair<Expr, set<Expr>*> (e[0], new set<
429  Expr> ));
430  Constrained_map[e[0]]->insert(e[1]);
431  } else if (Constrained_set.find(e[1]) != Constrained_set.end()) {
432  if (Constrained_map.find(e[1]) == Constrained_map.end())
433  Constrained_map.insert(pair<Expr, set<Expr>*> (e[1], new set<
434  Expr> ));
435  Constrained_map[e[1]]->insert(e[0]);
436  }
437  }
438  for (int i = 0; i < e.arity(); i++)
439  GetPEqs(e[i], name_map, P_constrained_set, Constrained_set, Constrained_map, SeenBefore);
440 }
441 
442 Expr ExprTransform::ConstrainedConstraints(set<Expr>& Not_replaced_set, T_generator_map& Constrained_map, B_name_map& name_map, B_Term_map& Creation_map, set<Expr>& Constrained_set, set<Expr>& UnConstrained_set, set<Expr>& P_constrained_set) {
443  if (Constrained_set.empty())
444  return d_core->trueExpr();
445 
446 
447  for (T_generator_map::iterator f = Constrained_map.begin(); f != Constrained_map.end(); f++) {
448 
449  Expr Value;
450  if ((*f).first.isVar())
451  Value = (*f).first;
452  else
453  Value = name_map.find(pair<Expr, Expr>((*f).first.getOpExpr(),(*f).first))->second;
454  for (set<Expr>::iterator j = (*f).second->begin(); j != (*f).second->end(); j++) {
455  if (Value != (*j)) {
456  if ((*j).isVar() || Not_replaced_set.find(*j) != Not_replaced_set.end()){
457  Expr Temp = Value.eqExpr(*j);
458  Temp = Temp.notExpr();
459  P_constrained_set.insert(Temp);
460  }
461  else {
462  vector<Expr>::iterator c = Creation_map[(*j).getOpExpr()]->begin();
463  bool done = false;
464  while ( !done && c != Creation_map[(*j).getOpExpr()]->end() ) {
465  if ((*c) == (*j))
466  done = true;
467  Expr Temp = name_map.find(pair<Expr, Expr>((*c).getOpExpr(),(*c)))->second;
468  Expr TempEqExpr = Value.eqExpr(Temp);
469  TempEqExpr = TempEqExpr.notExpr();
470  if (!Value == Temp)
471  P_constrained_set.insert(TempEqExpr);
472  c++;
473  }
474  }
475 
476  }
477  }
478  }
479  if (P_constrained_set.empty())
480  return d_core->trueExpr();
481  else {
482  Expr Constraints = *(P_constrained_set.begin());
483  set<Expr>::iterator i = P_constrained_set.begin();
484  i++;
485  for (; i != P_constrained_set.end(); i++)
486  Constraints = Constraints.andExpr(*i);
487 
488  return Constraints;
489  }
490 }
491 
492 
493 void ExprTransform::GetOrdering(B_Term_map& X_generator_map, B_Term_map& G_term_map, B_Term_map& P_term_map) {
494 
495  for (B_Term_map::iterator i = X_generator_map.begin(); i != X_generator_map.end(); i++) {
496  map<int, vector<Expr>*> Order_map;
497  set<int> Order_set;
498  for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++) {
499  int temp = 0;
500  int Counter = CountSubTerms(*j, temp);
501  if (Order_map.find(Counter) == Order_map.end())
502  Order_map.insert(pair<int, vector<Expr>*>(Counter, new vector<Expr>));
503  Order_map[Counter]->push_back(*j);
504  Order_set.insert(Counter);
505  }
506  vector<int> Order_vec;
507  for (set<int>::iterator m = Order_set.begin(); m != Order_set.end(); m++)
508  Order_vec.push_back(*m);
509  (*i).second->clear();
510  sort(Order_vec.begin(), Order_vec.end());
511  for (vector<int>::iterator k = Order_vec.begin(); k != Order_vec.end(); k++)
512  for (vector<Expr>::iterator l = Order_map[*k]->begin(); l != Order_map[*k]->end(); l++){
513  (*i).second->push_back(*l);
514 
515  }
516  }
517 
518 for (B_Term_map::iterator i = G_term_map.begin(); i != G_term_map.end(); i++) {
519  map<int, vector<Expr>*> Order_map;
520  set<int> Order_set;
521  for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++) {
522  int temp = 0;
523  int Counter = CountSubTerms(*j, temp);
524  if (Order_map.find(Counter) == Order_map.end())
525  Order_map.insert(pair<int, vector<Expr>*>(Counter, new vector<Expr>));
526  Order_map[Counter]->push_back(*j);
527  Order_set.insert(Counter);
528  }
529  vector<int> Order_vec;
530  for (set<int>::iterator m = Order_set.begin(); m != Order_set.end(); m++)
531  Order_vec.push_back(*m);
532  (*i).second->clear();
533  sort(Order_vec.begin(), Order_vec.end());
534  for (vector<int>::iterator k = Order_vec.begin(); k != Order_vec.end(); k++)
535  for (vector<Expr>::iterator l = Order_map[*k]->begin(); l != Order_map[*k]->end(); l++){
536  (*i).second->push_back(*l);
537  }
538  }
539 
540 for (B_Term_map::iterator i = P_term_map.begin(); i != P_term_map.end(); i++) {
541  map<int, vector<Expr>*> Order_map;
542  set<int> Order_set;
543  for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++) {
544  int temp = 0;
545  int Counter = CountSubTerms(*j, temp);
546  if (Order_map.find(Counter) == Order_map.end())
547  Order_map.insert(pair<int, vector<Expr>*>(Counter, new vector<Expr>));
548  Order_map[Counter]->push_back(*j);
549  Order_set.insert(Counter);
550  }
551  vector<int> Order_vec;
552  for (set<int>::iterator m = Order_set.begin(); m != Order_set.end(); m++)
553  Order_vec.push_back(*m);
554  (*i).second->clear();
555  sort(Order_vec.begin(), Order_vec.end());
556  for (vector<int>::iterator k = Order_vec.begin(); k != Order_vec.end(); k++)
557  for (vector<Expr>::iterator l = Order_map[*k]->begin(); l != Order_map[*k]->end(); l++){
558  (*i).second->push_back(*l);
559  }
560  }
561 }
562 
563 void ExprTransform::B_Term_Map_Deleter(B_Term_map& Map) {
564  for (B_Term_map::iterator j = Map.begin(); j != Map.end(); j++)
565  delete (*j).second;
566 }
567 
568 void ExprTransform::T_generator_Map_Deleter(T_generator_map& Map) {
569  for (T_generator_map::iterator j = Map.begin(); j != Map.end(); j++)
570  delete (*j).second;
571 }
572 
573 Theorem ExprTransform::dobryant(const Expr& T){
574 
575  Expr U = T.notExpr();
576  set<Expr> P_terms, G_terms, X_terms, formula_1_map, Constrained_set, UnConstrained_set, P_constrained_set, UnConstrained_Pred_set, Not_replaced_set;
577  B_name_map name_map;
578  B_type_map type_map;
579  B_Term_map P_term_map, G_term_map, X_term_map, X_generator_map, Creation_map;
580  B_formula_map instance_map;
581  T_generator_map generator_map, Constrained_map;
582  T_ITE_vec ITE_vec;
583  T_ITE_map ITE_map;
584  int size = 0;
585  GetFormulaMap(U, formula_1_map, G_terms, size, 0);
586 
587 
588  GetGTerms2(formula_1_map, G_terms);
589  vector<Expr> sortedOps, Constrained_vec, UnConstrained_vec, Pred_vec;
590  set<Expr> SeenBefore1, ITE_Added1;
591  BuildBryantMaps(U, generator_map, X_generator_map, type_map, Pred_vec, P_terms, G_terms, P_term_map, G_term_map, SeenBefore1, ITE_Added1);
592  bool proceed = false;
593  for (T_generator_map::iterator i = generator_map.begin(); i != generator_map.end(); i++)
594  if ((*i).second->begin()->isTerm()) {
595 
596  int count = 0;
597  for (set<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++)
598  count++;
599  if (count <= LIMIT)
600  proceed = true;
601  instance_map.insert(pair<Expr, int>((*i).first, count));
602  }
603 
604 
605  if (!proceed)
606  return d_core->reflexivityRule(T);
607 
608 
609  GetOrdering(X_generator_map, G_term_map, P_term_map);
610  name_map = BryantNames(generator_map, type_map);
611  set<Expr> SeenBefore2;
612  GetSortedOpVec(X_generator_map, X_term_map, P_term_map, P_terms, G_terms, X_terms, sortedOps, SeenBefore2);
613  set<Expr> SeenBefore3, ITE_added3;
614  GetOrderedTerms(instance_map, name_map, X_term_map, ITE_vec, G_terms, X_terms, Pred_vec, sortedOps, Constrained_vec, UnConstrained_vec, Constrained_set, UnConstrained_set, G_term_map, P_term_map, SeenBefore3, ITE_added3);
615 
616 
617 
618 
619  //PredicateEliminator(U, Pred_vec, UnConstrained_Pred_set, name_map, ITE_map, Constrained_set);
620 
621  Get_ITEs(instance_map, Not_replaced_set, P_term_map, ITE_vec, Creation_map, name_map, ITE_map);
622 
623  set<Expr> SeenBefore4;
624  GetPEqs(U, name_map, P_constrained_set, Constrained_set, Constrained_map, SeenBefore4);
625 
626 
627  PredConstrainTester(Not_replaced_set, U, name_map, Pred_vec, Constrained_set, P_constrained_set, Constrained_map);
628 
629  Expr Constraints = ConstrainedConstraints(Not_replaced_set, Constrained_map, name_map, Creation_map, Constrained_set, UnConstrained_set, P_constrained_set);
630 
631  // Constraints.pprintnodag();
632  vector< Expr > Old;
633  vector< Expr > New;
634 
635 
636 
637 
638 
639 
640 
641  set<Expr> SeenBefore6;
642 
643  RemoveFunctionApps(U, Not_replaced_set, Old, New, ITE_map, SeenBefore6);
644  Expr Result = U.substExpr(Old, New);
645  Expr Final = Constraints.impExpr(Result);
646  Final = Final.notExpr();
647 
648 
649 
650 
651  B_Term_Map_Deleter(Creation_map);
652  B_Term_Map_Deleter(X_generator_map);
653  B_Term_Map_Deleter(X_term_map);
654  B_Term_Map_Deleter(G_term_map);
655  T_generator_Map_Deleter(Constrained_map);
656  T_generator_Map_Deleter(generator_map);
657 
658 
659  return d_rules->dummyTheorem(T.iffExpr(Final));
660 
661 
662 }
663 
664 
665 
666 
667 
668 
669