CVC3

bryant.cpp

Go to the documentation of this file.
00001 #include "vc.h"
00002 #include "expr_transform.h"
00003 #include "theory_core.h"
00004 #include "command_line_flags.h"
00005 #include "core_proof_rules.h"
00006 
00007 
00008 using namespace std;
00009 using namespace CVC3;
00010 
00011 
00012 const int LIMIT = 55;
00013 
00014 int ExprTransform::CountSubTerms(const Expr& e, int& counter) {
00015   if (e.arity() == 0)
00016     return 0;
00017   for (int i = 0; i < e.arity(); i++) {
00018          int count = CountSubTerms(e[i], counter) + 1;
00019        if (count > counter)
00020            counter = count;
00021       }
00022   return counter;
00023 }
00024 
00025 std::string ExprTransform::NewBryantVar(const int a, const int b){
00026   std::string S;
00027   std::stringstream out1, out2;
00028   out1 << a;
00029   out2 << b;
00030   std::string Tempvar = "A";
00031     S = Tempvar + out1.str() + "B" + out2.str();
00032   return S;
00033 }
00034 
00035 
00036 ExprTransform::B_name_map ExprTransform::BryantNames(T_generator_map& generator_map, B_type_map& type_map) {
00037   B_name_map name_map;
00038   int VarTotal = 0;
00039   for (T_generator_map::iterator f = generator_map.begin(); f != generator_map.end(); f++){
00040     VarTotal++;
00041     Type TempType = type_map.find((*f).first)->second;
00042     int ArgVar = 0;
00043     for (set< Expr >::iterator p = (*f).second->begin(); p != (*f).second->end(); p++){
00044       ArgVar++;
00045       pair< Expr, Expr > key = pair< Expr, Expr >((*f).first, (*p));
00046       std::string NewName = NewBryantVar(VarTotal, ArgVar);
00047       Expr value = d_core->newVar(NewName, TempType);
00048       name_map.insert( *new pair< pair< Expr, Expr>, Expr >(key, value));
00049     }
00050   }
00051 return name_map;
00052 }
00053 
00054 
00055 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) {
00056   if (!SeenBefore.insert(e).second)
00057     return;
00058   if (e.isApply() && e.getOpKind() == UFUNC && !e.isTerm())
00059   if (e.getOpExpr() == Pred.getOpExpr() && Pred[location] != e[location]) {
00060 
00061              Expr Temp0, Temp1;
00062        if (e[location].isVar() || Not_replaced_set.find(e[location]) != Not_replaced_set.end())
00063                       Temp0 = e[location];
00064        else Temp0 = name_map.find(pair<Expr, Expr>((e[location]).getOpExpr(),(e[location])))->second;
00065        if (Pred[location].isVar())
00066          Temp1 = Pred[location];
00067        else Temp1 = name_map.find(pair<Expr, Expr>((Pred[location]).getOpExpr(),(Pred[location])))->second;
00068        if (Constrained_set.find(e[location]) != Constrained_set.end()) {
00069                  Expr Eq = Temp0.eqExpr(Temp1);
00070            Expr Reflexor = Temp1.eqExpr(Temp0);
00071            Eq = Eq.notExpr();
00072            Reflexor = Reflexor.notExpr();
00073            if (P_constrained_set.find(Reflexor) == P_constrained_set.end())
00074                  P_constrained_set.insert(Eq);
00075            }
00076 
00077 
00078 
00079     else {
00080             if (Constrained_map.find(Pred[location]) == Constrained_map.end())
00081              Constrained_map.insert(pair<Expr, set<Expr>*>(Pred[location], new set<Expr>));
00082         Constrained_map[Pred[location]]->insert(Temp0);
00083 
00084     }
00085   }
00086 
00087 
00088 
00089 
00090     for (int l = 0; l < e.arity(); l++)
00091        PredConstrainer(Not_replaced_set, e[l], Pred, location, name_map, SeenBefore, Constrained_set, Constrained_map, P_constrained_set);
00092 }
00093 
00094 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) {
00095   for (vector<Expr>::iterator i = Pred_vec.begin(); i != Pred_vec.end(); i++) {
00096     for (int k = 0; k < (*i).arity(); k++)
00097       if (Constrained_set.find((*i)[k]) != Constrained_set.end()){
00098            set<Expr> SeenBefore;
00099            PredConstrainer(Not_replaced_set, e, (*i), k, name_map, SeenBefore, Constrained_set, Constrained_map, P_constrained_set);
00100       }
00101   }
00102 
00103 }
00104 
00105 
00106 
00107 
00108 
00109 
00110 Expr ExprTransform::ITE_generator(Expr& Orig, Expr& Value, B_Term_map& Creation_map, B_name_map& name_map,
00111                       T_ITE_map& ITE_map) {
00112 
00113     Expr NewITE;
00114   for (vector<Expr>::reverse_iterator f = (Creation_map.find(Orig.getOpExpr())->second->rbegin());
00115     f != (Creation_map.find(Orig.getOpExpr())->second->rend()); f++) {
00116       if ((*f).getOpExpr() == Orig.getOpExpr()) {
00117       Expr TempExpr;
00118       for (int i = 0;  i < Orig.arity(); i++) {
00119         Expr TempEqExpr;
00120           if ((*f)[i].isApply())  //(Orig[i].isApply())
00121           TempEqExpr = ITE_map.find((*f)[i])->second;
00122         else
00123           TempEqExpr = (*f)[i];  // TempEqExpr = Orig[i];
00124           if (Orig[i].isApply())     // ((*f)[i].isApply())
00125             TempEqExpr = TempEqExpr.eqExpr(ITE_map.find(Orig[i])->second);
00126         else
00127           TempEqExpr = TempEqExpr.eqExpr(Orig[i]);
00128           if (TempExpr.isNull() == true)
00129             TempExpr = TempEqExpr;
00130           else
00131             TempExpr = TempExpr.andExpr(TempEqExpr);
00132        }
00133   if (NewITE.isNull() == true)
00134       NewITE = TempExpr.iteExpr(name_map.find(pair<Expr, Expr>((*f).getOpExpr(),(*f)))->second, Value);
00135   else {
00136     Expr Temp = NewITE;
00137     NewITE = TempExpr.iteExpr(name_map.find(pair<Expr, Expr>((*f).getOpExpr(),(*f)))->second, Temp);
00138   }
00139   }
00140 
00141   }
00142 return NewITE;
00143 }
00144 
00145 
00146 
00147 
00148 
00149 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,
00150                 B_name_map& name_map, T_ITE_map& ITE_map) {
00151 
00152   for (T_ITE_vec::iterator f = ITE_vec.begin(); f != ITE_vec.end(); f++) {
00153     if (!(*f).isVar()) {
00154       if (Creation_map.find((*f).getOpExpr()) == Creation_map.end()) {
00155         Creation_map.insert(pair<Expr, vector<Expr>*> (
00156             (*f).getOpExpr(), new vector<Expr> ()));
00157         Creation_map[(*f).getOpExpr()]->push_back((*f));
00158         if (instance_map[(*f).getOpExpr()] < LIMIT || !(*f).isTerm())
00159           ITE_map.insert(pair<Expr, Expr> ((*f), name_map.find(pair<
00160               Expr, Expr> ((*f).getOpExpr(), (*f)))->second));
00161         else {
00162           ITE_map.insert(pair<Expr, Expr> ((*f), (*f)));
00163           Not_replaced_set.insert(*f);
00164         }
00165       } else {
00166         if (instance_map[(*f).getOpExpr()] > LIMIT && (*f).isTerm()) {
00167           ITE_map.insert(pair<Expr, Expr> ((*f), (*f)));
00168           Creation_map[(*f).getOpExpr()]->push_back((*f));
00169           Not_replaced_set.insert(*f);
00170         } else {
00171           Expr NewValue = name_map.find(pair<Expr, Expr> (
00172               (*f).getOpExpr(), (*f)))->second;
00173           Expr Add = ITE_generator((*f), NewValue, Creation_map,
00174               name_map, ITE_map);
00175           ITE_map.insert(pair<Expr, Expr> ((*f), Add));
00176           Creation_map[(*f).getOpExpr()]->push_back((*f));
00177         }
00178       }
00179     }
00180   }
00181 }
00182 
00183 
00184 
00185 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) {
00186   if (!SeenBefore.insert( orig ).second)
00187     return;
00188 
00189   for (int i = 0; i < orig.arity() ; i++)
00190     RemoveFunctionApps(orig[i], Not_replaced_set, Old, New, ITE_map, SeenBefore);
00191     if (orig.isApply() && orig.getOpKind() == UFUNC && Not_replaced_set.find(orig) != Not_replaced_set.end()) {
00192     Old.push_back(orig);
00193     New.push_back(ITE_map.find(orig)->second);
00194   }
00195 }
00196 
00197 
00198 
00199 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) {
00200 
00201   for (B_Term_map::iterator i = X_generator_map.begin(); i != X_generator_map.end(); i++) {
00202 
00203     for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++) {
00204       if (P_terms.find(*j) != P_terms.end()) {
00205         vector<Expr>::iterator k = j;
00206             k++;
00207           bool added = false;
00208         for (; k != (*i).second->end(); k++) {
00209           if (G_terms.find(*k) != G_terms.end() && !added) {
00210             if (X_term_map.find((*j).getOpExpr()) == X_term_map.end())
00211               X_term_map.insert(pair<Expr, vector<Expr>*>((*j).getOpExpr(), new vector<Expr>));
00212               X_term_map[(*j).getOpExpr()]->push_back(*j);
00213               X_terms.insert(*j);
00214               added = true;
00215 
00216           }
00217         }
00218       }
00219     }
00220   }
00221 
00222 
00223   set<int> sorted;
00224   map<int, set<Expr>*> Opmap;
00225   for (B_Term_map::iterator i = P_term_map.begin(); i != P_term_map.end(); i++) {
00226     int count = 0;
00227     for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++)
00228           count++;
00229     if (X_term_map.find((*i).first) != X_term_map.end()) {
00230     for (vector<Expr>::iterator j = X_term_map[(*i).first]->begin(); j != X_term_map[(*i).first]->end(); j++)
00231           count--;
00232     }
00233     if (Opmap.find(count) == Opmap.end())
00234       Opmap.insert(pair<int, set<Expr>*>(count, new set<Expr>));
00235     Opmap[count]->insert((*i).first);
00236     sorted.insert(count);
00237   }
00238   vector<int> sortedvec;
00239   for (set<int>::iterator i = sorted.begin(); i != sorted.end(); i++)
00240          sortedvec.push_back(*i);
00241     sort(sortedvec.begin(), sortedvec.end());
00242 
00243 
00244   for (vector<int>::iterator i = sortedvec.begin(); i != sortedvec.end(); i++) {
00245     for (set<Expr>::iterator j = Opmap[*i]->begin(); j != Opmap[*i]->end(); j++)
00246       sortedOps.push_back(*j);
00247   }
00248 
00249 
00250 }
00251 
00252 void ExprTransform::GetFormulaMap(const Expr& e, set<Expr>& formula_map, set<Expr>& G_terms, int& size, int negations) {
00253     if (e.isEq() && negations % 2 == 1)
00254          formula_map.insert(e);
00255     if (e.isNot())
00256        negations++;
00257         size++;
00258     for (int i = 0; i < e.arity(); i++)
00259     GetFormulaMap(e[i], formula_map, G_terms, size, negations);
00260 }
00261 
00262 void ExprTransform::GetGTerms2(set<Expr>& formula_map, set<Expr>& G_terms) {
00263 
00264   for (set<Expr>::iterator i = formula_map.begin(); i != formula_map.end(); i++)
00265     if ((*i)[0].isTerm())
00266       for (int j = 0; j < 2; j++)  {
00267          G_terms.insert((*i)[j]);
00268       }
00269 }
00270 
00271 void ExprTransform::GetSub_vec(T_ITE_vec& ITE_vec, const Expr& e, set<Expr>& ITE_Added) {
00272 
00273    for (int i = 0; i < e.arity(); i++ )
00274     GetSub_vec(ITE_vec, e[i], ITE_Added);
00275    if (e.isTerm() && ITE_Added.insert(e).second)
00276          ITE_vec.push_back(e);
00277 }
00278 
00279 
00280 
00281 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) {
00282 
00283 
00284   for (vector<Expr>::iterator i = sortedOps.begin(); i != sortedOps.end(); i++){
00285     if (G_term_map.find(*i) != G_term_map.end()) {
00286       for (vector<Expr>::iterator j = G_term_map[*i]->begin(); j != G_term_map[*i]->end(); j++)
00287         GetSub_vec(ITE_vec,(*j), ITE_Added);
00288     }
00289   }
00290   for (vector<Expr>::iterator i = sortedOps.begin(); i != sortedOps.end(); i++){
00291     if (!P_term_map[*i]->empty()) {
00292       for (vector<Expr>::iterator j = P_term_map[*i]->begin(); j != P_term_map[*i]->end(); j++)
00293                 GetSub_vec(ITE_vec, (*j), ITE_Added);
00294     }
00295      }
00296   for (vector<Expr>::iterator i = ITE_vec.begin(); i != ITE_vec.end(); i++) {
00297     if (G_terms.find(*i) != G_terms.end()) {
00298       UnConstrained_set.insert(*i);
00299       UnConstrained_vec.push_back(*i);
00300     }
00301     else if ((*i).isApply()) {
00302       if (instance_map[(*i).getOpExpr()] > 40){
00303         UnConstrained_set.insert(*i);
00304             UnConstrained_vec.push_back(*i);
00305       }
00306     } else if (X_terms.find(*i) == X_terms.end()) {
00307       Constrained_set.insert(*i);
00308       Constrained_vec.push_back(*i);
00309     }
00310     else {
00311       vector<Expr>::iterator j = i;
00312       j = j + 1;
00313       bool found = false;
00314       for (; j != ITE_vec.end(); j++) {
00315         if (!(*j).isVar())
00316             if (G_terms.find(*j) != G_terms.end() && (*j).getOpExpr() == (*i).getOpExpr() && !found) {
00317               UnConstrained_vec.push_back(*i);
00318               UnConstrained_set.insert(*i);
00319             j = ITE_vec.end();
00320               j--;
00321               found = true;
00322             }
00323       }
00324       if (!found) {
00325         Constrained_vec.push_back(*i);
00326           Constrained_set.insert(*i);
00327 
00328       }
00329 
00330     }
00331   }
00332     for (vector<Expr>::iterator l = Pred_vec.begin(); l != Pred_vec.end(); l++)
00333     ITE_vec.push_back(*l);
00334 }
00335 
00336 
00337 
00338 
00339 
00340 
00341 
00342 void ExprTransform::BuildBryantMaps(const Expr& e, T_generator_map& generator_map, B_Term_map& X_generator_map,
00343                   B_type_map& type_map, vector<Expr>& Pred_vec, set<Expr>& P_terms, set<Expr>& G_terms,
00344                   B_Term_map& P_term_map, B_Term_map& G_term_map, set< Expr >& SeenBefore, set<Expr>& ITE_Added){
00345   if ( !SeenBefore.insert( e ).second )
00346     return;
00347   if ( e.isApply() && e.getOpKind() == UFUNC){
00348     type_map.insert(pair<Expr, Type>(e.getOpExpr(), e.getType()));
00349   if ( generator_map.find( e.getOpExpr() ) == generator_map.end() )
00350       generator_map.insert(pair< Expr, set<Expr>* >( e.getOpExpr(), new set<Expr>()));
00351     generator_map[e.getOpExpr()]->insert(e);
00352   }
00353   if (e.isApply() && e.getOpKind() == UFUNC && !e.isTerm())
00354     Pred_vec.push_back(e);
00355   for ( int i = 0; i < e.arity(); i++ )
00356     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);
00357 
00358 
00359   if (e.isTerm() && G_terms.find(e) == G_terms.end())
00360     P_terms.insert(e);
00361 
00362     if (e.isTerm()) {
00363     if (!e.isVar()) {
00364         if (X_generator_map.find(e.getOpExpr()) == X_generator_map.end())
00365           X_generator_map.insert(pair< Expr, vector<Expr>* >( e.getOpExpr(), new vector<Expr>()));
00366       X_generator_map[e.getOpExpr()]->push_back(e);
00367     }
00368     if (ITE_Added.insert(e).second) {
00369         if (G_terms.find(e) != G_terms.end()) {
00370           if (e.isVar()) {
00371             G_term_map.insert(pair<Expr, vector<Expr>*>(e, new vector<Expr>()));
00372             P_term_map.insert(pair<Expr, vector<Expr>*>(e, new vector<Expr>()));
00373             G_term_map[e]->push_back(e);
00374 
00375           }
00376           else {
00377             if (G_term_map.find(e.getOpExpr()) == G_term_map.end()) {
00378                 G_term_map.insert(pair<Expr, vector<Expr>*>(e.getOpExpr(), new vector<Expr>()));
00379               P_term_map.insert(pair<Expr, vector<Expr>*>(e.getOpExpr(), new vector<Expr>()));
00380             }
00381                         G_term_map[e.getOpExpr()]->push_back(e);
00382             }
00383         }
00384         else {
00385           if (e.isVar()) {
00386             if (P_term_map.find(e) == P_term_map.end())
00387                P_term_map.insert(pair<Expr, vector<Expr>*>(e, new vector<Expr>()));
00388             P_term_map[e]->push_back(e);
00389           }
00390           else {
00391             if (P_term_map.find(e.getOpExpr()) == P_term_map.end())
00392                P_term_map.insert(pair<Expr, vector<Expr>*>(e.getOpExpr(), new vector<Expr>()));
00393               P_term_map[e.getOpExpr()]->push_back(e);
00394           }
00395         }
00396       }
00397     }
00398 return;
00399 }
00400 
00401 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) {
00402     if (!SeenBefore.insert(e).second)
00403       return;
00404   if (e.isEq()) {
00405     if (Constrained_set.find(e[1]) != Constrained_set.end()
00406         && Constrained_set.find(e[0]) != Constrained_set.end()) {
00407       Expr Temp0, Temp1;
00408       if (e[0] != e[1]) {
00409         if (e[0].isVar())
00410           Temp0 = e[0];
00411         else
00412           Temp0 = name_map.find(pair<Expr, Expr> ((e[0]).getOpExpr(),
00413               (e[0])))->second;
00414         if (e[1].isVar())
00415           Temp1 = e[1];
00416         else
00417           Temp1 = name_map.find(pair<Expr, Expr> ((e[1]).getOpExpr(),
00418               (e[1])))->second;
00419         Expr Eq = Temp0.eqExpr(Temp1);
00420         Expr Reflexor = Temp1.eqExpr(Temp0);
00421         Eq = Eq.notExpr();
00422         Reflexor = Reflexor.notExpr();
00423         if (P_constrained_set.find(Reflexor) == P_constrained_set.end())
00424           P_constrained_set.insert(Eq);
00425       }
00426     } else if (Constrained_set.find(e[0]) != Constrained_set.end()) {
00427       if (Constrained_map.find(e[0]) == Constrained_map.end())
00428         Constrained_map.insert(pair<Expr, set<Expr>*> (e[0], new set<
00429             Expr> ));
00430       Constrained_map[e[0]]->insert(e[1]);
00431     } else if (Constrained_set.find(e[1]) != Constrained_set.end()) {
00432       if (Constrained_map.find(e[1]) == Constrained_map.end())
00433         Constrained_map.insert(pair<Expr, set<Expr>*> (e[1], new set<
00434             Expr> ));
00435       Constrained_map[e[1]]->insert(e[0]);
00436     }
00437   }
00438   for (int i = 0; i < e.arity(); i++)
00439      GetPEqs(e[i], name_map, P_constrained_set, Constrained_set, Constrained_map, SeenBefore);
00440 }
00441 
00442 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) {
00443   if (Constrained_set.empty())
00444     return d_core->trueExpr();
00445 
00446 
00447   for (T_generator_map::iterator f = Constrained_map.begin(); f != Constrained_map.end(); f++) {
00448 
00449               Expr Value;
00450     if ((*f).first.isVar())
00451       Value = (*f).first;
00452     else
00453       Value = name_map.find(pair<Expr, Expr>((*f).first.getOpExpr(),(*f).first))->second;
00454       for (set<Expr>::iterator j = (*f).second->begin(); j != (*f).second->end(); j++) {
00455              if (Value != (*j)) {
00456                             if ((*j).isVar() || Not_replaced_set.find(*j) != Not_replaced_set.end()){
00457           Expr Temp = Value.eqExpr(*j);
00458           Temp = Temp.notExpr();
00459           P_constrained_set.insert(Temp);
00460         }
00461         else {
00462         vector<Expr>::iterator c = Creation_map[(*j).getOpExpr()]->begin();
00463         bool done = false;
00464         while ( !done && c != Creation_map[(*j).getOpExpr()]->end() ) {
00465           if ((*c) == (*j))
00466             done = true;
00467           Expr Temp = name_map.find(pair<Expr, Expr>((*c).getOpExpr(),(*c)))->second;
00468           Expr TempEqExpr = Value.eqExpr(Temp);
00469           TempEqExpr = TempEqExpr.notExpr();
00470           if (!Value == Temp)
00471                        P_constrained_set.insert(TempEqExpr);
00472           c++;
00473           }
00474         }
00475 
00476       }
00477     }
00478   }
00479   if (P_constrained_set.empty())
00480     return d_core->trueExpr();
00481   else {
00482   Expr Constraints = *(P_constrained_set.begin());
00483   set<Expr>::iterator i = P_constrained_set.begin();
00484   i++;
00485   for (; i != P_constrained_set.end(); i++)
00486          Constraints = Constraints.andExpr(*i);
00487 
00488     return Constraints;
00489   }
00490 }
00491 
00492 
00493 void ExprTransform::GetOrdering(B_Term_map& X_generator_map, B_Term_map& G_term_map, B_Term_map& P_term_map) {
00494 
00495   for (B_Term_map::iterator i = X_generator_map.begin(); i != X_generator_map.end(); i++) {
00496     map<int, vector<Expr>*> Order_map;
00497     set<int> Order_set;
00498     for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++) {
00499       int temp = 0;
00500       int Counter = CountSubTerms(*j, temp);
00501       if (Order_map.find(Counter) == Order_map.end())
00502                 Order_map.insert(pair<int, vector<Expr>*>(Counter, new vector<Expr>));
00503       Order_map[Counter]->push_back(*j);
00504       Order_set.insert(Counter);
00505     }
00506     vector<int> Order_vec;
00507     for (set<int>::iterator m = Order_set.begin(); m != Order_set.end(); m++)
00508             Order_vec.push_back(*m);
00509     (*i).second->clear();
00510     sort(Order_vec.begin(), Order_vec.end());
00511     for (vector<int>::iterator k = Order_vec.begin(); k != Order_vec.end(); k++)
00512       for (vector<Expr>::iterator l = Order_map[*k]->begin(); l != Order_map[*k]->end(); l++){
00513         (*i).second->push_back(*l);
00514 
00515       }
00516   }
00517 
00518 for (B_Term_map::iterator i = G_term_map.begin(); i != G_term_map.end(); i++) {
00519     map<int, vector<Expr>*> Order_map;
00520     set<int> Order_set;
00521     for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++) {
00522       int temp = 0;
00523       int Counter = CountSubTerms(*j, temp);
00524       if (Order_map.find(Counter) == Order_map.end())
00525                 Order_map.insert(pair<int, vector<Expr>*>(Counter, new vector<Expr>));
00526       Order_map[Counter]->push_back(*j);
00527       Order_set.insert(Counter);
00528     }
00529     vector<int> Order_vec;
00530     for (set<int>::iterator m = Order_set.begin(); m != Order_set.end(); m++)
00531             Order_vec.push_back(*m);
00532     (*i).second->clear();
00533     sort(Order_vec.begin(), Order_vec.end());
00534     for (vector<int>::iterator k = Order_vec.begin(); k != Order_vec.end(); k++)
00535       for (vector<Expr>::iterator l = Order_map[*k]->begin(); l != Order_map[*k]->end(); l++){
00536         (*i).second->push_back(*l);
00537       }
00538   }
00539 
00540 for (B_Term_map::iterator i = P_term_map.begin(); i != P_term_map.end(); i++) {
00541     map<int, vector<Expr>*> Order_map;
00542     set<int> Order_set;
00543     for (vector<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++) {
00544       int temp = 0;
00545       int Counter = CountSubTerms(*j, temp);
00546       if (Order_map.find(Counter) == Order_map.end())
00547                 Order_map.insert(pair<int, vector<Expr>*>(Counter, new vector<Expr>));
00548       Order_map[Counter]->push_back(*j);
00549       Order_set.insert(Counter);
00550     }
00551     vector<int> Order_vec;
00552     for (set<int>::iterator m = Order_set.begin(); m != Order_set.end(); m++)
00553             Order_vec.push_back(*m);
00554     (*i).second->clear();
00555     sort(Order_vec.begin(), Order_vec.end());
00556     for (vector<int>::iterator k = Order_vec.begin(); k != Order_vec.end(); k++)
00557       for (vector<Expr>::iterator l = Order_map[*k]->begin(); l != Order_map[*k]->end(); l++){
00558         (*i).second->push_back(*l);
00559       }
00560   }
00561 }
00562 
00563 void ExprTransform::B_Term_Map_Deleter(B_Term_map& Map) {
00564   for (B_Term_map::iterator j = Map.begin(); j != Map.end(); j++)
00565       delete (*j).second;
00566 }
00567 
00568 void ExprTransform::T_generator_Map_Deleter(T_generator_map& Map) {
00569   for (T_generator_map::iterator j = Map.begin(); j != Map.end(); j++)
00570     delete (*j).second;
00571 }
00572 
00573 Theorem ExprTransform::dobryant(const Expr& T){
00574 
00575   Expr U = T.notExpr();
00576   set<Expr> P_terms, G_terms, X_terms, formula_1_map, Constrained_set, UnConstrained_set, P_constrained_set, UnConstrained_Pred_set, Not_replaced_set;
00577   B_name_map name_map;
00578   B_type_map type_map;
00579   B_Term_map P_term_map, G_term_map, X_term_map, X_generator_map, Creation_map;
00580   B_formula_map instance_map;
00581   T_generator_map generator_map, Constrained_map;
00582   T_ITE_vec ITE_vec;
00583   T_ITE_map ITE_map;
00584   int size = 0;
00585   GetFormulaMap(U, formula_1_map, G_terms, size, 0);
00586 
00587 
00588   GetGTerms2(formula_1_map, G_terms);
00589   vector<Expr> sortedOps, Constrained_vec, UnConstrained_vec, Pred_vec;
00590   set<Expr> SeenBefore1, ITE_Added1;
00591   BuildBryantMaps(U, generator_map, X_generator_map, type_map, Pred_vec, P_terms, G_terms, P_term_map, G_term_map, SeenBefore1, ITE_Added1);
00592   bool proceed = false;
00593   for (T_generator_map::iterator i = generator_map.begin(); i != generator_map.end(); i++)
00594   if ((*i).second->begin()->isTerm()) {
00595 
00596               int count = 0;
00597       for (set<Expr>::iterator j = (*i).second->begin(); j != (*i).second->end(); j++)
00598       count++;
00599       if (count <= LIMIT)
00600               proceed = true;
00601            instance_map.insert(pair<Expr, int>((*i).first, count));
00602   }
00603 
00604 
00605        if (!proceed)
00606          return d_core->reflexivityRule(T);
00607 
00608 
00609   GetOrdering(X_generator_map, G_term_map, P_term_map);
00610   name_map = BryantNames(generator_map, type_map);
00611   set<Expr> SeenBefore2;
00612   GetSortedOpVec(X_generator_map, X_term_map, P_term_map, P_terms, G_terms, X_terms, sortedOps, SeenBefore2);
00613   set<Expr> SeenBefore3, ITE_added3;
00614   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);
00615 
00616 
00617 
00618 
00619   //PredicateEliminator(U, Pred_vec, UnConstrained_Pred_set, name_map, ITE_map, Constrained_set);
00620 
00621   Get_ITEs(instance_map, Not_replaced_set, P_term_map, ITE_vec, Creation_map, name_map, ITE_map);
00622 
00623   set<Expr> SeenBefore4;
00624   GetPEqs(U, name_map, P_constrained_set, Constrained_set, Constrained_map, SeenBefore4);
00625 
00626 
00627       PredConstrainTester(Not_replaced_set, U, name_map, Pred_vec, Constrained_set, P_constrained_set, Constrained_map);
00628 
00629   Expr Constraints = ConstrainedConstraints(Not_replaced_set, Constrained_map, name_map, Creation_map, Constrained_set, UnConstrained_set, P_constrained_set);
00630 
00631         //       Constraints.pprintnodag();
00632   vector< Expr > Old;
00633   vector< Expr > New;
00634 
00635 
00636 
00637 
00638 
00639 
00640 
00641   set<Expr> SeenBefore6;
00642 
00643   RemoveFunctionApps(U, Not_replaced_set, Old, New, ITE_map, SeenBefore6);
00644   Expr Result = U.substExpr(Old, New);
00645   Expr Final = Constraints.impExpr(Result);
00646   Final = Final.notExpr();
00647 
00648 
00649 
00650 
00651      B_Term_Map_Deleter(Creation_map);
00652      B_Term_Map_Deleter(X_generator_map);
00653        B_Term_Map_Deleter(X_term_map);
00654      B_Term_Map_Deleter(G_term_map);
00655        T_generator_Map_Deleter(Constrained_map);
00656      T_generator_Map_Deleter(generator_map);
00657 
00658 
00659        return d_rules->dummyTheorem(T.iffExpr(Final));
00660 
00661 
00662 }
00663 
00664 
00665 
00666 
00667 
00668 
00669