theory_quant.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*! 
00003  * \file theory_quant.cpp
00004  * 
00005  * Author: Daniel Wichs, Yeting Ge
00006  * 
00007  * Created: Wednesday July 2, 2003
00008  * 
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 #include "theory_quant.h"
00021 #include "theory_arith.h"
00022 #include "theory_array.h"
00023 #include "typecheck_exception.h"
00024 #include "parser_exception.h"
00025 #include "smtlib_exception.h"
00026 #include "quant_proof_rules.h"
00027 #include "theory_core.h"
00028 #include "command_line_flags.h"
00029 #include "vcl.h"
00030 #include<string>
00031 #include<string.h>
00032 #include <algorithm>
00033 using namespace std;
00034 using namespace CVC3;
00035 
00036 ///////////////////////////////////////////////////////////////////////////////
00037 // TheoryQuant Public Methods                                                 //
00038 ///////////////////////////////////////////////////////////////////////////////
00039 
00040 static const Expr null_expr;
00041 const int FOUND_FALSE = 1;
00042 
00043 Trigger::Trigger(TheoryCore* core, Expr e, Polarity pol, std::set<Expr> boundVars){
00044   trig=e ;
00045   polarity=pol;
00046   head=null_expr;
00047   hasRWOp=false;
00048   hasTrans=false;
00049   hasT2=false;
00050   isSimple=false;
00051   isSuperSimple=false;
00052   isMulti=false;
00053   multiIndex = 99999;
00054   multiId = 99999;
00055   for(std::set<Expr>::const_iterator i=boundVars.begin(),iend=boundVars.end(); i!=iend; ++i)
00056     bvs.push_back(*i);
00057 }
00058 
00059 bool Trigger::isPos(){
00060   return (Pos==polarity||PosNeg==polarity);
00061 }
00062 
00063 bool Trigger::isNeg(){
00064   return (Neg==polarity || PosNeg==polarity);
00065 }
00066 
00067 std::vector<Expr> Trigger::getBVs(){
00068   return bvs;
00069 }
00070 
00071 Expr Trigger::getEx(){
00072   return trig;
00073 }
00074 
00075 void Trigger::setHead(Expr h){
00076   head=h; 
00077 }
00078 
00079 Expr Trigger::getHead(){
00080   return head;
00081 }
00082 
00083 void Trigger::setRWOp(bool b){
00084   hasRWOp =b ; 
00085 }
00086 
00087 bool Trigger::hasRW(){
00088   return hasRWOp;
00089 }
00090 
00091 void Trigger::setTrans(bool b){
00092   hasTrans =b ; 
00093 }
00094 
00095 bool Trigger::hasTr(){
00096   return hasTrans;
00097 }
00098 
00099 void Trigger::setTrans2(bool b){
00100   hasT2 =b ; 
00101 }
00102 
00103 bool Trigger::hasTr2(){
00104   return hasT2;
00105 }
00106 
00107 void Trigger::setSimp(){
00108   isSimple =true ; 
00109 }
00110 
00111 bool Trigger::isSimp(){
00112   return isSimple;
00113 }
00114 
00115 void Trigger::setSuperSimp(){
00116   isSuperSimple =true ; 
00117 }
00118 
00119 bool Trigger::isSuperSimp(){
00120   return isSuperSimple;
00121 }
00122 
00123 void Trigger::setMultiTrig(){
00124   isMulti = true ; 
00125 }
00126 
00127 bool Trigger::isMultiTrig(){
00128   return isMulti;
00129 }
00130 
00131 
00132 dynTrig::dynTrig(Trigger t, ExprMap<Expr> b, size_t id)
00133   :trig(t),
00134    univ_id(id),
00135    binds(b)
00136 {}
00137 
00138 TheoryQuant::TheoryQuant(TheoryCore* core) //!< Constructor
00139   : Theory(core, "Quantified Expressions"),
00140     d_univs(core->getCM()->getCurrentContext()),    
00141     d_rawUnivs(core->getCM()->getCurrentContext()),    
00142     d_arrayTrigs(core->getCM()->getCurrentContext()),    
00143     d_lastArrayPos(core->getCM()->getCurrentContext(), 0 , 0),    
00144     d_lastPredsPos(core->getCM()->getCurrentContext(), 0, 0),
00145     d_lastTermsPos(core->getCM()->getCurrentContext(), 0, 0),
00146     d_lastPartPredsPos(core->getCM()->getCurrentContext(), 0, 0),
00147     d_lastPartTermsPos(core->getCM()->getCurrentContext(), 0, 0),
00148     d_univsPartSavedPos(core->getCM()->getCurrentContext(), 0, 0),
00149     d_lastPartLevel(core->getCM()->getCurrentContext(), 0, 0),
00150     d_usefulGterms(core->getCM()->getCurrentContext()),
00151     d_lastUsefulGtermsPos(core->getCM()->getCurrentContext(), 0, 0),
00152     d_savedTermsPos(core->getCM()->getCurrentContext(), 0, 0),
00153     d_univsSavedPos(core->getCM()->getCurrentContext(), 0, 0),
00154     d_rawUnivsSavedPos(core->getCM()->getCurrentContext(), 0, 0),
00155     d_univsPosFull(core->getCM()->getCurrentContext(), 0, 0),
00156     d_univsContextPos(core->getCM()->getCurrentContext(), 0, 0),
00157     d_instCount(core->getCM()->getCurrentContext(), 0,0),
00158     d_contextTerms(core->getCM()->getCurrentContext()),
00159     d_contextCache(core->getCM()->getCurrentContext()),
00160     d_maxQuantInst(&(core->getFlags()["max-quant-inst"].getInt())),
00161     d_useNew(&(core->getFlags()["quant-new"].getBool())),
00162     d_useLazyInst(&(core->getFlags()["quant-lazy"].getBool())),
00163     d_useSemMatch(&(core->getFlags()["quant-sem-match"].getBool())),
00164     d_useAtomSem(&(core->getFlags()["quant-const-match"].getBool())),
00165     d_translate(&(core->getFlags()["translate"].getBool())),
00166     d_useTrigNew(&(core->getFlags()["quant-trig-new"].getBool())),
00167     d_usePart(&(core->getFlags()["quant-inst-part"].getBool())),
00168     d_useMult(&(core->getFlags()["quant-inst-mult"].getBool())),
00169     d_useInstEnd(&(core->getFlags()["quant-inst-end"].getBool())),
00170     d_useInstLCache(&(core->getFlags()["quant-inst-lcache"].getBool())),
00171     d_useInstGCache(&(core->getFlags()["quant-inst-gcache"].getBool())),
00172     d_useInstTrue(&(core->getFlags()["quant-inst-true"].getBool())),
00173     d_usePullVar(&(core->getFlags()["quant-pullvar"].getBool())),
00174     d_useExprScore(&(core->getFlags()["quant-score"].getBool())),
00175     d_useTrigLoop(&(core->getFlags()["quant-trig-loop"].getInt())),
00176     d_maxInst(&(core->getFlags()["quant-max-inst"].getInt())),
00177     d_useTrans(&(core->getFlags()["quant-trans3"].getBool())),
00178     d_useTrans2(&(core->getFlags()["quant-trans2"].getBool())),
00179     d_useInstAll(&(core->getFlags()["quant-inst-all"].getBool())),
00180     d_usePolarity(&(core->getFlags()["quant-polarity"].getBool())),
00181     d_useEqu(&(core->getFlags()["quant-equ"].getBool())),
00182     d_maxNaiveCall(&(core->getFlags()["quant-naive-num"].getInt())),
00183     d_curMaxExprScore(core->getCM()->getCurrentContext(), (core->getFlags()["quant-max-score"].getInt()),0),
00184     d_arrayIndic(core->getCM()->getCurrentContext()),
00185     d_exprLastUpdatedPos(core->getCM()->getCurrentContext(),0 ,0),
00186     d_trans_found(core->getCM()->getCurrentContext()),
00187     d_trans2_found(core->getCM()->getCurrentContext()),
00188     null_cdlist(core->getCM()->getCurrentContext()),
00189     d_eqs(core->getCM()->getCurrentContext()),
00190     d_eqs_pos(core->getCM()->getCurrentContext(), 0, 0),
00191     d_allInstCount(core->getStatistics().counter("quantifier instantiations")),
00192     d_partCalled(core->getCM()->getCurrentContext(),false,0),
00193     d_instHistory(core->getCM()->getCurrentContext()),
00194     d_alltrig_list(core->getCM()->getCurrentContext())
00195 {
00196   IF_DEBUG(d_univs.setName("CDList[TheoryQuant::d_univs]"));
00197   vector<int> kinds;
00198   d_instCount = 0;
00199   d_cacheThmPos=0;
00200   d_trans_num=0;
00201   d_trans2_num=0;
00202   d_rules=createProofRules();
00203   kinds.push_back(EXISTS);
00204   kinds.push_back(FORALL);
00205   registerTheory(this, kinds);
00206   d_partCalled=false;
00207   d_offset_multi_trig=2;
00208   d_initMaxScore=(theoryCore()->getFlags()["quant-max-score"].getInt());
00209   for(size_t i=0; i<MAX_TRIG_BVS; i++){
00210     d_mybvs[i] = getEM()->newBoundVarExpr("_genbv", int2string(i), Type::anyType(getEM()));
00211   }
00212 }
00213 
00214 //! Destructor
00215 TheoryQuant::~TheoryQuant() {
00216   if(d_rules != NULL) delete d_rules;
00217   for(std::map<Type, CDList<size_t>* ,TypeComp>::iterator 
00218   it = d_contextMap.begin(), iend = d_contextMap.end(); 
00219       it!= iend; ++it) {
00220     delete it->second;
00221      free(it->second);
00222   }
00223 }
00224 
00225 int TheoryQuant::getExprScore(const Expr& e){
00226   return theoryCore()->getQuantLevelForTerm(e);
00227 }
00228 
00229 bool isSysPred(const Expr& e){
00230   return ( isLE(e) || isLT(e) || isGE(e) || isGT(e) || e.isEq());
00231 }
00232 
00233 bool canGetHead(const Expr& e){ 
00234   return (e.getKind() == APPLY || e.getKind() == READ || e.getKind() == WRITE); 
00235 } 
00236 
00237 bool isSimpleTrig(const Expr& t){
00238   if(!canGetHead(t)) return false; 
00239   for(int i = 0; i < t.arity(); i++){
00240     if (t[i].arity()>0 && t[i].containsBoundVar()) return false;
00241     if (BOUND_VAR == t[i].getKind()){
00242       for(int j = 0; j < i; j++){
00243   if(t[i] == t[j]) return false;
00244       }
00245     } 
00246   }
00247   return true;
00248 }
00249 
00250 bool isSuperSimpleTrig(const Expr& t){
00251   if(!isSimpleTrig(t)) return false; 
00252   for(int i = 0; i < t.arity(); i++){
00253     if (t[i].arity()>0 ) return false;
00254     if (BOUND_VAR != t[i].getKind()){
00255       return false;
00256     }
00257   } 
00258   return true;
00259 }
00260 
00261 
00262 bool usefulInMatch(const Expr& e){
00263   if(e.arity() == 0){
00264     TRACE("usefulInMatch", e.toString()+": ",e.arity(), "");
00265     TRACE("usefulInMatch", e.isRational(), "", "");
00266   }
00267   return ( canGetHead(e) || (isSysPred(e) && (!e.isEq()) ) );
00268 } 
00269 
00270 void TheoryQuant::setup(const Expr& e) {}
00271 
00272 void TheoryQuant::update(const Theorem& t, const Expr& e) {
00273 }
00274 
00275 std::string vectorExpr2string(const std::vector<Expr> & vec){
00276   std::string buf;
00277   for(size_t i=0; i<vec.size(); i++){
00278     buf.append(vec[i].toString());
00279     buf.append(" # ");
00280   }
00281   return buf;
00282 }
00283 
00284 static void recursiveGetSubTrig(const Expr& e, std::vector<Expr> & res) {
00285   if(e.getFlag())
00286    return;
00287 
00288   if(e.isClosure())
00289     return recursiveGetSubTrig(e.getBody(),res); 
00290 
00291   if (e.isApply()|| isSysPred(e)){
00292     res.push_back(e);
00293   }
00294   else
00295     if ( e.isTerm() && (!e.isVar()) && (e.getKind()!=RATIONAL_EXPR) ) {
00296   res.push_back(e);
00297       }
00298 
00299   for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)    {  
00300       recursiveGetSubTrig(*i,res);
00301     }
00302   
00303   e.setFlag();
00304   return ;
00305 }
00306 
00307 std::vector<Expr> getSubTrig(const Expr& e){
00308   e.clearFlags();
00309   std::vector<Expr> res;
00310   recursiveGetSubTrig(e,res);
00311   e.clearFlags();
00312   TRACE("getsub","e is ", e.toString(),"");
00313   TRACE("getsub","have ", res.size()," subterms");
00314   return res;
00315 }
00316 
00317 static void recGetSubTerms(const Expr& e, std::vector<Expr> & res) {
00318   if(e.getFlag())
00319    return;
00320 
00321   if(e.isClosure())
00322     return recGetSubTerms(e.getBody(),res); 
00323 
00324   for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)  {  
00325     recGetSubTerms(*i,res);
00326   }
00327 
00328   res.push_back(e);
00329 
00330   e.setFlag();
00331   return ;
00332 }
00333 
00334 const std::vector<Expr>& TheoryQuant::getSubTerms(const Expr& e){
00335   //the last item in res is e itself
00336   ExprMap<std::vector<Expr> >::iterator iter= d_subTermsMap.find(e);
00337   if( d_subTermsMap.end() == iter){
00338     e.clearFlags();
00339     std::vector<Expr> res;
00340     recGetSubTerms(e,res);
00341     e.clearFlags();
00342 
00343     TRACE("getsubs", "getsubs, e is: ", e, "");
00344     TRACE("getsubs", "e has ", res.size(), " subterms");
00345 
00346     d_subTermsMap[e] = res;
00347     return d_subTermsMap[e];
00348   }
00349   else{
00350     return (*iter).second;
00351   }
00352 }
00353 
00354 void TheoryQuant::enqueueInst(const Theorem& univ, const vector<Expr>& bind, const Expr& gterm){
00355   static int max_score =-1;
00356 
00357   bool partInst=false;
00358   if(bind.size() < univ.getExpr().getVars().size()){
00359     partInst=false;
00360     TRACE("sendinst","partinst",partInst,"");
00361   }
00362   
00363   Expr bind_expr(RAW_LIST, bind, getEM());
00364   
00365   if (*d_useInstLCache){
00366     const Expr& e = univ.getExpr();
00367     ExprMap<CDMap<Expr,bool>*>::iterator iterCache = d_bindHistory.find(e);
00368     if (iterCache != d_bindHistory.end()){
00369       CDMap<Expr,bool>* cache = (*iterCache).second; 
00370       if(cache->find(bind_expr) !=cache->end()){
00371   return ;
00372       }
00373       else{
00374   (*cache)[bind_expr] = true;
00375       }
00376     }
00377     else{
00378       CDMap<Expr,bool>* new_cache = new(true) CDMap<Expr,bool> (theoryCore()->getCM()->getCurrentContext());
00379       (*new_cache)[bind_expr] = true;
00380     }
00381   }
00382   
00383   Theorem thm ;
00384   if(null_expr == gterm ){//it is from naive instantiation or multi-inst
00385     TRACE("sendinst","gterm",gterm,"");
00386     if(partInst) {
00387       thm = d_rules->partialUniversalInst(univ, bind, 0);
00388     }
00389     else{
00390       thm = d_rules->universalInst(univ, bind, 0);
00391     }
00392   }
00393   else{
00394     int gscore = theoryCore()->getQuantLevelForTerm(gterm);    
00395     if(gscore > max_score){
00396       max_score = gscore;
00397       //      cout<<"max score "<<max_score<<endl;
00398     }
00399     if(partInst) {
00400       thm = d_rules->partialUniversalInst(univ, bind, gscore);
00401     }
00402     else{
00403       thm = d_rules->universalInst(univ, bind, gscore);
00404     }
00405   }
00406 
00407   Theorem simpThm = simplify(thm.getExpr());  
00408   
00409   if(*d_useInstTrue){
00410     Expr res = simpThm.getRHS();
00411     if(res.isTrue()){
00412       return;
00413     }
00414     if(res.isFalse() ){
00415       enqueueFact(thm); 
00416       //      setInconsistent(simpThm);
00417       d_allInstCount++;
00418       d_instThisRound++;
00419       throw FOUND_FALSE;
00420     }
00421   }
00422 
00423   d_simplifiedThmQueue.push(thm);
00424 
00425   TRACE("quant sendinst", "=gterm: ",gterm, "");
00426   TRACE("quant sendinst", "==add fact simp =", simplifyExpr(thm.getExpr()), "");
00427   TRACE("quant sendinst", "==add fact org =", thm.getExpr(), "");
00428   TRACE("quant sendinst", "==add fact from= ", univ.getExpr(), "\n===: "+vectorExpr2string(bind)); 
00429 }
00430 
00431 
00432 void TheoryQuant::enqueueInst(size_t univ_id , const std::vector<Expr>& bind, const Expr& gterm){
00433   static int max_score =-1;
00434 
00435   const Theorem& univ = d_univs[univ_id]; 
00436 
00437   bool partInst=false;
00438   if(bind.size() < univ.getExpr().getVars().size()){
00439     partInst=false;
00440     TRACE("sendinst","partinst",partInst,"");
00441   }
00442   
00443   Expr bind_expr(RAW_LIST, bind, getEM());
00444   
00445   if (*d_useInstLCache){
00446     const Expr& e = univ.getExpr();
00447     ExprMap<CDMap<Expr,bool>*>::iterator iterCache = d_bindHistory.find(e);
00448     if (iterCache != d_bindHistory.end()){
00449       CDMap<Expr,bool>* cache = (*iterCache).second; 
00450       if(cache->find(bind_expr) !=cache->end()){
00451   return ;
00452       }
00453       else{
00454   (*cache)[bind_expr] = true;
00455       }
00456     }
00457     else{
00458       CDMap<Expr,bool>* new_cache = new(true) CDMap<Expr,bool> (theoryCore()->getCM()->getCurrentContext());
00459       (*new_cache)[bind_expr] = true;
00460     }
00461   }
00462   
00463   Theorem thm ;
00464   if(null_expr == gterm ){//it is from naive instantiation or multi-inst
00465     TRACE("sendinst","gterm",gterm,"");
00466     if(partInst) {
00467       thm = d_rules->partialUniversalInst(univ, bind, 0);
00468     }
00469     else{
00470       thm = d_rules->universalInst(univ, bind, 0);
00471     }
00472   }
00473   else{
00474     int gscore = theoryCore()->getQuantLevelForTerm(gterm);    
00475     if(gscore > max_score){
00476       max_score = gscore;
00477       //      cout<<"max score "<<max_score<<endl;
00478     }
00479     if(partInst) {
00480       thm = d_rules->partialUniversalInst(univ, bind, gscore);
00481     }
00482     else{
00483       thm = d_rules->universalInst(univ, bind, gscore);
00484     }
00485   }
00486 
00487   Theorem simpThm = simplify(thm.getExpr());  
00488   
00489   if(*d_useInstTrue){
00490     Expr res = simpThm.getRHS();
00491     if(res.isTrue()){
00492       return;
00493     }
00494     if(res.isFalse() ){
00495       enqueueFact(thm); 
00496       //      setInconsistent(simpThm);
00497       d_allInstCount++;
00498       d_instThisRound++;
00499       throw FOUND_FALSE;
00500     }
00501   }
00502 
00503   d_simplifiedThmQueue.push(thm);
00504   //  cout<<"enqueue inst"<<thm << endl;
00505   TRACE("quant sendinst", "=gterm: ",gterm, "");
00506   TRACE("quant sendinst", "==add fact simp =", simplifyExpr(thm.getExpr()), "");
00507   TRACE("quant sendinst", "==add fact org =", thm.getExpr(), "");
00508   TRACE("quant sendinst", "==add fact from= ", univ.getExpr(), "\n===: "+vectorExpr2string(bind)); 
00509 }
00510 
00511 
00512 void TheoryQuant::enqueueInst(const Theorem& univ, 
00513             Trigger& trig, 
00514             const std::vector<Expr>& binds,  
00515             const Expr& gterm
00516             ) {
00517   return enqueueInst(univ,binds,gterm);
00518 }
00519 
00520 int TheoryQuant::sendInstNew(){
00521   int resNum = 0 ;
00522   
00523   while(!d_simplifiedThmQueue.empty()){
00524     const Theorem thm = d_simplifiedThmQueue.front();
00525     d_simplifiedThmQueue.pop();
00526     
00527     d_allInstCount++;
00528     d_instThisRound++;
00529     resNum++;
00530     enqueueFact(thm);
00531   }
00532 
00533   return resNum;
00534 }
00535 
00536 void TheoryQuant::addNotify(const Expr& e){}
00537 
00538 int recursiveExprScore(const Expr& e) {
00539   int res=0;
00540   DebugAssert(!(e.isClosure()), "exprScore called on closure");
00541   
00542   if(e.arity()== 0){
00543     res = 0;
00544   }
00545   else{
00546     for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)  {  
00547       res += recursiveExprScore(*i);
00548     }
00549   }
00550   res++;
00551   return res;
00552 }
00553 
00554 int exprScore(const Expr& e){
00555   return recursiveExprScore(e);
00556 }
00557 
00558 Expr getHeadExpr(const Expr& e){
00559   if (e.getKind() == APPLY){
00560     return e.getOp().getExpr();
00561   }
00562   
00563   if ( READ == e.getKind() || WRITE == e.getKind() )  {
00564     int kind = e[0].getKind();
00565     if (UCONST==kind) {
00566       return e[0];
00567     }
00568     else if (APPLY==kind || UFUNC == kind || READ == kind || WRITE == kind){
00569       return getHeadExpr(e[0]);
00570     }
00571     else if(e[0].isSkolem()){
00572       return e[0];
00573     }
00574   }
00575 
00576   return null_expr;
00577 }
00578 
00579 Expr  getHead(const Expr& e) {
00580   return getHeadExpr(e);
00581 }
00582 
00583 //! get the bound vars in term e,
00584 static bool recursiveGetBoundVars(const Expr& e, std::set<Expr>& result) {
00585   bool res(false);
00586   if(e.getFlag()){
00587     return e.containsBoundVar();
00588   }
00589   else if(e.isClosure()){
00590     res = recursiveGetBoundVars(e.getBody(),result); 
00591   }
00592   else if (BOUND_VAR == e.getKind() ){
00593     result.insert(e);
00594     e.setContainsBoundVar();
00595     res = true;
00596   }
00597   else {
00598     res = false;
00599     for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i){  
00600       if(recursiveGetBoundVars(*i,result)){
00601   res = true;
00602       }
00603     }
00604   }
00605 
00606   e.setFlag();
00607   
00608   if(res) {
00609     e.setContainsBoundVar();
00610   }
00611 
00612   return res;
00613 }
00614 
00615 
00616 //! get bound vars in term e, 
00617 std::set<Expr>  getBoundVars(const Expr& e){
00618   /*  
00619   //  static ExprMap<std::set<Expr> > bvsCache;
00620   static std::map<Expr, std::set<Expr> > bvsCache;
00621   std::map<Expr, std::set<Expr> >::iterator iterCache = bvsCache.find(e);
00622   //ExprMap<std::set<Expr> >::iterator iterCache = bvsCache.find(e);
00623 
00624   if (iterCache != bvsCache.end()){
00625     //    return iterCache->second; 
00626     return (*iterCache).second; 
00627   }
00628   */
00629   e.clearFlags(); 
00630   std::set<Expr> result ;   
00631   recursiveGetBoundVars(e,result);
00632   e.clearFlags();
00633   //  bvsCache[e]=result;
00634   return  result;
00635 }
00636 
00637 bool isGoodSysPredTrigger(const Expr& e){
00638   if(!isSysPred(e)) return false;
00639   if(usefulInMatch(e[0]) || usefulInMatch(e[1])) return true;
00640   return false;
00641 }
00642 
00643 bool isGoodFullTrigger(const Expr& e, const std::vector<Expr>& bVarsThm){
00644   if( !usefulInMatch(e))
00645     return false;
00646   
00647   const std::set<Expr>& bvs = getBoundVars(e);
00648 
00649   if (bvs.size() >= bVarsThm.size()){
00650      for(size_t i=0; i<bVarsThm.size(); i++)  {
00651        if (bvs.find(bVarsThm[i]) == bvs.end()){
00652    return false;
00653        }
00654      }
00655      return true;
00656   }
00657   else {
00658     return false;
00659   }
00660 }
00661 
00662 bool isGoodMultiTrigger(const Expr& e, const std::vector<Expr>& bVarsThm, int offset){
00663   if( !usefulInMatch(e) )
00664     return false;
00665   
00666   int bvar_missing = 0;
00667   const std::set<Expr>& bvs = getBoundVars(e);
00668 
00669   if(bvs.size() <= 0) return false;
00670 
00671   for(size_t i=0; i<bVarsThm.size(); i++) {
00672     if (bvs.find(bVarsThm[i]) == bvs.end()){
00673       bvar_missing++; // found one bound var missing in the e.
00674     }
00675   }
00676 
00677   if (0 == bvar_missing){ //it is a full triggers
00678     return false; 
00679   }
00680   
00681   if(bvar_missing <= offset){
00682     if(isSysPred(e)){
00683       if (isGoodSysPredTrigger(e)) {
00684   return true;
00685       }
00686       else {
00687   return false;
00688       }
00689     }
00690     else {
00691       return true;
00692     }
00693   }
00694   return false;
00695 }
00696 
00697 bool isGoodPartTrigger(const Expr& e, const std::vector<Expr>& bVarsThm){
00698   if( !usefulInMatch(e) )
00699     return false;
00700   
00701   size_t bvar_missing = 0;
00702   const std::set<Expr>& bvs = getBoundVars(e);
00703   
00704   for(size_t i=0; i<bVarsThm.size(); i++) {
00705     if (bvs.find(bVarsThm[i]) == bvs.end()){
00706       bvar_missing++; // found one bound var missing in the e.
00707     }
00708   }
00709 
00710   if (0 == bvar_missing){ //it is a full triggers
00711     return false; 
00712   }
00713   
00714   if(0 == bvs.size()){
00715     return false;
00716   } 
00717   
00718   if(bvar_missing < bVarsThm.size()){
00719     if(isSysPred(e)){
00720       if (isGoodSysPredTrigger(e)) {
00721   return true;
00722       }
00723       else {
00724   return false;
00725       }
00726     }
00727     else {
00728       return true;
00729     }
00730   }
00731   return false;
00732 }
00733 
00734 
00735 static bool recursiveGetPartTriggers(const Expr& e, std::vector<Expr>& res) {
00736   if(e.getFlag())
00737    return false;
00738 
00739   if(e.isClosure())
00740     return recursiveGetPartTriggers(e.getBody(), res); 
00741   
00742   if(0 == e.arity()){
00743     if(BOUND_VAR == e.getKind()){
00744       return false;
00745     }
00746     else{
00747       return true;
00748     }
00749   }
00750 
00751   bool good=true;
00752   bool no_bound =true;
00753   
00754   for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 
00755     if(BOUND_VAR == i->getKind()){
00756       no_bound=false;
00757       continue;
00758     }
00759     bool temp = recursiveGetPartTriggers(*i,res);
00760     if(false == temp) {
00761       good=false;
00762     }
00763   }
00764   
00765   e.setFlag();
00766   
00767   if(good && no_bound) {
00768     return true;
00769   }
00770   else if(good && !no_bound){
00771     res.push_back(e);
00772     return false;
00773   }
00774   else{
00775     return false;
00776   }
00777 }
00778 
00779 
00780 std::vector<Expr> getPartTriggers(const Expr& e){
00781   e.clearFlags();
00782   std::vector<Expr> res;
00783   recursiveGetPartTriggers(e,res);
00784   e.clearFlags();
00785   return res;
00786 }
00787 
00788 int trigInitScore(const Expr& e){
00789   if( isSysPred(e) && !isGoodSysPredTrigger(e)){
00790     return 1;
00791   }
00792   else {
00793     return 0;
00794   }
00795 } 
00796 
00797 void findPolarity(const Expr& e, ExprMap<Polarity>& res, Polarity  pol){
00798   if(!e.getType().isBool()) return;
00799   //now a AND b will be given a polarity too, this is not necessary.
00800   if(res.count(e)>0){
00801     if ((Neg == res[e] && Pos == pol) || (Neg == res[e] && Pos == pol) ){
00802       res[e]=PosNeg;
00803     }
00804   }
00805   else{
00806     res[e]=pol;
00807   }
00808   
00809   if(PosNeg==pol){
00810     for(int i=0; i<e.arity(); i++){
00811       findPolarity(e[i], res, pol);
00812     }
00813   }
00814   else{
00815     Polarity neg_pol=Ukn;
00816     if(Pos == pol) {
00817       neg_pol = Neg;
00818     }
00819     else if(Neg == pol){
00820       neg_pol = Pos;
00821     }
00822 
00823     if(e.isImpl()){
00824       findPolarity(e[0], res, neg_pol);
00825       findPolarity(e[1], res, pol);
00826     }
00827     else if(e.isAnd() || e.isOr()){
00828       for(int i=0; i<e.arity(); i++){
00829   findPolarity(e[i], res, pol);
00830       }
00831     }
00832     else if(e.isNot()){
00833       findPolarity(e[0], res, neg_pol);
00834     }
00835     else if(e.isITE()){
00836       findPolarity(e[0], res, PosNeg);
00837       findPolarity(e[1], res, pol);
00838       findPolarity(e[2], res, pol);
00839     }
00840     else if(e.isClosure()){
00841       findPolarity(e.getBody(), res, pol);
00842     }
00843     else if(e.isIff()){
00844       findPolarity(e[0], res, PosNeg);
00845       findPolarity(e[1], res, PosNeg);
00846     }
00847     else if(e.isXor()){
00848       findPolarity(e[0], res, neg_pol);
00849       findPolarity(e[1], res, neg_pol);
00850     }
00851     else if(e.isAtomicFormula()){
00852       return;
00853     }
00854     else{
00855       DebugAssert(false, "Error in find polarity in "+e.toString());
00856     }
00857   }
00858 }
00859 
00860 void TheoryQuant::arrayIndexName(const Expr& e){
00861   std::vector<Expr> res;
00862 
00863   const std::vector<Expr>& subs=getSubTerms(e);
00864   
00865   for(size_t i=0; i<subs.size(); i++){
00866     int kind = subs[i].getKind();
00867     if (READ == kind || WRITE == kind){
00868       const Expr& name = subs[i][0];
00869       const Expr& index = subs[i][1];
00870       if(getBoundVars(name).size() <= 0 && (getBoundVars(index).size() <=0)){
00871   std::vector<Expr> tp = d_arrayIndic[name];
00872   tp.push_back(index);
00873   d_arrayIndic[name]=tp;
00874       }
00875       else {
00876       }
00877     }
00878   }
00879 }
00880 
00881 void TheoryQuant::registerTrig(ExprMap<ExprMap<std::vector<dynTrig>* >* >& cur_trig_map,
00882              Trigger trig, 
00883              const std::vector<Expr> thmBVs, 
00884              size_t univ_id){
00885   {
00886     if(trig.hasRWOp){
00887       ExprMap<Expr> bv_map;
00888       dynTrig newDynTrig(trig, bv_map,univ_id);
00889       d_arrayTrigs.push_back(newDynTrig);
00890     }
00891   }
00892 
00893   ExprMap<Expr> bv_map;
00894   for(size_t i = 0; i<thmBVs.size(); i++){
00895     bv_map[thmBVs[i]] = null_expr;
00896   }
00897   const Expr& trig_ex = trig.getEx();
00898 
00899   Expr genTrig = generalTrig(trig_ex, bv_map);
00900 
00901   dynTrig newDynTrig(trig,bv_map,univ_id);
00902 
00903   Expr head = trig.getHead();
00904 
00905   ExprMap<ExprMap<vector<dynTrig>* >* >::iterator iter = cur_trig_map.find(head);
00906   if(cur_trig_map.end() == iter){
00907     ExprMap<vector<dynTrig>* >* new_cd_map= new  ExprMap<vector<dynTrig>* > ;
00908     cur_trig_map[head] = new_cd_map;
00909     vector<dynTrig>* new_dyntrig_list = new vector<dynTrig>;
00910     (*new_cd_map)[genTrig] = new_dyntrig_list;
00911     (*new_dyntrig_list).push_back(newDynTrig);
00912   }
00913   else{
00914     ExprMap<vector<dynTrig>* >* cd_map = iter->second;
00915     ExprMap<vector<dynTrig>* >::iterator iter_map = cd_map->find(genTrig);
00916     if(cd_map->end() == iter_map){
00917       vector<dynTrig>* new_dyntrig_list = new vector<dynTrig>; 
00918       (*cd_map)[genTrig] = new_dyntrig_list;
00919       (*new_dyntrig_list).push_back(newDynTrig);
00920     }
00921     else{
00922       //      (*((*cd_map)[generalTrig])).push_back(newDynTrig);
00923       (*(iter_map->second)).push_back(newDynTrig);
00924     }
00925   }
00926 }
00927 
00928 /*
00929 void TheoryQuant::registerTrigReal(Trigger trig, const std::vector<Expr> thmBVs, size_t univ_id){
00930   cout<<"register: "<<trig.getEx()<<endl;
00931   ExprMap<Expr> bv_map;
00932   for(size_t i = 0; i<thmBVs.size(); i++){
00933     bv_map[thmBVs[i]] = null_expr;
00934   }
00935   const Expr& trig_ex = trig.getEx();
00936 
00937   Expr genTrig = generalTrig(trig_ex, bv_map);
00938 
00939   dynTrig newDynTrig(trig,bv_map,univ_id);
00940 
00941   Expr head = trig.getHead();
00942   
00943   ExprMap<CDMap<Expr, CDList<dynTrig>* >* >::iterator iter = d_allmap_trigs.find(head);
00944   if(d_allmap_trigs.end() == iter){
00945     CDMap<Expr, CDList<dynTrig>* >* new_cd_map= 
00946       new(true) CDMap<Expr, CDList<dynTrig>* > (theoryCore()->getCM()->getCurrentContext());
00947     d_allmap_trigs[head] = new_cd_map;
00948     CDList<dynTrig>* new_dyntrig_list = new(true) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
00949     (*new_cd_map)[genTrig] = new_dyntrig_list;
00950     (*new_dyntrig_list).push_back(newDynTrig);
00951   }
00952   else{
00953     CDMap<Expr, CDList<dynTrig>* >* cd_map = iter->second;
00954     CDMap<Expr, CDList<dynTrig>* >::iterator iter_map = cd_map->find(genTrig);
00955     if(cd_map->end() == iter_map){
00956       CDList<dynTrig>* new_dyntrig_list = new(true) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
00957       (*cd_map)[genTrig] = new_dyntrig_list;
00958       (*new_dyntrig_list).push_back(newDynTrig);
00959     }
00960     else{
00961       //      (*((*cd_map)[generalTrig])).push_back(newDynTrig);
00962       (*((*iter_map).second)).push_back(newDynTrig);
00963       cout<<"once more"<<endl;
00964     }
00965   }
00966   
00967 }
00968 */
00969 Expr TheoryQuant::generalTrig(const Expr& trig, ExprMap<Expr>& bvs){
00970   size_t count =1 ;
00971   Expr res = recGeneralTrig(trig, bvs, count);
00972   getBoundVars(res);
00973   return res;
00974 }
00975 
00976 Expr TheoryQuant::recGeneralTrig(const Expr& trig, ExprMap<Expr>& bvs, size_t& mybvs_count){
00977   
00978   if (!trig.containsBoundVar()) return trig;
00979   if (BOUND_VAR == trig.getKind()){
00980     if (bvs.find(trig) != bvs.end()){
00981       const Expr& ubv = bvs[trig];
00982       if(null_expr ==ubv){
00983   Expr new_bv = d_mybvs[mybvs_count++];
00984   bvs[trig] = new_bv ;
00985   if((mybvs_count) >= MAX_TRIG_BVS ){
00986     throw "general trig error";
00987   }
00988   else{
00989     return new_bv;
00990   }
00991       }
00992       else{
00993   return bvs[trig];
00994       }
00995     }
00996     else{
00997       return d_mybvs[0];
00998     }
00999   }
01000   else{
01001     vector<Expr> children;      
01002       for(Expr::iterator i=trig.begin(), iend=trig.end(); i!=iend; ++i){  
01003   Expr repChild;
01004   if(i->containsBoundVar()){
01005     repChild = recGeneralTrig(*i, bvs, mybvs_count);
01006   }
01007   else{
01008     repChild = *i;
01009   }
01010   children.push_back(repChild);
01011       }
01012       return Expr(trig.getOp(), children);
01013   }
01014 }
01015 
01016 
01017 //this function is used to check if two triggers can match with eath other
01018 bool TheoryQuant::canMatch(const Expr& t1, const Expr& t2, ExprMap<Expr>& env){
01019   if(getBaseType(t1) != getBaseType(t2)) return false;
01020 
01021   if (BOUND_VAR == t1.getKind() || BOUND_VAR == t2.getKind()) {
01022     return true;
01023   }
01024 
01025   if ( (t1.arity() != t2.arity()) || (t1.getKind() != t2.getKind() )) {
01026     return false;
01027   }
01028   if (canGetHead(t1) && canGetHead(t2)) {
01029     if ( getHead(t1) != getHead(t2) ){
01030       return false;
01031     }
01032     for(int i=0; i<t1.arity(); i++){
01033       if (false == canMatch(t1[i], t2[i] , env))
01034   return false;
01035     }
01036     return true;
01037   }
01038   else{
01039     return false;
01040   }
01041 }
01042 
01043 bool TheoryQuant::isTransLike (const vector<Expr>& cur_trig){
01044   if(!(*d_useTrans)){
01045     return false;
01046   }
01047   if(3==cur_trig.size()){
01048     const Expr& t1=cur_trig[0];
01049     const Expr& t2=cur_trig[1];
01050     const Expr& t3=cur_trig[2];
01051     if ( canGetHead(t1) && canGetHead(t2) && canGetHead(t3) && 
01052    (getHead(t1) == getHead(t2)) &&  (getHead(t2) == getHead(t3))){
01053       const std::set<Expr>& ts1 = getBoundVars(t1); 
01054       const std::set<Expr>& ts2 = getBoundVars(t2); 
01055       const std::set<Expr>& ts3 = getBoundVars(t3);
01056       if ( 2==ts1.size() && 2==ts2.size() && 2==ts2.size() && 
01057      (ts1 != ts2) && (ts2 != ts3) && (ts3 != ts1)){
01058   std::set<Expr> all;
01059   for(set<Expr>::const_iterator i=ts1.begin(), iend = ts1.end(); i != iend; i++){
01060     all.insert(*i);
01061   }
01062   for(set<Expr>::const_iterator i=ts2.begin(), iend = ts2.end(); i != iend; i++){
01063     all.insert(*i);
01064   }
01065   for(set<Expr>::const_iterator i=ts3.begin(), iend = ts3.end(); i != iend; i++){
01066     all.insert(*i);
01067   }
01068   bool res = true;
01069   if(3==all.size()){
01070     for(set<Expr>::const_iterator i=all.begin(), iend = all.end(); i != iend; i++){
01071       if(!i->isVar()) {
01072         res = false;
01073         break;
01074       }
01075     }
01076     if(res) {
01077     }
01078     return res;
01079   }
01080       } 
01081     }  
01082   }
01083   return false; 
01084 }
01085 
01086 bool TheoryQuant::isTrans2Like (const std::vector<Expr>& all_terms, const Expr& tr2){
01087   if(!(*d_useTrans2)){
01088     return false;
01089   }
01090   for(size_t i = 0; i < all_terms.size(); i++){
01091     if(all_terms[i].isEq()){
01092       const Expr& cur = all_terms[i];
01093       if(cur[0] != cur[1] && ( (cur[0]==tr2[0] && cur[1]==tr2[1]) || (cur[0]==tr2[1] && cur[1]==tr2[0]))){
01094   return true;
01095       } 
01096     }
01097   }
01098   return false; 
01099 }
01100 
01101 
01102 bool goodMultiTriggers(const std::vector<Expr>& exprs, const std::vector<Expr> bVars){
01103   ExprMap<bool> bvar_found;
01104   
01105   for( std::vector<Expr>::const_iterator i = bVars.begin(),  iend= bVars.end();  i!=iend; i++) {
01106     bvar_found[*i]=false;
01107   }
01108 
01109   for (size_t  i=0; i< exprs.size();i++){
01110     const std::set<Expr> & bv_in_trig = getBoundVars(exprs[i]);
01111     for(std::set<Expr>::const_iterator j=bv_in_trig.begin(), jend = bv_in_trig.end();  j != jend; j++){
01112       if(bvar_found.find(*j) != bvar_found.end()){
01113   bvar_found[*j]=true;
01114       }
01115     }
01116   }
01117   
01118   for( std::vector<Expr>::const_iterator i = bVars.begin(), iend= bVars.end();  i!=iend;  i++) {
01119     if(false == bvar_found[*i]){
01120       return false ;
01121     }
01122   }
01123   return true;
01124 }
01125 
01126 
01127 inline size_t locVar(const vector<Expr>& bvsThm, const Expr& bv){
01128   for(size_t i=0, iend = bvsThm.size(); i < iend; i++){
01129     if (bvsThm[i] == bv){
01130       return i;
01131     }
01132   }
01133   return 999; //this number should be big enough
01134 } 
01135 
01136 void TheoryQuant::setupTriggers(const Theorem& thm, size_t univs_id){
01137 }
01138 
01139 void TheoryQuant::setupTriggers(ExprMap<ExprMap<vector<dynTrig>* >*>& trig_maps,
01140         const Theorem& thm, 
01141         size_t univs_id){
01142   const Expr& e = thm.getExpr();
01143   TRACE("triggers","setup : ",e.toString()," || ");
01144   //  cout<<"set up "<<e<<endl;
01145   d_univs.push_back(thm);
01146   const std::vector<Expr>& bVarsThm = e.getVars(); 
01147   if  (d_hasTriggers.count(e) > 0) {
01148     std::vector<Trigger>& new_trigs = d_fullTrigs[e];
01149     for(size_t i=0; i<new_trigs.size(); i++){
01150       registerTrig(trig_maps, new_trigs[i], bVarsThm, univs_id);
01151     }
01152     if(0 == new_trigs.size()){
01153       std::vector<Trigger>& new_mult_trigs = d_multTrigs[e];
01154       for(size_t j=0; j<new_mult_trigs.size(); j++){
01155   registerTrig(trig_maps, new_mult_trigs[j], bVarsThm, univs_id);
01156       }
01157     } 
01158     return;
01159   }
01160 
01161   d_hasTriggers[e]=true;
01162 
01163   const std::vector<Expr>& subterms = getSubTrig(e);
01164 
01165 #ifdef DEBUG
01166   if( CVC3::debugger.trace("triggers")  ){
01167     cout<<"===========all sub terms =========="<<endl;
01168     for (size_t i=0; i<subterms.size(); i++){
01169       const Expr& sub = subterms[i];
01170       cout<<"i="<< i << " : " << findExpr(sub) << " | " << sub << " and type is " << sub.getType() 
01171     << " and kind is " << sub.getEM()->getKindName(sub.getKind()) << endl;
01172     }
01173   }
01174 #endif
01175 
01176   ExprMap<Polarity> exprPol;
01177   findPolarity(e, exprPol, Pos);
01178 
01179   {
01180     std::vector<Expr> trig_cadt;
01181     for(std::vector<Expr>::const_iterator i = subterms.begin(),iend=subterms.end(); i!=iend; i++){
01182       if(isGoodFullTrigger(*i, bVarsThm)) {
01183   trig_cadt.push_back(*i);
01184       }
01185     }
01186 
01187     std::vector<Expr> trig_list;
01188     std::vector<Expr> trig_extra;
01189 
01190     for(size_t iter =0; iter < trig_cadt.size(); iter++) {
01191       Expr* i = &(trig_cadt[iter]);
01192       bool notfound = true;
01193       
01194       for(size_t index=0; index< trig_list.size(); index++){ 
01195   if (i->subExprOf(trig_list[index])) {
01196     trig_list[index]=*i;
01197     notfound=false;
01198     break;
01199   }
01200   if (trig_list[index].subExprOf(*i)) {
01201     notfound=false;
01202     break;
01203   }
01204       }
01205       if (notfound) {
01206   trig_list.push_back(*i);
01207       }
01208     }
01209     
01210     std::vector<Trigger> trig_ex;
01211     
01212     for (size_t  i=0; i< trig_list.size();i++){
01213       const Expr& cur = trig_list[i];
01214       const std::set<Expr> cur_bvs = getBoundVars(cur);
01215       int score = trigInitScore(cur);
01216       if(score > 0) continue;
01217 
01218       //1. test trans2 
01219       //2. test whether a trigger can trig a bigger instance of itself, now we have no actions for such case because we use expr score and dynamic loop prevention. 
01220       
01221       for(size_t j=0; j< trig_cadt.size(); j++){
01222   if (trig_list[i] == trig_cadt[j]) continue;
01223   ExprMap<Expr> null;
01224   if (canMatch(trig_list[i], trig_cadt[j], null)){
01225     if(exprScore(trig_list[i]) < exprScore(trig_cadt[j])){
01226     } 
01227     else if(*d_useTrans2 &&
01228       trig_list.size() == 2 &&
01229       trig_list[i].arity() == 2 && 
01230       BOUND_VAR == trig_list[i][0].getKind() && 
01231       BOUND_VAR == trig_list[i][1].getKind() && 
01232       BOUND_VAR == trig_cadt[j][0].getKind() && 
01233       BOUND_VAR == trig_cadt[j][1].getKind() && 
01234       isTrans2Like(subterms, trig_list[i])
01235       ){
01236       
01237       score =0; //useless, to delete;
01238       d_trans2_num++;
01239       
01240       DebugAssert(d_trans2_num<=1, "more than 2 trans2 found");
01241       TRACE("triggers",  "trans2 found ", trig_list[i], "");
01242       
01243       Trigger t(theoryCore(), cur, Neg, cur_bvs);
01244       t.setTrans2(true);
01245       t.setHead(getHeadExpr(cur));
01246       if(isSimpleTrig(cur)){
01247         t.setSimp();
01248       }
01249       if(isSuperSimpleTrig(cur)){
01250         t.setSuperSimp();
01251       }
01252       d_fullTrigs[e].push_back(t);
01253       registerTrig(trig_maps,t, bVarsThm, univs_id);
01254       return;
01255     }
01256     else{
01257       score =0;
01258     }
01259   }
01260       }
01261       
01262       Polarity pol= Ukn;
01263       
01264       if(cur.getType().isBool()){
01265   DebugAssert(exprPol.count(e)>0,"unknown polarity:"+cur.toString());
01266   pol = exprPol[cur];
01267       }
01268       
01269       Trigger* t;
01270       Trigger* t_ex; //so, if a pred is PosNeg, we actually put two triggers into the list, one pos and the other neg
01271       
01272       if(PosNeg == pol && *d_usePolarity){
01273   t = new Trigger(theoryCore(), cur, Pos, cur_bvs);
01274   t_ex = new Trigger(theoryCore(), cur, Neg, cur_bvs);
01275   if(isSimpleTrig(cur)){
01276     t->setSimp();
01277     t_ex->setSimp();
01278   }
01279   if(isSuperSimpleTrig(cur)){
01280     t->setSuperSimp();
01281     t_ex->setSuperSimp();
01282   }
01283 
01284       }
01285       else{
01286   t = new Trigger(theoryCore(), cur, pol, cur_bvs);
01287   if(isSimpleTrig(cur)){
01288     t->setSimp();
01289   }
01290   if(isSuperSimpleTrig(cur)){
01291     t->setSuperSimp();
01292   }
01293   t_ex = NULL;
01294       }
01295       
01296       if(canGetHead(cur)) {
01297   t->setHead(getHeadExpr(cur));
01298   if(NULL != t_ex){
01299     t_ex->setHead(getHeadExpr(cur));
01300   }
01301       }
01302       else{
01303   if(!isSysPred(cur)){
01304     //    cout<<"cur " << cur <<endl;
01305     DebugAssert(false, "why this is a trigger");
01306   }
01307       } 
01308      
01309       t->setRWOp(false);
01310       
01311       if(READ == cur.getKind() || WRITE == cur.getKind()){
01312   arrayIndexName(cur);
01313       }
01314 
01315       if(READ == cur.getKind() && WRITE== cur[0].getKind() && 1 == bVarsThm.size() ){
01316   //  cout<<t->trig<<endl;
01317   t->setRWOp(true);
01318   if(t_ex != NULL) t_ex->setRWOp(true);
01319       }
01320       
01321       if(t_ex != NULL)  {
01322   trig_ex.push_back(*t_ex);
01323       }
01324       
01325       d_fullTrigs[e].push_back(*t);
01326       registerTrig(trig_maps,*t, bVarsThm, univs_id);
01327 
01328       TRACE("triggers", "new:full triggers:", cur.toString(),"");
01329       TRACE("triggers", "new:full trigger score:", score,"");
01330       TRACE("triggers", "new:full trigger pol:", pol,"");
01331     }
01332     
01333     for(size_t i=0; i<trig_ex.size(); i++){
01334       d_fullTrigs[e].push_back(trig_ex[i]);
01335       registerTrig(trig_maps,trig_ex[i], bVarsThm, univs_id);
01336       TRACE("triggers", "new extra :full triggers:", trig_ex[i].getEx().toString(),"");
01337     }
01338     
01339     if(d_fullTrigs[e].size() == 0){
01340       TRACE("triggers warning", "no full trig: ", e , ""); 
01341     }
01342   }
01343   
01344   if(0 == d_fullTrigs[e].size() )
01345     {  //setup multriggers
01346       for( std::vector<Expr>::const_iterator i = subterms.begin(),  iend=subterms.end();  i!=iend;  i++) {
01347   if(isGoodMultiTrigger(*i, bVarsThm, d_offset_multi_trig))  {
01348     bool notfound = true;
01349     for(size_t index=0; index<d_multTriggers[e].size(); index++){ 
01350       if (i->subExprOf(d_multTriggers[e][index]))    {
01351         (d_multTriggers[e][index])=*i; 
01352         notfound=false;
01353       }
01354     }
01355     if (notfound){        
01356       d_multTriggers[e].push_back(*i);
01357     }
01358   }
01359       }
01360       
01361       std::vector<Expr>& cur_trig = d_multTriggers[e];
01362       
01363       if (goodMultiTriggers(cur_trig, bVarsThm)){
01364   //  cout<<"good multi triggers"<<endl;
01365   TRACE("multi-triggers", "good set of multi triggers","","");
01366   for (size_t  i=0; i< d_multTriggers[e].size();i++){
01367     //    cout<<"multi-triggers" <<d_multTriggers[e][i]<<endl;
01368     TRACE("multi-triggers", "multi-triggers:", d_multTriggers[e][i].toString(),"");
01369   }
01370       }
01371       else{
01372   cur_trig.clear();
01373   //  cout<<"bad multi triggers"<<endl; 
01374   TRACE("multi-triggers", "bad set of multi triggers","","");
01375       }
01376       
01377       //special code for transitive pred,
01378       {
01379   if(isTransLike(cur_trig)){
01380     d_trans_num++;
01381     DebugAssert(d_trans_num <= 1, "more than one trans found");
01382     
01383     Expr ex = cur_trig[0];
01384 
01385     Trigger* trans_trig = new Trigger(theoryCore(), ex, Neg, getBoundVars(ex));
01386     trans_trig->setHead(getHeadExpr(ex));
01387     if(isSimpleTrig(ex)){
01388       trans_trig->setSimp();
01389     }
01390     if(isSuperSimpleTrig(ex)){
01391       trans_trig->setSuperSimp();
01392     }
01393 
01394     trans_trig->setTrans(true);
01395     
01396     d_fullTrigs[e].push_back(*trans_trig);
01397     registerTrig(trig_maps,*trans_trig, bVarsThm, univs_id);
01398     cur_trig.clear();
01399   }
01400       }
01401       
01402       //enhanced multi-triggers 
01403       if(cur_trig.size() >0 ){
01404   //  if(cur_trig.size() >0 ){
01405   std::vector<Expr> posList, negList;
01406   for(size_t k=0; k<cur_trig.size(); k++){
01407     const Expr& cur_item = cur_trig[k];
01408     if (cur_item.getType().isBool()){
01409       Polarity pol = exprPol[cur_item];
01410       if(PosNeg == pol || Pos == pol){
01411         posList.push_back(cur_item);
01412       }
01413       if(PosNeg == pol || Neg == pol){
01414         negList.push_back(cur_item);
01415       }
01416     }
01417   }
01418   if (goodMultiTriggers(posList, bVarsThm)){
01419     TRACE("multi-triggers", "good set of multi triggers pos","","");
01420     for (size_t  i=0; i< posList.size();i++){
01421       TRACE("multi-triggers", "multi-triggers:", posList[i].toString(),"");
01422     }
01423     cur_trig.clear();
01424     for(size_t m=0; m<posList.size(); m++){
01425       cur_trig.push_back(posList[m]);
01426     }
01427   }
01428   if (goodMultiTriggers(negList, bVarsThm) && negList.size() < cur_trig.size()){
01429     TRACE("multi-triggers", "good set of multi triggers neg","","");
01430     for (size_t  i=0; i< negList.size();i++){
01431       TRACE("multi-triggers", "multi-triggers:", negList[i].toString(),"");
01432     }
01433     cur_trig.clear();
01434     for(size_t m=0; m<negList.size(); m++){
01435       cur_trig.push_back(negList[m]);
01436     }
01437   }
01438   //  cout<<"neg list and pos list"<<negList.size()<<" | " <<posList.size()<<endl;
01439       }
01440       
01441       {//new way of multi trigger
01442 
01443   
01444   if( 3 == cur_trig.size() ||  4 == cur_trig.size() || 5 == cur_trig.size() || 6 == cur_trig.size()  ){
01445     for(size_t i = 0; i < cur_trig.size(); i++){
01446       for(size_t j = 0; j < i; j++){
01447         vector<Expr> tempList;
01448         tempList.clear();
01449         tempList.push_back(cur_trig[i]);
01450         tempList.push_back(cur_trig[j]);
01451         //        cout<<i<<" | "<<j<<endl;
01452         //        cout<<vectorExpr2string(tempList)<<endl;
01453         if (goodMultiTriggers(tempList, bVarsThm)){
01454     cur_trig.clear();
01455     cur_trig.push_back(tempList[0]);
01456     cur_trig.push_back(tempList[1]);
01457     break;
01458         }
01459       }
01460     }
01461   } 
01462   
01463   if(cur_trig.size() != 2){
01464     if( 0 == cur_trig.size()){
01465       return;
01466     }
01467     //    FatalAssert(false, "unsupported multi-triggers");
01468     //      cout<<"e: "<<e<<endl;
01469     //      cout<<cur_trig.size()<<endl;
01470     //      cout<<bVarsThm.size()<<endl;
01471     //
01472     //    cout<<vectorExpr2string(bVarsThm)<<endl;
01473     //    for(size_t i =0; i<cur_trig.size(); i++){
01474     //      cout<<cur_trig[i]<<endl;
01475     //    } 
01476     return;
01477   }
01478   
01479   for(size_t i = 0 ; i<cur_trig.size(); i++){
01480     set<Expr> bvs = getBoundVars(cur_trig[i]);
01481     Trigger trig(theoryCore(), cur_trig[i], Ukn, bvs); // 
01482     trig.setHead(getHead(cur_trig[i]));
01483     trig.setMultiTrig();
01484     trig.multiIndex = i;
01485     trig.multiId=d_all_multTrigsInfo.size();
01486     d_multTrigs[e].push_back(trig);
01487     registerTrig(trig_maps, trig, bVarsThm, univs_id);
01488   }
01489   
01490   {
01491     multTrigsInfo multTrigs;
01492     for(size_t i =0, iend = d_multTrigs[e].size(); i<iend; i++){
01493       const std::vector<Expr>& one_set_bvs = d_multTrigs[e][i].bvs;
01494       std::vector<size_t> one_set_pos;
01495       
01496       for(size_t v = 0, vend = one_set_bvs.size(); v<vend; v++){
01497         size_t loc = locVar(bVarsThm, one_set_bvs[v]); 
01498         if( 999 != loc ){
01499     one_set_pos.push_back(loc);
01500         }
01501       }
01502       
01503       sort(one_set_pos.begin(), one_set_pos.end());
01504 
01505       for(size_t v = 0, vend = one_set_pos.size(); v<vend; v++){
01506       }
01507 
01508       multTrigs.var_pos.push_back(one_set_pos);
01509     }//setup pos of all multi tirggers
01510     
01511     //now we only consider two multi triggers
01512     vector<size_t> common;
01513     std::vector<size_t>& tar1 = multTrigs.var_pos[0];
01514     std::vector<size_t>& tar2 = multTrigs.var_pos[1];
01515     vector<size_t>::iterator t1(tar1.begin()), t2(tar2.begin());
01516     while(t1 != tar1.end() && t2!= tar2.end()){
01517       size_t pos1 = *t1;
01518       size_t pos2 = *t2;
01519       if( pos1  == pos2 ) {
01520         common.push_back(pos1);
01521         t1=tar1.erase(t1); 
01522         t2=tar2.erase(t2);
01523       }
01524       else if( pos1 > pos2 ){
01525         t2++;
01526       }
01527       else {
01528         t1++;
01529       }
01530     }
01531     multTrigs.common_pos.push_back(common);
01532     
01533     size_t multi_size = d_multTrigs[e].size(); //should be 2
01534     for(size_t i =0; i< multi_size; i++){
01535       multTrigs.var_binds_found.push_back(new (true) CDMap<Expr, bool> (theoryCore()->getCM()->getCurrentContext()));
01536     }
01537     multTrigs.uncomm_list.push_back(new ExprMap<CDList<Expr>* >);
01538     multTrigs.uncomm_list.push_back(new ExprMap<CDList<Expr>* >);
01539     d_multitrigs_maps[e]=multTrigs;
01540     d_all_multTrigsInfo.push_back(multTrigs);
01541   }
01542       }
01543     }
01544   
01545   //setup partial triggers
01546   if(*d_usePart)
01547     {
01548     std::vector<Trigger> trig_ex;
01549     
01550     trig_ex.clear();
01551     for( std::vector<Expr>::const_iterator i = subterms.begin(),  iend=subterms.end();  i!=iend;  i++) {
01552       if(isGoodPartTrigger(*i, bVarsThm))  {
01553   bool notfound = true;
01554   for(size_t index=0; index<d_partTriggers[e].size(); index++){ 
01555     if (i->subExprOf(d_partTriggers[e][index]))    {
01556       (d_partTriggers[e][index])=*i; 
01557       notfound=false;
01558     }
01559   }
01560   if (notfound)       
01561     d_partTriggers[e].push_back(*i); 
01562       }
01563     }
01564     
01565     for (size_t  i=0; i< d_partTriggers[e].size();i++){
01566       TRACE("triggers", "partial triggers:", d_partTriggers[e][i].toString(),"");
01567     }
01568     
01569     for (size_t  i=0; i< d_partTriggers[e].size();i++){
01570       Polarity pol= Ukn;
01571       const Expr& cur = d_partTriggers[e][i]; 
01572       const std::set<Expr> cur_bvs = getBoundVars(cur); 
01573       if(cur.getType().isBool()){
01574   DebugAssert(exprPol.count(e)>0,"unknown polarity:"+cur.toString());
01575   pol = exprPol[cur];
01576       }
01577       
01578       Trigger* t;
01579       Trigger* t_ex; //so, if a pred is PosNeg, we actually put two triggers into the list, one pos and the other neg
01580       
01581       if(PosNeg == pol && *d_usePolarity){
01582   t = new Trigger(theoryCore(), cur, Pos, cur_bvs);
01583   t_ex = new Trigger(theoryCore(), cur, Neg, cur_bvs);
01584       }
01585       else{
01586   t = new Trigger(theoryCore(), cur, pol, cur_bvs);
01587   t_ex = NULL;
01588       }
01589       
01590       if(canGetHead(cur)) {
01591   t->setHead(getHeadExpr(cur));
01592       }
01593       
01594       if(t_ex != NULL)  trig_ex.push_back(*t_ex);
01595       
01596       d_partTrigs[e].push_back(*t);
01597       
01598       TRACE("triggers", "new:part trigger pol:", pol,cur.toString());
01599     }
01600     
01601     for(size_t i=0; i<trig_ex.size(); i++){
01602       d_partTrigs[e].push_back(trig_ex[i]);
01603       TRACE("triggers", "new extra :part triggers:", trig_ex[i].getEx().toString(),"");
01604     }
01605   }  
01606 }
01607 
01608 
01609 
01610 //! test if a sub-term contains more bounded vars than quantified by out-most quantifier.
01611 int hasMoreBVs(const Expr& thm){
01612   DebugAssert(thm.isForall(), "hasMoreBVS called by non-forall exprs");
01613   
01614   const std::vector<Expr>& bvsOutmost = thm.getVars();
01615   const std::set<Expr>& bvs = getBoundVars(thm); 
01616 
01617   return int(bvs.size()-bvsOutmost.size()); 
01618 
01619 }
01620 
01621 /*! \brief Theory interface function to assert quantified formulas
01622  *
01623  * pushes in negations and converts to either universally or existentially 
01624  * quantified theorems. Universals are stored in a database while 
01625  * existentials are enqueued to be handled by the search engine.
01626  */
01627 void TheoryQuant::assertFact(const Theorem& thm){
01628 
01629   if(*d_translate) return;
01630   TRACE("quant assertfact", "assertFact => ", thm.toString(), "{");
01631   Theorem rule, result;
01632   const Expr& expr = thm.getExpr();
01633   // Ignore existentials
01634 
01635   if(expr.isExists()) {
01636     TRACE("quant assertfact", "assertFact => (ignoring existential) }", expr.toString(), "");
01637     return;
01638   }
01639 
01640   DebugAssert(expr.isForall() || (expr.isNot() && (expr[0].isExists() || expr[0].isForall())),
01641         "Theory of quantifiers cannot handle expression "
01642         + expr.toString());
01643 
01644   if(expr.isNot()) {//find the right rule to eliminate negation
01645     if(expr[0].isForall()) {
01646       rule = d_rules->rewriteNotForall(expr);
01647     }
01648     else if(expr[0].isExists()) {
01649       rule = d_rules->rewriteNotExists(expr);
01650     }
01651     result = iffMP(thm, rule);
01652   }
01653   else{
01654     result = thm;
01655   }
01656 
01657   result = d_rules->boundVarElim(result); //eliminate useless bound variables
01658   
01659   if(result.getExpr().isForall()){
01660 
01661     if(*d_useNew){
01662 
01663       if(result.getExpr().getBody().isForall()){ // if it is of the form forall x. forall. y
01664   result=d_rules->packVar(result);
01665       }
01666       result = d_rules->boundVarElim(result); //eliminate useless bound variables
01667 
01668       int nBVs = hasMoreBVs(result.getExpr());
01669       if( nBVs >= 1){
01670   d_hasMoreBVs[result.getExpr()]=true;
01671       }
01672       d_rawUnivs.push_back(result);
01673       return;
01674       /* -------------------------------------- */
01675       //      int nBVs = hasMoreBVs(result.getExpr());
01676 
01677       if(0 == nBVs){//good 
01678   TRACE("quant assertfact", "assertFact => forall enqueueing: ", result.toString(), "}");
01679         d_univs.push_back(result);
01680   setupTriggers(result, d_univs.size()-1);
01681       }
01682       else if(1== nBVs){
01683   d_hasMoreBVs[result.getExpr()]=true;
01684   const Expr& body = result.getExpr().getBody();
01685 
01686   if(*d_usePullVar){
01687     if((body.isAnd() && body[1].isForall()) || (body.isImpl() && body[1].isForall()) ){
01688       result=d_rules->pullVarOut(result);
01689 
01690       TRACE("quant assertfact", "assertFact => pull-var enqueueing: ", result.toString(), "}");
01691 
01692       d_univs.push_back(result);
01693       setupTriggers(result,  d_univs.size()-1);
01694     }
01695   }
01696   else{
01697     TRACE("quant assertfact", "debug:not recognized case", result.toString(), thm.toString());
01698 
01699     d_univs.push_back(result);
01700     setupTriggers(result,  d_univs.size()-1);
01701     return;
01702   }
01703       }
01704       else{
01705   d_hasMoreBVs[result.getExpr()]=true;
01706   d_univs.push_back(result);
01707   setupTriggers(result,  d_univs.size()-1);
01708   return;
01709       }
01710     }
01711     else{
01712 
01713       TRACE("quant assertfact", "assertFact => old-fashoin enqueueing: ", result.toString(), "}");
01714       //      cout<<"error"<<endl;
01715       d_univs.push_back(result);
01716     }
01717   }
01718   else { //quantifier got eliminated or is an existantial formula 
01719 
01720     TRACE("quant assertfact", "assertFact => non-forall enqueueing: ", result.toString(), "}");
01721     enqueueFact(result);
01722   }
01723 }
01724 
01725 void TheoryQuant::recGoodSemMatch(const Expr& e,
01726           const std::vector<Expr>& bVars,
01727           std::vector<Expr>& newInst,
01728           std::set<std::vector<Expr> >& instSet)
01729 {
01730   size_t curPos = newInst.size();
01731   if (bVars.size() == curPos)    {
01732     Expr simpleExpr = simplifyExpr(e.substExpr(bVars,newInst));
01733     if (simpleExpr.hasFind()){
01734       std::vector<Expr> temp = newInst;
01735       instSet.insert(temp);
01736       TRACE("quant yeting", "new inst found for ", e.toString()+" ==> ", simpleExpr.toString());
01737     };
01738   }
01739   else {
01740     Type t = getBaseType(bVars[curPos]);
01741     std::vector<Expr> tyExprs= d_typeExprMap[t];
01742     if (0 == tyExprs.size())  {
01743       return;//has some problem
01744     }
01745     else{
01746       for (size_t i=0;i<tyExprs.size();i++){
01747   newInst.push_back(tyExprs[i]);
01748   recGoodSemMatch(e,bVars,newInst,instSet);
01749   newInst.pop_back();
01750       }
01751     }
01752   }
01753 }
01754 
01755 bool isIntx(const Expr& e, const Rational& x){
01756   if(e.isRational() && e.getRational()==x)
01757     return true;
01758   else return false;
01759 }
01760 
01761 Expr getLeft(const Expr& e){
01762   if(e.getKind()!= PLUS) return null_expr;
01763   if(e.arity() != 3) return null_expr;
01764   Expr const_expr, minus ,pos;
01765   int numMinus=0, numPos=0, numConst=0;;
01766   for(int i=0; i<e.arity(); i++){
01767     if((e[i]).getKind() == MULT){
01768       if(isIntx(e[i][0], -1)){
01769   numMinus++;
01770   minus=e[i][1];
01771       }
01772       else{
01773   numPos++;
01774   pos=e[i];
01775       }
01776     }
01777     else if(e[i].isRational())      {
01778       const_expr = e[i];
01779       numConst++;
01780     }
01781     else{
01782       numPos++;
01783       pos=e[i];
01784     }
01785   }
01786   if(1==numPos && 1==numConst && 1==numMinus){
01787     return minus;
01788   }
01789   else{
01790     return null_expr;
01791   }
01792 }
01793 
01794 Expr getRight(const Expr& e){
01795   if(e.getKind()!= PLUS) return null_expr;
01796   if(e.arity() != 3) return null_expr;
01797   Expr const_expr, minus ,pos;
01798   int numMinus=0, numPos=0, numConst=0;;
01799  
01800   for(int i=0; i<e.arity(); i++){
01801     if((e[i]).getKind() == MULT){
01802       if(isIntx(e[i][0], -1)){
01803   numMinus++;
01804   minus=e[i][1];
01805       }
01806       else{
01807   numPos++;
01808   pos=e[i];
01809       }
01810     }
01811     else if(e[i].isRational())      {
01812       const_expr = e[i];
01813       numConst++;
01814     }
01815     else{
01816       numPos++;
01817       pos=e[i];
01818     }
01819   }
01820   
01821   if(1==numPos && 1==numConst && 1==numMinus){
01822     if(isIntx(const_expr,0)){
01823       return pos;
01824     }
01825     else{
01826       //      return null_expr;
01827       return Expr(PLUS, const_expr, pos);
01828     }
01829   }
01830   else{
01831     return null_expr;
01832   }
01833 }
01834  
01835 inline void TheoryQuant::add_parent(const Expr& parent){
01836   ExprMap<CDList<Expr>* >::iterator iter;
01837   for(int i=0; i< parent.arity(); i++){
01838     const Expr& child = parent[i];
01839     iter = d_parent_list.find(child);
01840     if(d_parent_list.end() == iter){
01841       d_parent_list[child] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
01842       d_parent_list[child]->push_back(parent);
01843     }
01844     else{
01845       iter->second->push_back(parent);
01846     }
01847   }
01848 }
01849 
01850 void TheoryQuant::collectChangedTerms(CDList<Expr>& changed){
01851   ExprMap<bool> eqs_hash;
01852   ExprMap<bool> changed_hash;
01853   /*
01854   {
01855     for(ExprMap<CDList<Expr>* >::iterator iter = d_eq_list.begin(), iter_end=d_eq_list.end(); 
01856   iter != iter_end; iter++){
01857       CDList<Expr>* cur_eqs = iter->second;
01858       int begin_pos;
01859       Expr head = iter->first;
01860       if(d_eq_pos.find(head) == d_eq_pos.end()){
01861   begin_pos=0;
01862   d_eq_pos[head]= new(true) CDO<size_t>(theoryCore()->getCM()->getCurrentContext(), 0, 0);
01863   
01864       }
01865       else{
01866   begin_pos = *(d_eq_pos[head]);
01867       } 
01868       for(size_t i=begin_pos; i<cur_eqs->size(); i++){
01869   eqs_hash[(*cur_eqs)[i]]=true;
01870       }
01871       (d_eq_pos[head])->set(cur_eqs->size());
01872     }
01873     }*/
01874   for(size_t i=d_eqs_pos; i<d_eqs.size(); i++){
01875     eqs_hash[d_eqs[i]]=true;
01876   }
01877   d_eqs_pos.set(d_eqs.size());
01878   {
01879     for(ExprMap<bool>::iterator iter = eqs_hash.begin(), iter_end = eqs_hash.end(); iter != iter_end; iter++){
01880       const Expr& cur_ex = iter->first;
01881       ExprMap<CDList<Expr>* >::iterator iter_parent = d_parent_list.find(cur_ex);
01882       if(d_parent_list.end() != iter_parent){
01883   CDList<Expr>* cur_parents = iter_parent->second;
01884   for(size_t i=0; i<cur_parents->size(); i++){
01885     changed_hash[(*cur_parents)[i]]=true;
01886   }
01887       }
01888     }
01889   }
01890   {
01891     for(ExprMap<bool>::iterator iter = changed_hash.begin(), iter_end = changed_hash.end(); iter != iter_end; iter++){
01892       changed.push_back(iter->first);
01893     }
01894   }
01895 }
01896 
01897 inline bool TheoryQuant::matchChild(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env){
01898   if(gterm.arity() != vterm.arity()) {
01899     return false; 
01900   }
01901   for(int i = 0 ; i< gterm.arity(); i++){
01902     const Expr& cur_v = vterm[i];
01903     const Expr& cur_g = gterm[i];
01904     if(BOUND_VAR == cur_v.getKind()){
01905       ExprMap<Expr>::iterator p = env.find(cur_v);
01906       if ( p != env.end()){
01907   if (simplifyExpr(cur_g) != simplifyExpr(p->second)){
01908     return false;
01909   }
01910       }
01911       else {
01912   env[cur_v] = simplifyExpr(cur_g);
01913       }
01914     }
01915     else if (!cur_v.containsBoundVar()){
01916       if(simplifyExpr(cur_v) != simplifyExpr(cur_g)){
01917   return false;
01918       }
01919     }
01920     else{
01921       if (false == recSynMatch(cur_g, cur_v, env)){
01922   return false;
01923       }
01924     }
01925   }
01926   return true;
01927 }
01928 
01929 inline void TheoryQuant::matchChild(const Expr& gterm, const Expr& vterm, vector<ExprMap<Expr> >& binds){
01930   ExprMap<Expr> env;
01931   if(gterm.arity() != vterm.arity()) {
01932     return; 
01933   }
01934   
01935   for(int i = 0 ; i< gterm.arity(); i++){
01936     const Expr& cur_v = vterm[i];
01937     const Expr& cur_g = gterm[i];
01938     if(BOUND_VAR == cur_v.getKind()){
01939       ExprMap<Expr>::iterator p = env.find(cur_v);
01940       if ( p != env.end()){
01941   if (simplifyExpr(cur_g) != simplifyExpr(p->second)){
01942     return;
01943   }
01944       }
01945       else {
01946   env[cur_v] = simplifyExpr(cur_g);
01947       }
01948     }
01949     else if (!cur_v.containsBoundVar()){
01950       if(simplifyExpr(cur_v) != simplifyExpr(cur_g)){
01951   return ;
01952       }
01953     }
01954     else{
01955       if (false == recSynMatch(cur_g, cur_v, env)){
01956   return;
01957       }
01958     }
01959   }
01960   binds.push_back(env);
01961   return;
01962 }
01963 
01964 
01965 
01966 //match a gterm against all the trigs in d_allmap_trigs
01967 void TheoryQuant::matchListOld(const CDList<Expr>& glist, size_t gbegin, size_t gend){
01968   for(size_t g_index = gbegin; g_index < gend; g_index++){
01969 
01970     const Expr& gterm = glist[g_index]; 
01971     if(gterm.isEq()){
01972       continue; // we do not match with equality
01973     }
01974     
01975     Expr head = getHead(gterm);  
01976     
01977     ExprMap<CDMap<Expr, CDList<dynTrig>* > *>::iterator iter = d_allmap_trigs.find(head);
01978     if(d_allmap_trigs.end() == iter) continue;
01979     CDMap<Expr, CDList<dynTrig>*>* cd_map = iter->second;
01980 //     if(cd_map->size()>10){
01981 //       cout<<"map size1:"<<cd_map->size()<<endl;
01982 //       cout<<head<<endl;
01983 //     }
01984 
01985     CDMap<Expr, CDList<dynTrig>*>::iterator iter_trig = (*cd_map).begin();
01986     CDMap<Expr, CDList<dynTrig>*>::iterator iter_trig_end = (*cd_map).end();
01987     
01988     for(;iter_trig != iter_trig_end; iter_trig++){
01989       CDList<dynTrig>* cur_list = (*iter_trig).second;
01990       if(1 == cur_list->size() || null_expr == head || gterm.getType().isBool()){
01991   for(size_t cur_index =0; cur_index < cur_list->size(); cur_index++){
01992   
01993     const Trigger& cur_trig = (*cur_list)[cur_index].trig;
01994     size_t univ_id = (*cur_list)[cur_index].univ_id;
01995     vector<ExprMap<Expr> > binds;
01996     const Expr& vterm = cur_trig.trig;
01997     if  ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans && !cur_trig.isMulti) continue;
01998     //      if  ( d_allout && cur_trig.isSimple ) continue;
01999     newTopMatch(gterm, vterm, binds, cur_trig);
02000     
02001     for(size_t i=0; i<binds.size(); i++){
02002       ExprMap<Expr>& cur_map = binds[i];
02003       vector<Expr> bind_vec;
02004       const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
02005       for(size_t j=0; j< bVarsThm.size(); j++){
02006         bind_vec.push_back(cur_map[bVarsThm[j]]);
02007       }
02008       synNewInst(univ_id, bind_vec, gterm, cur_trig);
02009     }
02010   }
02011       }
02012       else if ( cur_list->size() > 1){
02013   
02014   const Trigger& cur_trig = (*cur_list)[0].trig;//here we have a polarity problem
02015   const Expr& general_vterm = (*iter_trig).first;
02016   vector<ExprMap<Expr> > binds;       
02017   if  ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans && !cur_trig.isMulti) continue;
02018   //if  ( d_allout && cur_trig.isSimple ) continue;
02019   newTopMatch(gterm, general_vterm, binds, cur_trig);
02020   
02021   for(size_t trig_index = 0; trig_index< cur_list->size(); trig_index++){
02022     size_t univ_id = (*cur_list)[trig_index].univ_id;
02023     const ExprMap<Expr>& trig_map = (*cur_list)[trig_index].binds;
02024     const Trigger& ind_cur_trig = (*cur_list)[trig_index].trig;
02025     for(size_t i=0; i<binds.size(); i++){
02026       ExprMap<Expr>& cur_map = binds[i];
02027       vector<Expr> bind_vec;
02028       const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
02029       for(size_t j=0; j< bVarsThm.size(); j++){
02030         const Expr& inter=(*(trig_map.find(bVarsThm[j]))).second;
02031         const Expr& inter2 = cur_map[inter];
02032         bind_vec.push_back(inter2);
02033       }
02034       synNewInst(univ_id, bind_vec, gterm, ind_cur_trig);
02035     }
02036   }
02037       }
02038       else{
02039   FatalAssert(false, "error in matchlistold");
02040       }
02041     }//end of for each trig begins with head
02042   }//end of each gterm
02043 }
02044 
02045 void TheoryQuant::delNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs){
02046   //return;
02047   ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator i = new_trigs.begin();
02048   ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator iend = new_trigs.end();
02049   for(; i!=iend; i++){
02050     ExprMap<std::vector<dynTrig>*>* cur_new_cd_map = i->second;
02051     ExprMap<vector<dynTrig>* >::iterator j = cur_new_cd_map->begin();
02052     ExprMap<vector<dynTrig>* >::iterator jend = cur_new_cd_map->end();
02053       for(; j!=jend; j++){
02054   Expr general_trig = j->first;
02055   vector<dynTrig>* trigs = j->second;
02056   delete trigs;
02057       }
02058       delete cur_new_cd_map;
02059     }
02060   new_trigs.clear();
02061 }
02062 
02063 
02064 void TheoryQuant::combineOldNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs){
02065   ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator i = new_trigs.begin();
02066   ExprMap<ExprMap<std::vector<dynTrig>*>*>::iterator iend = new_trigs.end();
02067   for(; i!=iend; i++){
02068     ExprMap<std::vector<dynTrig>*>* cur_new_cd_map = i->second;
02069     Expr head = i->first;
02070     ExprMap<CDMap<Expr, CDList<dynTrig>* >* >::iterator old_iter = d_allmap_trigs.find(head);
02071     if(d_allmap_trigs.end() == old_iter){
02072       CDMap<Expr, CDList<dynTrig>* >* old_cd_map = 
02073   //  new(true) CDMap<Expr, CDList<dynTrig>* > (theoryCore()->getCM()->getCurrentContext());
02074   new(false) CDMap<Expr, CDList<dynTrig>* > (theoryCore()->getCM()->getCurrentContext());
02075       d_allmap_trigs[head] = old_cd_map;
02076       ExprMap<vector<dynTrig>* >::iterator j = cur_new_cd_map->begin();
02077       ExprMap<vector<dynTrig>* >::iterator jend = cur_new_cd_map->end();
02078       for(; j!=jend; j++){
02079   Expr general_trig = j->first;
02080   vector<dynTrig>* trigs = j->second;
02081   CDList<dynTrig>* old_cd_list =  
02082     //new(true) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
02083     new(false) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
02084   (*old_cd_map)[general_trig] = old_cd_list;
02085   for(size_t k=0; k<trigs->size(); k++){
02086     (*old_cd_list).push_back((*trigs)[k]);
02087     //    cout<<"combined 1 "<<(*trigs)[k].trig.getEx()<<endl;
02088   }
02089   //  delete trigs;
02090       }
02091       //      delete cur_new_cd_map;
02092     }
02093     else{
02094       CDMap<Expr, CDList<dynTrig>* >* old_cd_map = old_iter->second;
02095       ExprMap<std::vector<dynTrig>*>::iterator j = cur_new_cd_map->begin();
02096       ExprMap<std::vector<dynTrig>*>::iterator jend = cur_new_cd_map->end();
02097       for(; j!=jend; j++){
02098   Expr general_trig = j->first;
02099   vector<dynTrig>* trigs = j->second;
02100   CDMap<Expr, CDList<dynTrig>* >::iterator old_trigs_iter = old_cd_map->find(general_trig);
02101   CDList<dynTrig>* old_cd_list;
02102   if(old_cd_map->end() == old_trigs_iter){
02103    old_cd_list = 
02104      //new(true) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
02105      new(false) CDList<dynTrig> (theoryCore()->getCM()->getCurrentContext());
02106    (*old_cd_map)[general_trig] = old_cd_list;
02107   }
02108   else{
02109     old_cd_list = (*old_trigs_iter).second; 
02110   }
02111   for(size_t k=0; k<trigs->size(); k++){
02112     (*old_cd_list).push_back((*trigs)[k]);
02113     //    cout<<"combined 2 "<<(*trigs)[k].trig.getEx()<<endl;
02114   }
02115   //  delete trigs;
02116       }
02117       //      delete cur_new_cd_map;
02118     }
02119   }
02120   delNewTrigs(new_trigs);
02121   //  new_trigs.clear();
02122 }
02123 
02124 //match a gterm against all the trigs in d_allmap_trigs
02125 void TheoryQuant::matchListNew(ExprMap<ExprMap<vector<dynTrig>*>*>& new_trigs,
02126              const CDList<Expr>& glist,
02127              size_t gbegin,
02128              size_t gend){
02129   for(size_t g_index = gbegin; g_index<gend; g_index++){
02130 
02131     const Expr& gterm = glist[g_index]; 
02132   
02133     if(gterm.isEq()){
02134       continue; // we do not match with equality
02135     }
02136     
02137     Expr head = getHead(gterm);  
02138     
02139     ExprMap<ExprMap<vector<dynTrig>* > *>::iterator iter = new_trigs.find(head);
02140     if(new_trigs.end() == iter) continue;
02141     ExprMap<vector<dynTrig>*>* cd_map = iter->second;
02142 //     if(cd_map->size()>10){
02143 //       cout<<"map size2:"<<cd_map->size()<<endl;
02144 //       cout<<head<<endl;
02145 //     }
02146 
02147     ExprMap<vector<dynTrig>*>::iterator iter_trig = (*cd_map).begin();
02148     ExprMap<vector<dynTrig>*>::iterator iter_trig_end = (*cd_map).end();
02149     
02150     for(;iter_trig != iter_trig_end; iter_trig++){
02151       
02152       vector<dynTrig>* cur_list = (*iter_trig).second;
02153       if(1 == cur_list->size() || null_expr == head ||  gterm.getType().isBool()){
02154   for(size_t cur_index =0; cur_index < cur_list->size(); cur_index++){
02155     const Trigger& cur_trig = (*cur_list)[cur_index].trig;
02156     
02157     //  if  ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans) continue;
02158     
02159     size_t univ_id = (*cur_list)[cur_index].univ_id;
02160     vector<ExprMap<Expr> > binds;
02161     const Expr& vterm = cur_trig.trig;
02162     
02163     newTopMatch(gterm, vterm, binds, cur_trig);
02164     for(size_t i=0; i<binds.size(); i++){
02165       ExprMap<Expr>& cur_map = binds[i];
02166       vector<Expr> bind_vec;
02167       const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
02168       for(size_t j=0; j< bVarsThm.size(); j++){
02169         bind_vec.push_back(cur_map[bVarsThm[j]]);
02170       }
02171       synNewInst(univ_id, bind_vec, gterm, cur_trig);
02172     }
02173   }
02174       }
02175       else if ( cur_list->size() > 1){
02176 
02177   const Trigger& cur_trig = (*cur_list)[0].trig;//here we have a polarity problem
02178 
02179   //  if  ( d_allout && cur_trig.isSuperSimple && !cur_trig.hasTrans) continue;
02180   const Expr& general_vterm = (*iter_trig).first;
02181   vector<ExprMap<Expr> > binds;      
02182   newTopMatch(gterm, general_vterm, binds, cur_trig);
02183   
02184   for(size_t trig_index = 0; trig_index< cur_list->size(); trig_index++){
02185     size_t univ_id = (*cur_list)[trig_index].univ_id;
02186     const Trigger& ind_cur_trig = (*cur_list)[trig_index].trig;
02187     const ExprMap<Expr>& trig_map = (*cur_list)[trig_index].binds;
02188     
02189     for(size_t i=0; i<binds.size(); i++){
02190       ExprMap<Expr>& cur_map = binds[i];
02191       vector<Expr> bind_vec;
02192       const vector<Expr>& bVarsThm = d_univs[univ_id].getExpr().getVars();
02193       for(size_t j=0; j< bVarsThm.size(); j++){
02194         const Expr& inter=(*(trig_map.find(bVarsThm[j]))).second;
02195         const Expr& inter2 = cur_map[inter];
02196         bind_vec.push_back(inter2);
02197       }
02198       synNewInst(univ_id, bind_vec, gterm, ind_cur_trig);
02199     }
02200   }
02201       }
02202       else{
02203   FatalAssert(false, "error in matchlistold");
02204       }
02205     }//end of for each trig begins with head
02206   }// end of each gterm
02207 }
02208 
02209 
02210 void TheoryQuant::newTopMatch(const Expr& gterm, 
02211             const Expr& vterm, 
02212             vector<ExprMap<Expr> >& binds, 
02213             const Trigger& trig){
02214   ExprMap<Expr>  cur_bind;
02215   if(trig.isSuperSimple){
02216     for(int i = vterm.arity()-1; i>=0 ; i--){
02217       cur_bind[vterm[i]] = simplifyExpr(gterm[i]);
02218     } 
02219     binds.push_back(cur_bind);
02220     return;
02221   }
02222   
02223   if(trig.isSimple){
02224     for(int i = vterm.arity()-1; i>=0 ; i--){
02225       if(BOUND_VAR != vterm[i].getKind()){
02226   if(simplifyExpr(gterm[i]) != simplifyExpr(vterm[i])) {
02227     return ;
02228   }
02229       }
02230       else{
02231   cur_bind[vterm[i]] = simplifyExpr(gterm[i]);
02232       }
02233     }
02234     binds.push_back(cur_bind);
02235     return;
02236   }
02237 
02238 
02239   if(!isSysPred(vterm)){ //then gterm cannot be a syspred
02240     if(!gterm.getType().isBool()){
02241       //      res2= recSynMatch(gterm, vterm, env);
02242       matchChild(gterm, vterm, binds);
02243       return;
02244     }
02245 
02246     matchChild(gterm, vterm, binds);
02247     return;
02248 
02249   
02250     if(!*d_usePolarity){
02251       //      return recSynMatch(gterm, vterm, env);
02252       matchChild(gterm, vterm, binds);
02253       return;
02254     }
02255     
02256     const bool gtrue = (trueExpr()==findExpr(gterm));
02257     //    const bool gtrue = (trueExpr()==simplifyExpr(gterm));
02258     if(gtrue ){
02259       if((Neg==trig.polarity || PosNeg==trig.polarity)) {
02260   //  return recSynMatch(gterm, vterm, env);
02261   matchChild(gterm, vterm, binds);
02262   return;
02263       }
02264       else{
02265   //  cout<<"returned 1"<<endl;
02266   return;
02267       }
02268     }
02269     const bool gfalse = (falseExpr()==findExpr(gterm));
02270     //const bool gfalse = (falseExpr()==simplifyExpr(gterm));
02271     if(gfalse){
02272       if((Pos==trig.polarity || PosNeg==trig.polarity)) {
02273   //  return recSynMatch(gterm, vterm, env);
02274   matchChild(gterm, vterm, binds); //it is possible that we need binds here, not a single bind
02275   return;
02276       }
02277       else{
02278   //  cout<<"returned 2"<<endl;
02279   return;
02280       }
02281     }
02282 
02283 
02284 //     cout<<"immpossible here in new top match"<<endl;
02285 //     cout<<"vterm "<<vterm<<endl;
02286 //     cout<<trig.polarity<<endl;
02287 //     cout<<gtrue<<" | " <<gfalse<<endl;
02288 //     cout<<"gterm " <<gterm<<endl;
02289 //     cout<<"gterm " <<simplifyExpr(gterm)<<endl;
02290     
02291     matchChild(gterm, vterm, binds);
02292     return;
02293 
02294     return;
02295   }
02296   else{ // must be syspreds
02297     //we can move the work to split vterm into left and right into setuptriggers
02298     Expr gl = getLeft(gterm[1]);
02299     Expr gr = getRight(gterm[1]);
02300     
02301     if(null_expr == gr || null_expr == gl){
02302       gl = gterm[0];
02303       gr = gterm[1];
02304     }
02305     
02306     Expr vr, vl;
02307     Expr tvr, tvl;
02308     
02309     tvr=null_expr;
02310     tvl=null_expr;
02311     
02312     if(isGE(vterm) || isGT(vterm)){
02313       vr = vterm[0];
02314       vl = vterm[1];
02315     }
02316     else if(isLE(vterm) || isLT(vterm)){
02317       vr = vterm[1];
02318       vl = vterm[0];
02319     }
02320     else{
02321       FatalAssert(false, "impossilbe in toppred");
02322     }
02323     
02324     if(isIntx(vl,0)){
02325       tvl = getLeft(vr);
02326       tvr = getRight(vr);
02327     }
02328     else if(isIntx(vr,0)) {
02329       tvl = getLeft(vl);
02330       tvr = getRight(vl);
02331     }
02332     
02333     if( (null_expr != tvl) && (null_expr != tvr)){
02334       vl = tvl;
02335       vr = tvr;
02336     }
02337     
02338     
02339     const bool gtrue = (trueExpr()==findExpr(gterm));
02340     const bool gfalse = (falseExpr()==findExpr(gterm));
02341     
02342     TRACE("quant toppred"," vl, gl, vr, gr:", vl.toString()+"::"+gl.toString()+"||", vr.toString()+"::"+gr.toString());
02343     
02344     //    DebugAssert(!(trig.isNeg() && trig.isPos()), "expr in both pos and neg");
02345     
02346     if(!*d_usePolarity){
02347       if((recSynMatch(gl, vl, cur_bind) && recSynMatch(gr, vr, cur_bind))){
02348   binds.push_back(cur_bind); // it is possible that cur_bind will be binds
02349   return;
02350       }
02351       else{
02352   return;
02353       }
02354     }
02355     if((Neg==trig.polarity || PosNeg==trig.polarity)) {
02356       if (( gtrue ) )  {
02357   if (recSynMatch(gl, vl, cur_bind) && recSynMatch(gr, vr, cur_bind)){
02358     binds.push_back(cur_bind);
02359     return;
02360   }
02361   else{
02362     return;
02363   }
02364       }
02365       else {
02366   if(recSynMatch(gl, vr, cur_bind) && recSynMatch(gr, vl, cur_bind)){
02367     binds.push_back(cur_bind);
02368     return;
02369   }
02370   else{
02371     return;
02372   }
02373       }
02374     }
02375     else if((Pos==trig.polarity || PosNeg==trig.polarity)) {
02376       if (( gfalse )) {
02377   if(recSynMatch(gl, vl, cur_bind) && recSynMatch(gr, vr, cur_bind)){
02378     binds.push_back(cur_bind);
02379     return;
02380   }
02381   else{
02382     return;
02383   }
02384       }
02385       else {
02386   if(recSynMatch(gl, vr, cur_bind) && recSynMatch(gr, vl, cur_bind)){
02387     binds.push_back(cur_bind);
02388     return;
02389   }
02390   else{
02391     return;
02392   }
02393       }
02394     }
02395     else {
02396       FatalAssert(false, "impossible polarity for trig");
02397   //DebugAssert(false, "impossible polarity for trig");
02398 //      res = false;
02399       return;
02400     }
02401   } 
02402 }
02403 
02404 /*
02405 bool TheoryQuant::synMatchTopPred(const Expr& gterm, Trigger trig, ExprMap<Expr>& env){
02406 
02407 
02408   Expr vterm = trig.getEx();
02409 
02410   TRACE("quant toppred", "top pred: gterm:| "+gterm.toString()," vterm:| "+vterm.toString(),"");
02411 
02412   DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
02413   DebugAssert ((BOUND_VAR != vterm.getKind()),"top pred match "+gterm.toString()+" has bound var");
02414 
02415   if(gterm.isEq() || vterm.isEq()){
02416     return false; // we do not match with equality
02417   }
02418 
02419   bool res2=false;
02420   
02421   if(vterm.arity() != gterm.arity()) return false;
02422   
02423   if(trig.isSuperSimp()){
02424     if(trig.getHead() == getHead(gterm) ){
02425       for(int i = vterm.arity()-1; i>=0 ; i--){
02426   env[vterm[i]] = simplifyExpr(gterm[i]);
02427       } 
02428       return true;
02429     }
02430     return false;
02431   }
02432   
02433 
02434 
02435   if(trig.isSimp()){
02436     if(trig.getHead() == getHead(gterm) ){
02437        for(int i = vterm.arity()-1; i>=0 ; i--){
02438   if(BOUND_VAR != vterm[i].getKind()){
02439     if(simplifyExpr(gterm[i]) != simplifyExpr(vterm[i])) {
02440       return false;
02441     }
02442   } 
02443        }
02444       for(int i = vterm.arity()-1; i>=0 ; i--){
02445   if(BOUND_VAR == vterm[i].getKind()){
02446     if(d_allout){
02447       env[vterm[i]] = simplifyExpr(gterm[i]);
02448     }
02449     else {
02450       env[vterm[i]] = simplifyExpr(gterm[i]);
02451     }
02452   } 
02453       }
02454       return true;
02455     }
02456     else{
02457       return false;
02458     }
02459   }
02460 
02461   if(!(isSysPred(vterm) && isSysPred(gterm))){
02462     if(isSysPred(vterm) || isSysPred(gterm)) {
02463       return false;
02464     }
02465     if(!usefulInMatch(gterm)){
02466       return false;
02467     }
02468     if(trig.getHead() != getHead(gterm)){
02469       return false;
02470     }
02471     
02472     if(!gterm.getType().isBool()){
02473       //      res2= recSynMatch(gterm, vterm, env);
02474       res2= matchChild(gterm, vterm, env);
02475       return res2;
02476     }
02477     
02478     if(!*d_usePolarity){
02479       //      return recSynMatch(gterm, vterm, env);
02480       return matchChild(gterm, vterm, env);
02481     }
02482     
02483     const bool gtrue = (trueExpr()==findExpr(gterm));
02484     if(gtrue ){
02485       if(trig.isNeg()) {
02486   //  return recSynMatch(gterm, vterm, env);
02487   return matchChild(gterm, vterm, env);
02488       }
02489       else{
02490   return false;
02491       }
02492     }
02493     const bool gfalse = (falseExpr()==findExpr(gterm));
02494     if(gfalse){
02495       if (trig.isPos()){
02496   //  return recSynMatch(gterm, vterm, env);
02497   return matchChild(gterm, vterm, env);
02498       }
02499       else{
02500   return false;
02501       }
02502     }
02503     else {
02504       return false;
02505     }
02506   }
02507   else{
02508     DebugAssert((2==gterm.arity() && 2==vterm.arity()), "impossible situation in top pred");
02509     DebugAssert(!((isLE(gterm) || isLT(gterm)) && !isIntx(gterm[0],0)), "canonical form changed");
02510     
02511 #ifdef DEBUG
02512     if( CVC3::debugger.trace("quant toppred")  ){
02513       cout << "toppred gterm, vterm" << gterm << "::" << vterm << endl;
02514       cout << findExpr(gterm) << "::" << trig.isPos() << "|" << trig.isNeg() << endl;
02515     }
02516 #endif
02517     
02518     
02519     Expr gl = getLeft(gterm[1]);
02520     Expr gr = getRight(gterm[1]);
02521     
02522     if(null_expr == gr || null_expr == gl){
02523       gl = gterm[0];
02524       gr = gterm[1];
02525     }
02526     
02527     Expr vr, vl;
02528     Expr tvr, tvl;
02529     
02530     tvr=null_expr;
02531     tvl=null_expr;
02532     
02533     if(isGE(vterm) || isGT(vterm)){
02534       vr = vterm[0];
02535       vl = vterm[1];
02536     }
02537     else if(isLE(vterm) || isLT(vterm)){
02538       vr = vterm[1];
02539       vl = vterm[0];
02540     }
02541     else{
02542       DebugAssert(false, "impossilbe in toppred");
02543     }
02544     
02545     if(isIntx(vl,0)){
02546       tvl = getLeft(vr);
02547       tvr = getRight(vr);
02548     }
02549     else if(isIntx(vr,0)) {
02550       tvl = getLeft(vl);
02551       tvr = getRight(vl);
02552     }
02553     
02554     if( (null_expr != tvl) && (null_expr != tvr)){
02555       vl = tvl;
02556       vr = tvr;
02557     }
02558     
02559     
02560     const bool gtrue = (trueExpr()==findExpr(gterm));
02561     const bool gfalse = (falseExpr()==findExpr(gterm));
02562     
02563     TRACE("quant toppred"," vl, gl, vr, gr:", vl.toString()+"::"+gl.toString()+"||", vr.toString()+"::"+gr.toString());
02564     
02565     bool res;
02566     
02567     DebugAssert(!(trig.isNeg() && trig.isPos()), "expr in both pos and neg");
02568     
02569     if(!*d_usePolarity){
02570       return (recSynMatch(gl, vl, env) && recSynMatch(gr, vr, env));
02571     }
02572     
02573     if(trig.isNeg()){
02574       if (( gtrue ) )  {
02575   res=(recSynMatch(gl, vl, env) && recSynMatch(gr, vr, env));
02576       }
02577       else {
02578   res=(recSynMatch(gl, vr, env) && recSynMatch(gr, vl, env));
02579       }
02580     }
02581     else if(trig.isPos()){
02582       if (( gfalse )) {
02583   res=(recSynMatch(gl, vl, env) && recSynMatch(gr, vr, env)); 
02584       }
02585       else {
02586   res=(recSynMatch(gl, vr, env) && recSynMatch(gr, vl, env));
02587       }
02588     }
02589     else {
02590       DebugAssert(false, "impossible polarity for trig");
02591       res = false;
02592     }
02593     
02594 #ifdef DEBUG
02595     if( CVC3::debugger.trace("quant toppred")  ){
02596       cout<<"res| "<< res << " | " << gtrue << " | " << gfalse << endl;
02597     }
02598 #endif
02599     return res;
02600   }
02601 }
02602 */
02603 
02604 bool TheoryQuant::recSynMatch(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env){
02605   TRACE("quant match", "gterm:| "+gterm.toString()," vterm:| "+vterm.toString(),"");
02606   DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
02607   
02608   if (BOUND_VAR == vterm.getKind() )  {
02609     TRACE("quant match", "bound var found;", vterm.toString(),"");
02610     ExprMap<Expr>::iterator p = env.find(vterm);
02611     if ( p != env.end()){
02612       if (simplifyExpr(gterm) != simplifyExpr(p->second)){ 
02613   return false; 
02614       }
02615       else
02616   return true;
02617     }
02618     else {
02619       env[vterm] = simplifyExpr(gterm);
02620       return true; 
02621     }
02622   }
02623   else if (!vterm.containsBoundVar()){
02624     //    return true;
02625     //    cout<<"vterm and gterm"<<vterm << " # " <<gterm<<endl;
02626     if(simplifyExpr(vterm) == simplifyExpr(gterm)) {
02627       return true;
02628     }
02629     else{
02630       return false;
02631     }
02632   }
02633 
02634   else if(false && isSysPred(vterm) && isSysPred(gterm)){
02635     
02636     TRACE("quant syspred"," vterm, gterm ", vterm.toString()+" :|: ", gterm.toString());
02637     TRACE("quant syspred"," simplified vterm, gterm ", simplifyExpr(vterm).toString()+" :|: ", simplifyExpr(gterm).toString());
02638     FatalAssert(false, "should not be here in synmatch");
02639     exit(3);
02640   }
02641   else{ 
02642       if(canGetHead(vterm)){
02643   Expr vhead = getHead(vterm);
02644   TRACE("quant match", "head vterm:", getHead(vterm), "");
02645   if(vterm.isAtomicFormula()){
02646     if (canGetHead(gterm)) {
02647       if ( vhead != getHead(gterm) ){
02648         return false;
02649       }
02650       return matchChild(gterm, vterm, env);
02651 //      for(int i=vterm.arity()-1; i >= 0; i--){
02652 //        if (false == recSynMatch(gterm[i], vterm[i] , env))
02653 //    return false;
02654 //      }
02655 //      return true;
02656     }
02657     else{
02658       return false;
02659     }
02660   }
02661   if ( (canGetHead(gterm)) && vhead == getHead(gterm)){
02662     //    if(gterm.arity() != vterm.arity()){
02663     //      return false;
02664     //    }
02665 //    for(int i=vterm.arity()-1; i >= 0; i--){
02666 //      if (false == recSynMatch(gterm[i], vterm[i] , env)) {
02667 //        return false;
02668 //      }
02669 //    }
02670 //    return true;
02671     return matchChild(gterm, vterm, env);
02672   }
02673   
02674   if(!*d_useEqu){
02675     return false;
02676   }
02677 
02678   
02679   //  cout<<"==============================="<<endl;
02680   //  cout<<gterm<<" # " <<vterm<<endl;
02681 
02682   /*
02683   { // 
02684     //    std::set<Expr> eq_set;
02685     std::map<Expr,bool> eq_set;
02686     eq_set.clear();
02687     eq_set[gterm]=true;
02688     
02689     std::queue<Expr> eq_queue;
02690 
02691     ExprMap<CDList<Expr>* >::iterator iter = d_eq_list.find(gterm);
02692     
02693     if(iter != d_eq_list.end()){
02694       for(size_t len =0; len< iter->second->size(); len++){
02695         eq_queue.push((*(iter->second))[len]);
02696       }
02697       int count =0;
02698       while(eq_queue.size()>0){
02699         count++;
02700         const Expr& cur = eq_queue.front();
02701         eq_queue.pop();
02702         if(eq_set.find(cur) == eq_set.end()){
02703     if(canGetHead(cur) && getHead(cur) == vhead){
02704 //              cout<<"VTERM: "<<vterm<<endl;
02705 //              cout<<"FOUND: "<<cur<<endl;
02706 //              cout<<"GTERM:  "<<gterm<<endl;
02707       //      cout<<"--good match: " << count << "  // " << gterm << " # " << cur << endl;
02708       //      cout<<"===good simple: " << count << "  // " << simplifyExpr(gterm) << " # " << simplifyExpr(cur) << endl;
02709 
02710       if(simplifyExpr(cur) != simplifyExpr(gterm)){
02711         // return false;
02712         //        return matchChild(cur, vterm, env);
02713         //        cout<<"en? "<<gterm<<" # " <<cur <<" # " <<vterm<<endl;
02714       }
02715       else{
02716         //        cout<<"--good match: " << count << "  // " << gterm << " # " << cur << endl;
02717         //        cout<<"===good simple: " << count << "  // " << simplifyExpr(gterm) << " # " << simplifyExpr(cur) << endl;
02718         //        return matchChild(cur, vterm, env);
02719       }
02720     }
02721     
02722     eq_set[cur]=true;
02723     ExprMap<CDList<Expr>* >::iterator iter = d_eq_list.find(cur);
02724     
02725     if(iter != d_eq_list.end()){
02726       for(size_t len =0; len< iter->second->size(); len++){
02727         eq_queue.push((*(iter->second))[len]);
02728       }
02729     }
02730         }
02731       }
02732     }
02733     //    return false;
02734   }
02735   */
02736   if( d_same_head_expr.count(vhead) > 0 ) {
02737     const Expr& findGterm = simplifyExpr(gterm);
02738     //if(isIntx(findGterm,0) || isIntx(findGterm,1)) return false;//special for simplify benchmark
02739     TRACE("quant match", "find gterm:", findGterm.toString(),"");
02740     CDList<Expr>* gls = d_same_head_expr[vhead];
02741     /*
02742     { int count =0;
02743       for(size_t i = 0; i<gls->size(); i++){
02744         if (simplifyExpr((*gls)[i]) == findGterm){
02745     count++;
02746         }
02747       }
02748       if(count>1){
02749         cout<<"count " << count << " # " << gls->size() << " | "<<gterm<<endl;
02750         for(size_t i = 0; i<gls->size(); i++){
02751     if (simplifyExpr((*gls)[i]) == findGterm){
02752       cout<<"eq "<<(*gls)[i]<<endl;
02753     }
02754         }
02755       }
02756     }
02757     */
02758     for(size_t i = 0; i<gls->size(); i++){
02759       if (simplifyExpr((*gls)[i]) == findGterm){
02760         TRACE("quant match", "find matched gterm:", (*gls)[i].toString(),"");
02761         DebugAssert((*gls)[i].arity() == vterm.arity(), "gls has different arity");
02762 
02763         const Expr& newgterm = (*gls)[i];
02764         for(int child=vterm.arity()-1; child >= 0 ; child--){
02765     if (false == recSynMatch(newgterm[child], vterm[child] , env)){
02766       TRACE("quant match", "match false", (*gls)[i][child].toString(), vterm[child].toString());
02767       return false;
02768     }
02769         }
02770         TRACE("quant match", "good match, return true:", gterm, vterm.toString());
02771         //        cout<<"quant good match: " <<i<<" // "<<gterm << " # "<<vterm<<endl;
02772         //        cout<<"quant simple: " <<i<<" // "<<simplifyExpr(gterm) << " # "<<vterm<<endl;
02773         return true;
02774       }
02775     }//end of for
02776     return false;
02777   } 
02778   else  {
02779     return false;//end of if
02780   }
02781       }
02782       else{
02783   TRACE("quant match more", "match more", gterm.toString()+" # ", vterm.toString());
02784   if( (gterm.getKind() == vterm.getKind()) && 
02785       (gterm.arity() == vterm.arity()) &&
02786       gterm.arity()>0 ){
02787 //      for(int child=0; child < vterm.arity() ; child++){
02788 //        if (false == recSynMatch(gterm[child], vterm[child] , env)){
02789 //          TRACE("quant match", "match false", gterm[child].toString(), vterm[child].toString());
02790 //          return false;
02791 //        }
02792 //      }
02793 //      return true;
02794 //      if( gterm.getKind() == PLUS || gterm.getKind() == MINUS){
02795 //        cout<<"g v"<<gterm<< " # " <<vterm<<endl;
02796 //      }
02797 
02798     return matchChild(gterm, vterm, env);
02799   }
02800   else {
02801 //      if( gterm.getKind() == PLUS || gterm.getKind() == MINUS){
02802 //      static bool gvfound = false;
02803 //        if(!gvfound){
02804 //        cout<<"g v 1"<<endl;
02805 //        gvfound =true;
02806 //      }
02807       //gterm<< " # " <<vterm<<endl;
02808     //  }
02809     return false;
02810   }
02811       }
02812   }
02813 }
02814 
02815 /*
02816 
02817 bool TheoryQuant::synMatchTopPred(const Expr& gterm, Trigger trig, ExprMap<Expr>& env){
02818 
02819   const Expr vterm = trig.getEx();
02820 
02821   TRACE("quant toppred", "top pred: gterm:| "+gterm.toString()," vterm:| "+vterm.toString(),"");
02822 
02823   DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
02824   DebugAssert ((BOUND_VAR != vterm.getKind()),"top pred match "+gterm.toString()+" has bound var");
02825 
02826   if(gterm.isEq() || vterm.isEq()){
02827     return false; // we do not match with equality
02828   }
02829 
02830   bool res2=false;
02831   
02832   //  if(vterm.arity() != gterm.arity()) return false;
02833 
02834   if(trig.isSimp()){
02835     if(trig.getHead() == getHead(gterm) ){
02836       for(int i = vterm.arity()-1; i>=0 ; i--){
02837   if(BOUND_VAR != vterm[i].getKind()){
02838     if(simplifyExpr(gterm[i]) != simplifyExpr(vterm[i])) {
02839       return false;
02840     }
02841   } 
02842       }
02843       for(int i = vterm.arity()-1; i>=0 ; i--){
02844   if(BOUND_VAR == vterm[i].getKind()){
02845     if(d_allout){
02846       env[vterm[i]] = simplifyExpr(gterm[i]);
02847     }
02848     else {
02849       env[vterm[i]] = simplifyExpr(gterm[i]);
02850     }
02851   } 
02852       }
02853       return true;
02854     }
02855     else{
02856       return false;
02857     }
02858   }
02859 
02860   if(!(isSysPred(vterm) && isSysPred(gterm))){
02861     if(isSysPred(vterm) || isSysPred(gterm)) {
02862       return false;
02863     }
02864     if(!usefulInMatch(gterm)){
02865       return false;
02866     }
02867     if(trig.getHead() != getHead(gterm)){
02868       return false;
02869     }
02870     
02871     if(!gterm.getType().isBool()){
02872       res2= recSynMatch(gterm, vterm, env);
02873       return res2;
02874     }
02875     
02876     if(!*d_usePolarity){
02877       return recSynMatch(gterm, vterm, env);
02878     }
02879     
02880     const bool gtrue = (trueExpr()==findExpr(gterm));
02881     if(gtrue ){
02882       if(trig.isNeg()) {
02883   return recSynMatch(gterm, vterm, env);
02884       }
02885       else{
02886   return false;
02887       }
02888     }
02889     const bool gfalse = (falseExpr()==findExpr(gterm));
02890     if(gfalse){
02891       if (trig.isPos()){
02892   return recSynMatch(gterm, vterm, env);
02893       }
02894       else{
02895   return false;
02896       }
02897     }
02898     else {
02899       return false;
02900     }
02901   }
02902   else{
02903     DebugAssert((2==gterm.arity() && 2==vterm.arity()), "impossible situation in top pred");
02904     DebugAssert(!((isLE(gterm) || isLT(gterm)) && !isIntx(gterm[0],0)), "canonical form changed");
02905     
02906 #ifdef DEBUG
02907     if( CVC3::debugger.trace("quant toppred")  ){
02908       cout << "toppred gterm, vterm" << gterm << "::" << vterm << endl;
02909       cout << findExpr(gterm) << "::" << trig.isPos() << "|" << trig.isNeg() << endl;
02910     }
02911 #endif
02912     
02913     
02914     Expr gl = getLeft(gterm[1]);
02915     Expr gr = getRight(gterm[1]);
02916     
02917     if(null_expr == gr || null_expr == gl){
02918       gl = gterm[0];
02919       gr = gterm[1];
02920     }
02921     
02922     Expr vr, vl;
02923     Expr tvr, tvl;
02924     
02925     tvr=null_expr;
02926     tvl=null_expr;
02927     
02928     if(isGE(vterm) || isGT(vterm)){
02929       vr = vterm[0];
02930       vl = vterm[1];
02931     }
02932     else if(isLE(vterm) || isLT(vterm)){
02933       vr = vterm[1];
02934       vl = vterm[0];
02935     }
02936     else{
02937       DebugAssert(false, "impossilbe in toppred");
02938     }
02939     
02940     if(isIntx(vl,0)){
02941       tvl = getLeft(vr);
02942       tvr = getRight(vr);
02943     }
02944     else if(isIntx(vr,0)) {
02945       tvl = getLeft(vl);
02946       tvr = getRight(vl);
02947     }
02948     
02949     if( (null_expr != tvl) && (null_expr != tvr)){
02950       vl = tvl;
02951       vr = tvr;
02952     }
02953     
02954     
02955     const bool gtrue = (trueExpr()==findExpr(gterm));
02956     const bool gfalse = (falseExpr()==findExpr(gterm));
02957     
02958     TRACE("quant toppred"," vl, gl, vr, gr:", vl.toString()+"::"+gl.toString()+"||", vr.toString()+"::"+gr.toString());
02959     
02960     bool res;
02961     
02962     DebugAssert(!(trig.isNeg() && trig.isPos()), "expr in both pos and neg");
02963     
02964     if(!*d_usePolarity){
02965       return (recSynMatch(gl, vl, env) && recSynMatch(gr, vr, env));
02966     }
02967     
02968     if(trig.isNeg()){
02969       if (( gtrue ) )  {
02970   res=(recSynMatch(gl, vl, env) && recSynMatch(gr, vr, env));
02971       }
02972       else {
02973   res=(recSynMatch(gl, vr, env) && recSynMatch(gr, vl, env));
02974       }
02975     }
02976     else if(trig.isPos()){
02977       if (( gfalse )) {
02978   res=(recSynMatch(gl, vl, env) && recSynMatch(gr, vr, env)); 
02979       }
02980       else {
02981   res=(recSynMatch(gl, vr, env) && recSynMatch(gr, vl, env));
02982       }
02983     }
02984     else {
02985       DebugAssert(false, "impossible polarity for trig");
02986       res = false;
02987     }
02988     
02989 #ifdef DEBUG
02990     if( CVC3::debugger.trace("quant toppred")  ){
02991       cout<<"res| "<< res << " | " << gtrue << " | " << gfalse << endl;
02992     }
02993 #endif
02994     return res;
02995   }
02996 }
02997 
02998 bool TheoryQuant::recSynMatch(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env){
02999   TRACE("quant match", "gterm:| "+gterm.toString()," vterm:| "+vterm.toString(),"");
03000   DebugAssert ((BOUND_VAR != gterm.getKind()),"gound term "+gterm.toString()+" has bound var");
03001   
03002   if (BOUND_VAR == vterm.getKind())  {
03003     TRACE("quant match", "bound var found;", vterm.toString(),"");
03004     ExprMap<Expr>::iterator p = env.find(vterm);
03005     if ( p != env.end()){
03006       if (simplifyExpr(gterm) != simplifyExpr(p->second)){ 
03007   return false; 
03008       }
03009       else
03010   return true;
03011     }
03012     else {
03013       env[vterm] = simplifyExpr(gterm);
03014       return true; 
03015     }
03016   }
03017   else if (!vterm.containsBoundVar()){
03018     if(simplifyExpr(vterm) == simplifyExpr(gterm)) {
03019       return true;
03020     }
03021     else{
03022       return false;
03023     }
03024   }
03025 
03026   else if(false && isSysPred(vterm) && isSysPred(gterm)){
03027     
03028     TRACE("quant syspred"," vterm, gterm ", vterm.toString()+" :|: ", gterm.toString());
03029     TRACE("quant syspred"," simplified vterm, gterm ", simplifyExpr(vterm).toString()+" :|: ", simplifyExpr(gterm).toString());
03030     FatalAssert(false, "should not be here in synmatch");
03031     exit(3);
03032   }
03033   else{ 
03034       if(canGetHead(vterm)){
03035   Expr vhead = getHead(vterm);
03036   TRACE("quant match", "head vterm:", getHead(vterm), "");
03037   if(vterm.isAtomicFormula()){
03038     if (canGetHead(gterm)) {
03039       if ( vhead != getHead(gterm) ){
03040         return false;
03041       }
03042       for(int i=vterm.arity()-1; i >= 0; i--){
03043         if (false == recSynMatch(gterm[i], vterm[i] , env))
03044     return false;
03045       }
03046       return true;
03047     }
03048     else{
03049       return false;
03050     }
03051   }
03052   if ( (canGetHead(gterm)) && vhead == getHead(gterm)){
03053     if(gterm.arity() != vterm.arity()){
03054       return false;
03055     }
03056     for(int i=vterm.arity()-1; i >= 0; i--){
03057       if (false == recSynMatch(gterm[i], vterm[i] , env)) {
03058         return false;
03059       }
03060     }
03061     return true;
03062   }
03063   
03064   if(false && !*d_useEqu){
03065     return false;
03066   }
03067 
03068   if( d_same_head_expr.count(vhead) > 0 ) {
03069     const Expr& findGterm = simplifyExpr(gterm);
03070     //if(isIntx(findGterm,0) || isIntx(findGterm,1)) return false;//special for simplify benchmark
03071     TRACE("quant match", "find gterm:", findGterm.toString(),"");
03072     CDList<Expr>* gls = d_same_head_expr[vhead];
03073     for(size_t i = 0; i<gls->size(); i++){
03074       if (simplifyExpr((*gls)[i]) == findGterm){
03075         TRACE("quant match", "find matched gterm:", (*gls)[i].toString(),"");
03076         DebugAssert((*gls)[i].arity() == vterm.arity(), "gls has different arity");
03077 
03078         for(int child=vterm.arity()-1; child >= 0 ; child--){
03079     const Expr& newgterm = (*gls)[i];
03080     if (false == recSynMatch(newgterm[child], vterm[child] , env)){
03081       TRACE("quant match", "match false", (*gls)[i][child].toString(), vterm[child].toString());
03082       return false;
03083     }
03084         }
03085         TRACE("quant match", "good match, return true:", gterm, vterm.toString());
03086         return true;
03087       }
03088     }//end of for
03089     return false;
03090   } 
03091   else  {
03092     return false;//end of if
03093   }
03094       }
03095       else{
03096   TRACE("quant match more", "match more", gterm.toString()+" # ", vterm.toString());
03097   if( (gterm.getKind() == vterm.getKind()) && 
03098       (gterm.arity() == vterm.arity()) &&
03099       gterm.arity()>0 ){
03100     for(int child=0; child < vterm.arity() ; child++){
03101       if (false == recSynMatch(gterm[child], vterm[child] , env)){
03102         TRACE("quant match", "match false", gterm[child].toString(), vterm[child].toString());
03103         return false;
03104       }
03105     }
03106     return true;
03107   }
03108   else  return false;
03109       }
03110   }
03111 }
03112 
03113 */
03114 
03115 void TheoryQuant::goodSynMatch(const Expr& e,
03116              const std::vector<Expr> & boundVars,
03117              std::vector<std::vector<Expr> >& instBinds,
03118              std::vector<Expr>& instGterms,
03119              const CDList<Expr>& allterms,           
03120              size_t tBegin){
03121   for (size_t i=tBegin; i<allterms.size(); i++)    {
03122     Expr gterm = allterms[i];
03123     if (0 == gterm.arity() )
03124       continue;
03125     TRACE("quant matching", gterm.toString(), "||", e.toString()) ;
03126     //    if( usefulInMatch(gterm) && possibleMatch(gterm,e))   {
03127     if(usefulInMatch(gterm))   {
03128       ExprMap<Expr> env;
03129       env.clear();
03130       bool found = recSynMatch(gterm,e,env); 
03131       if(found){
03132   
03133   TRACE("quant matching found", " good:",gterm.toString()+" to " , e.toString());
03134   TRACE("quant matching found", " simplified good:",simplifyExpr(gterm).toString()+" to " , simplifyExpr(e).toString());
03135   std::vector<Expr> inst;
03136   
03137   DebugAssert((boundVars.size() == env.size()),"bound var size != env.size()");
03138   
03139   for(size_t i=0; i<boundVars.size(); i++) {
03140     ExprMap<Expr>::iterator p = env.find(boundVars[i]);
03141     DebugAssert((p!=env.end()),"bound var cannot be found");
03142     inst.push_back(p->second);
03143   }
03144   instBinds.push_back(inst);
03145   instGterms.push_back(gterm);
03146       }
03147       else{
03148   TRACE("quant matching", "bad one",gterm.toString()+" to " , e.toString());
03149       }
03150     }
03151   }
03152 }
03153  
03154 /*
03155 void TheoryQuant::goodSynMatchNewTrig(const Trigger& trig,
03156               const std::vector<Expr> & boundVars,
03157               std::vector<std::vector<Expr> >& instBinds,
03158               std::vector<Expr>& instGterms,
03159               const CDList<Expr>& allterms,          
03160               size_t tBegin){
03161   for (size_t i=tBegin; i<allterms.size(); i++)    {
03162     Expr gterm (allterms[i]);
03163     //    TRACE("quant matching", gterm.toString(), "||", trig.getEx().toString()) ;
03164     if(usefulInMatch(gterm)) {
03165       ExprMap<Expr> env;
03166       env.clear();
03167       bool found = synMatchTopPred(gterm,trig,env); 
03168       if(found){
03169   //TRACE("quant matching found", " top good:",gterm.toString()+" to " , trig.getEx().toString());
03170   std::vector<Expr> inst;
03171   inst.clear();
03172   DebugAssert((boundVars.size() <= env.size()),"bound var size != env.size()");
03173 
03174   for(size_t i=0; i<boundVars.size(); i++) {
03175     ExprMap<Expr>::iterator p = env.find(boundVars[i]);
03176     DebugAssert((p!=env.end()),"bound var cannot be found");
03177     inst.push_back(p->second);
03178   }
03179   
03180   instBinds.push_back(inst);
03181   instGterms.push_back(gterm);
03182       }
03183       else{
03184   //  TRACE("quant matching", "bad one",gterm.toString()+" to ", trig.getEx().toString());
03185       }
03186     }
03187   }
03188 }
03189 */
03190 
03191 /*
03192 bool TheoryQuant::hasGoodSynInstNewTrigOld(Trigger& trig,
03193              std::vector<Expr> & boundVars,
03194              std::vector<std::vector<Expr> >& instBinds,
03195              std::vector<Expr>& instGterms,
03196              const CDList<Expr>& allterms,           
03197              size_t tBegin){
03198 
03199   const std::set<Expr>& bvs = getBoundVars(trig.getEx());
03200   
03201   boundVars.clear();
03202   for(std::set<Expr>::const_iterator i=bvs.begin(),iend=bvs.end(); i!=iend; ++i)
03203     boundVars.push_back(*i);
03204   
03205   instBinds.clear();
03206   goodSynMatchNewTrig(trig, boundVars, instBinds, instGterms, allterms, tBegin);
03207   
03208   if (instBinds.size() > 0)
03209     return true;
03210   else
03211     return false;    
03212 }
03213 
03214 
03215 bool TheoryQuant::hasGoodSynInstNewTrig(Trigger& trig,
03216           const std::vector<Expr>& boundVars,
03217           std::vector<std::vector<Expr> >& instBinds,
03218           std::vector<Expr>& instGterms,
03219           const CDList<Expr>& allterms,          
03220           size_t tBegin){
03221 //   boundVars=trig.getBVs();
03222 //   const std::set<Expr>& bvs = getBoundVars(trig.getEx());
03223   
03224 //   boundVars.clear();
03225 //   for(std::set<Expr>::const_iterator i=bvs.begin(),iend=bvs.end(); i!=iend; ++i)
03226 //     boundVars.push_back(*i);
03227   
03228   instBinds.clear();
03229   goodSynMatchNewTrig(trig, boundVars, instBinds, instGterms, allterms, tBegin);
03230   
03231   if (instBinds.size() > 0)
03232     return true;
03233   else
03234     return false;    
03235 }
03236 */
03237 int TheoryQuant::loc_gterm(const std::vector<Expr>& border,
03238          const Expr& vterm, 
03239          int pos){
03240   const std::vector<Expr>& order = d_mtrigs_bvorder[vterm];
03241   const Expr& var = order[pos];
03242   for(size_t i=0; i<border.size(); i++){
03243     if (border[i] == var) return i;
03244   }
03245 
03246   DebugAssert(false, "internal error in loc_germ");
03247   return -1;
03248 }
03249 
03250 void  TheoryQuant::recSearchCover(const std::vector<Expr>& border,
03251           const std::vector<Expr>& mtrigs, 
03252           int cur_depth, 
03253           std::vector<std::vector<Expr> >& instSet,
03254           std::vector<Expr>& cur_inst
03255           ){
03256   int max_dep = mtrigs.size();
03257 
03258   if(cur_depth >= max_dep) return; 
03259 
03260   Expr cur_vterm = mtrigs[cur_depth]; //get the current vterm
03261   if(d_mtrigs_inst.count(cur_vterm) <=0) return;
03262   CDList<std::vector<Expr> >* gterm_list = d_mtrigs_inst[cur_vterm]; // get the list of ground term found for cur_vterm
03263   for(size_t i=0; i< gterm_list->size(); i++){
03264     const std::vector<Expr>& cur_gterm = (*gterm_list)[i];
03265     std::vector<Expr> new_inst(border.size()); //get a new inst array
03266     
03267     for(size_t j=0; j< border.size(); j++){
03268       new_inst[j]=cur_inst[j]; //copy to cur_int to new_inst
03269     }
03270     
03271     bool has_problem = false;//next, try to put the cur gterm into new_inst
03272     for(size_t j=0; j< cur_gterm.size(); j++){
03273       int cur_loc_gterm = loc_gterm(border, cur_vterm, j);
03274       
03275       if( null_expr == new_inst[cur_loc_gterm]){
03276   new_inst[cur_loc_gterm] = cur_gterm[j];
03277       }
03278       else if (new_inst[cur_loc_gterm] != cur_gterm[j]){
03279   has_problem = true;
03280   break;
03281       }
03282       
03283     }
03284     
03285     if (has_problem){
03286       continue;
03287     }
03288 
03289     bool finished = true;
03290     for(size_t j=0; j< border.size() ;j++){
03291       if(null_expr == new_inst[j]){
03292   finished = false;
03293   break;
03294       }
03295     }
03296     
03297     if(finished){
03298       std::vector<Expr> good_inst;
03299       for(size_t j=0; j<border.size(); j++){
03300   good_inst.push_back(new_inst[j]);
03301       }
03302       instSet.push_back(good_inst);
03303     }
03304     else{
03305       recSearchCover(border,
03306          mtrigs, 
03307          cur_depth+1, 
03308          instSet,
03309          new_inst);
03310     }
03311   }//end of for
03312 }
03313 
03314 void  TheoryQuant::searchCover(const Expr& thm,
03315              const std::vector<Expr>& border,
03316              std::vector<std::vector<Expr> >& instSet
03317              ){
03318   std::vector<Expr> dumy(border.size()) ; //use dynamic array here
03319   for(size_t j=0; j< border.size() ;j++){
03320     dumy[j]=null_expr;
03321   }
03322   const std::vector<Expr>& mtrigs = d_multTriggers[thm];
03323   recSearchCover(border, mtrigs, 0, instSet, dumy);
03324 }
03325 
03326 bool TheoryQuant::hasGoodSynMultiInst(const Expr& thm,
03327               std::vector<Expr> & boundVars,
03328               std::vector<std::vector<Expr> >& instSet,
03329               const CDList<Expr>& allterms,          
03330               size_t tBegin){
03331 
03332   const std::set<Expr>& bvs = getBoundVars(thm);
03333   
03334   boundVars.clear();
03335   for(std::set<Expr>::const_iterator i=bvs.begin(),iend=bvs.end(); i!=iend; ++i)
03336     boundVars.push_back(*i);
03337   
03338   instSet.clear();
03339   
03340   bool new_match = false;
03341   //assumption: every trig is different
03342   //this is not true later, fix this asap
03343   const std::vector<Expr>& mtrigs = d_multTriggers[thm];
03344   
03345   for(std::vector<Expr>::const_iterator i= mtrigs.begin(), iend = mtrigs.end(); i != iend; i++){
03346 
03347     if(d_mtrigs_bvorder[*i].empty()){ //setup an order
03348       const std::set<Expr>& trig_bvs = getBoundVars(*i);
03349       for(std::set<Expr>::const_iterator j= trig_bvs.begin(), jend = trig_bvs.end();
03350     j != jend;
03351     j++){
03352   d_mtrigs_bvorder[*i].push_back(*j);
03353       }
03354     }
03355     
03356     const std::vector<Expr>& trig_bvorder = d_mtrigs_bvorder[*i];
03357     //    std::set<std::vector<Expr> > trig_insts;    
03358     std::vector<std::vector<Expr> > trig_insts;    
03359     trig_insts.clear();
03360 
03361     std::vector<Expr> gtms;
03362     goodSynMatch(*i, trig_bvorder, trig_insts, gtms, allterms, tBegin);
03363 
03364     if (trig_insts.size() > 0){
03365       new_match=true;
03366       if(d_mtrigs_inst.count(*i) <= 0){
03367   d_mtrigs_inst[*i] = new(true) CDList<std::vector<Expr> > (theoryCore()->getCM()->getCurrentContext());
03368       }
03369       for(std::vector<std::vector<Expr> >::const_iterator j = trig_insts.begin(), jend = trig_insts.end();
03370     j != jend;
03371     j++){
03372   
03373   d_mtrigs_inst[*i]->push_back(*j);
03374   for(std::vector<Expr>::const_iterator k = j->begin(), kend = j->end();
03375       k != kend;
03376       k++){
03377   }
03378       }
03379     }
03380   } // end of for
03381 
03382   for(std::vector<Expr>::const_iterator i= mtrigs.begin(), iend = mtrigs.end(); i != iend; i++){
03383     if (d_mtrigs_inst.count(*i) <=0 ) continue;
03384     for(CDList<std::vector<Expr> >::const_iterator j = d_mtrigs_inst[*i]->begin(), 
03385     jend = d_mtrigs_inst[*i]->end();
03386     j != jend;
03387     j++){
03388       
03389       for(std::vector<Expr>::const_iterator k = j->begin(), kend = j->end();
03390     k != kend;
03391     k++){
03392       }
03393     }
03394   }
03395   {//code for search a cover
03396     if(new_match){
03397       searchCover(thm, boundVars, instSet);
03398     }
03399   }      
03400 
03401   if(instSet.size() > 0 ) {
03402     return true;
03403   }
03404   else {
03405     return false;
03406   }
03407   
03408 }
03409 
03410 bool inStrCache(std::set<std::string> cache, std::string str){
03411   return (cache.find(str) != cache.end());
03412 } 
03413 
03414 
03415 bool TheoryQuant::hasGoodSemInst(const Expr& e,
03416          std::vector<Expr> & boundVars,
03417          std::set<std::vector<Expr> >& instSet,
03418          size_t tBegin){
03419   return false;
03420 }
03421 
03422 void genPartInstSetThm(const std::vector<Expr>&  bVarsThm,
03423            std::vector<Expr>& bVarsTerm,
03424            const std::vector<std::vector<Expr> >& termInst,
03425            std::vector<std::vector<Expr> >& instSetThm){
03426   ExprMap<bool> bVmap;
03427 
03428   for(size_t i=0; i< bVarsThm.size(); ++i)    {
03429     bVmap[bVarsThm[i]]=true;
03430   }
03431 
03432   std::vector<Expr> tempBVterm;
03433   std::vector<int> locTerm;
03434 
03435   for (size_t j=0; j<bVarsTerm.size(); j++){
03436     if (bVmap.count(bVarsTerm[j]) > 0){
03437       locTerm.push_back(1);
03438       tempBVterm.push_back(bVarsTerm[j]);
03439     }
03440     else{
03441       locTerm.push_back(0);
03442     }
03443   }
03444 
03445   DebugAssert(locTerm.size() == bVarsTerm.size(), "locTerm.size !- bVarsTerm.size()");
03446 
03447   for(std::vector<std::vector<Expr> >::const_iterator i=termInst.begin(),
03448   iend=termInst.end();i!=iend; i++)  {
03449     std::vector<Expr> buf;
03450     buf.clear();
03451     for(size_t j=0; j< bVarsTerm.size(); ++j){
03452       if(locTerm[j])
03453   buf.push_back((*i)[j]);
03454     }
03455     instSetThm.push_back(buf);
03456   }
03457   bVarsTerm=tempBVterm;
03458 }
03459 
03460 
03461 void genInstSetThm(const std::vector<Expr>& bVarsThm,
03462        const std::vector<Expr>& bVarsTerm,
03463        const std::vector<std::vector<Expr> >& termInst,
03464        std::vector<std::vector<Expr> >& instSetThm){
03465 
03466   std::vector<int> bVmap;
03467 
03468   for(size_t i=0; i< bVarsThm.size(); ++i)    {
03469     bVmap.push_back(-1);
03470     for (size_t j=0; j<bVarsTerm.size(); j++){
03471       if (bVarsThm[i] == bVarsTerm[j]){
03472   DebugAssert(bVmap[i] == -1, "bVmap[1] != -1");
03473   bVmap[i]=j;       
03474       }
03475     }
03476   }
03477   
03478   for(size_t i=0; i< bVarsThm.size(); ++i)
03479     if( -1 == bVmap[i])  {
03480       return;
03481     }
03482   
03483   for(std::vector<std::vector<Expr> >::const_iterator i=termInst.begin(),
03484   iend=termInst.end();i!=iend; i++)  {
03485     std::vector<Expr> buf;
03486     buf.clear();
03487     for(size_t j=0; j< bVarsThm.size(); ++j){
03488       buf.push_back((*i)[bVmap[j]]);
03489     }
03490     instSetThm.push_back(buf);
03491   }
03492 }
03493   
03494 
03495 /*
03496 void TheoryQuant::synInst(const Theorem & univ, const CDList<Expr>& allterms, size_t tBegin ){
03497   if(d_useFullTrig){
03498     synFullInst(univ, allterms, tBegin);
03499   }
03500 
03501   if(d_useMultTrig){
03502     synMultInst(univ, allterms, tBegin);
03503   }
03504 
03505   if(d_usePartTrig){
03506     synPartInst(univ, allterms, tBegin);
03507   }
03508 }
03509 */
03510 inline bool TheoryQuant::transFound(const Expr& comb){
03511   return (d_trans_found.count(comb) > 0);
03512 }
03513 
03514 inline void TheoryQuant::setTransFound(const Expr& comb){
03515   d_trans_found[comb] = true;
03516 }
03517 
03518 inline bool TheoryQuant::trans2Found(const Expr& comb){
03519   return (d_trans2_found.count(comb) > 0);
03520 }
03521 
03522 inline void TheoryQuant::setTrans2Found(const Expr& comb){
03523   d_trans2_found[comb] = true;
03524 }
03525 
03526 
03527 inline CDList<Expr> & TheoryQuant::backList(const Expr& ex){
03528   if(d_trans_back.count(ex)>0){
03529     return *d_trans_back[ex];
03530   }
03531   else{
03532     return null_cdlist;
03533   } 
03534 } 
03535 
03536 inline CDList<Expr> & TheoryQuant::forwList(const Expr& ex){
03537   if(d_trans_forw.count(ex)>0){
03538     return *d_trans_forw[ex];
03539   }
03540   else{
03541     return null_cdlist;
03542   } 
03543 } 
03544 
03545 inline void  TheoryQuant::pushBackList(const Expr& node, Expr ex){
03546   if(d_trans_back.count(node)>0){
03547     d_trans_back[node]->push_back(ex);
03548   }
03549   else{
03550     d_trans_back[node] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext());
03551     d_trans_back[node]->push_back(ex);
03552   } 
03553 } 
03554 
03555 inline void  TheoryQuant::pushForwList(const Expr& node, Expr ex){
03556   if(d_trans_forw.count(node)>0){
03557     d_trans_forw[node]->push_back(ex);
03558   }
03559   else{
03560     d_trans_forw[node] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext());
03561     d_trans_forw[node]->push_back(ex);
03562   } 
03563 } 
03564 
03565 /*
03566 void TheoryQuant::synFullInst(const Theorem & univ, const CDList<Expr>& allterms, size_t tBegin ){
03567 
03568   const Expr& quantExpr = univ.getExpr();  
03569   //  const std::vector<Expr>& bVarsThm = quantExpr.getVars();
03570   std::vector<Expr> bVarsThm = quantExpr.getVars();
03571 
03572   TRACE("quant inst", "try full inst with:|", quantExpr.toString() , " ");
03573   
03574   std::vector<std::vector<Expr> > instBindsThm; //set of instantiations for the thm,
03575   std::vector<std::vector<Expr> > instBindsTerm; //bindings, in the order of bVarsTrig
03576   std::vector<Expr > instGterms; //instGterms are gterms matched, instBindsTerm and instGterms must have the same length
03577   std::vector<Expr> bVarsTrig; 
03578 
03579   if(*d_useTrigNew){
03580     std::vector<Trigger>& new_trigs=d_fullTrigs[quantExpr];
03581     for( size_t i= 0; i<new_trigs.size(); i++)  {
03582       Trigger& trig = new_trigs[i];
03583       //      if( 0 != trig.getPri()) continue;
03584       TRACE("quant inst","try new full trigger:|", trig.getEx().toString(),"");
03585       
03586       instBindsTerm.clear();
03587       bVarsTrig.clear();
03588       instBindsThm.clear();
03589       instGterms.clear();
03590       
03591       {//code for trans2
03592   if(trig.hasTr2()){
03593     //if(hasGoodSynInstNewTrig(trig, bVarsTrig, instBindsTerm, instGterms, allterms, tBegin)) {
03594     if(hasGoodSynInstNewTrig(trig, trig.getBVs(), instBindsTerm, instGterms, allterms, tBegin)) {
03595       for(size_t j=0; j<instBindsTerm.size(); j++){
03596         DebugAssert(2 == instBindsTerm[j].size(), "internal error in trans2");
03597 
03598         Expr& gterm = instGterms[j];
03599         
03600         if(simplifyExpr(instBindsTerm[j][0]) != simplifyExpr(instBindsTerm[j][1])){
03601     Expr comb = Expr(RAW_LIST,instBindsTerm[j][0],instBindsTerm[j][1]);
03602     if(!trans2Found(comb)){
03603       setTrans2Found(comb);
03604       
03605       TRACE("quant trans","new trans2: ", vectorExpr2string(instBindsTerm[j]), "");     
03606       
03607       Expr comb_rev = Expr(RAW_LIST,instBindsTerm[j][1],instBindsTerm[j][0]);
03608       if(trans2Found(comb_rev)){
03609         Expr sr(instBindsTerm[j][0]);
03610         Expr dt(instBindsTerm[j][1]);
03611         
03612         vector<Expr> bind;
03613         bind.clear();
03614         bind.push_back(sr);
03615         bind.push_back(dt);
03616         
03617         enqueueInst(univ, bind, gterm);
03618         TRACE("quant inst", "trans pred rule2 ", univ.toString(), " | with bind: "+vectorExpr2string(bind));          TRACE("quant trans", "trans2 ", vectorExpr2string(bind), "");
03619       }
03620     }
03621         } 
03622       }
03623     }
03624     return;
03625   }
03626       }
03627             
03628       {//code for trans pred
03629   if(trig.hasTr()){
03630     //    if(hasGoodSynInstNewTrig(trig, bVarsTrig, instBindsTerm, instGterms, allterms, tBegin)) {
03631     if(hasGoodSynInstNewTrig(trig, trig.getBVs(), instBindsTerm, instGterms, allterms, tBegin)) {
03632       for(size_t j=0; j<instBindsTerm.size(); j++){
03633         DebugAssert(2 == instBindsTerm[j].size(), "internal error in trans");
03634 
03635         Expr& gterm = instGterms[j];
03636 
03637         if(simplifyExpr(instBindsTerm[j][0]) != simplifyExpr(instBindsTerm[j][1])){
03638 
03639     Expr comb = Expr(RAW_LIST,instBindsTerm[j][0],instBindsTerm[j][1]);
03640 
03641     if(!transFound(comb)){
03642       setTransFound(comb);
03643 
03644       TRACE("quant trans","new: ", vectorExpr2string(instBindsTerm[j]), "");      
03645 
03646       Expr sr(instBindsTerm[j][0]);
03647       Expr dt(instBindsTerm[j][1]);
03648       
03649       const CDList<Expr>& dtForw = forwList(dt);
03650       const CDList<Expr>& srBack = backList(sr);
03651       
03652       for(size_t k=0; k<dtForw.size(); k++){
03653         vector<Expr> bind;
03654         bind.clear();
03655         bind.push_back(sr);
03656         bind.push_back(dt);
03657         bind.push_back(dtForw[k]);
03658 
03659         enqueueInst(univ, bind, gterm);
03660 
03661         TRACE("quant inst", "trans pred rule", univ.toString(), " | with bind: "+vectorExpr2string(bind));  
03662         TRACE("quant trans", "trans res forw: ", vectorExpr2string(bind), "");
03663       }
03664 
03665       for(size_t k=0; k<srBack.size(); k++){
03666         vector<Expr> bind;
03667         bind.clear();
03668         bind.push_back(srBack[k]);
03669         bind.push_back(sr);
03670         bind.push_back(dt);
03671 
03672         enqueueInst(univ, bind, gterm);
03673         TRACE("quant inst", "trans pred rule ", univ.toString(), " | with bind: "+vectorExpr2string(bind));
03674           TRACE("quant trans", "trans res back: ", vectorExpr2string(bind), "");
03675       }
03676 
03677       pushForwList(sr,dt);
03678       pushBackList(dt,sr);
03679     }
03680         } 
03681       }
03682     }
03683     return;
03684   }
03685       }
03686             
03687       bool univsHasMoreBVs ;
03688 
03689       univsHasMoreBVs = (d_hasMoreBVs.count(quantExpr) > 0);
03690 
03691       //      if ( !d_allout || !trig.isSimp() || univsHasMoreBVs || *d_useLazyInst){
03692       //      if ( !d_allout || !trig.isSimp() || univsHasMoreBVs || true){
03693       if  ( !d_allout || !trig.isSuperSimp() || univsHasMoreBVs ){
03694       //      if ( !d_allout || !trig.isSimp() || univsHasMoreBVs ){
03695       */
03696   /*
03697   if(hasGoodSynInstNewTrigOld(trig, bVarsTrig, instBindsTerm, instGterms, allterms, tBegin)) {
03698     genInstSetThm(bVarsThm, bVarsTrig, instBindsTerm, instBindsThm);
03699     for (size_t j = 0; j<instBindsTerm.size(); j++){
03700       const Expr& gterm = instGterms[j];
03701       const std::vector<Expr>& binds = instBindsThm[j];
03702       enqueueInst(univ, trig, binds, gterm); 
03703       TRACE("quant inst", "insert full inst", univ.toString(), " | with bind: "+vectorExpr2string(binds));  
03704     }
03705   }
03706   */
03707 /*
03708   bVarsTrig=trig.getBVs();//vVarsTrig is used later, do not forget this.
03709   if(hasGoodSynInstNewTrig(trig, bVarsThm, instBindsTerm, instGterms, allterms, tBegin)) {
03710       for (size_t j = 0; j<instBindsTerm.size(); j++){
03711         const Expr& gterm = instGterms[j];
03712         const std::vector<Expr>& binds = instBindsTerm[j];
03713       
03714         enqueueInst(univ, trig, binds, gterm); 
03715       
03716         TRACE("quant inst", "insert full inst", univ.toString(), " | with bind: "+vectorExpr2string(binds));  
03717       }
03718     }
03719   
03720       }      
03721       
03722       //      if(!d_allout || *d_useLazyInst){
03723       if(!d_allout){
03724   if(trig.hasRW() ){
03725     
03726     if(1 == bVarsTrig.size()){
03727       std::vector<Expr> tp = d_arrayIndic[trig.getHead()];
03728       for(size_t i=0; i<tp.size(); i++){
03729         std::vector<Expr> tp = d_arrayIndic[trig.getHead()];
03730 
03731         Expr index = tp[i];
03732         std::vector<Expr> temp;
03733         temp.clear();
03734         temp.push_back(index);
03735         
03736         enqueueInst(univ, temp, index);
03737         TRACE("quant inst", "read write rule", univ.toString(), " | with bind: "+vectorExpr2string(temp));  
03738       }
03739     }
03740     else{
03741     }
03742   }
03743       }
03744     }//end for each trigger      
03745   }
03746 }
03747 */
03748 void TheoryQuant::arrayHeuristic(const Trigger& trig, size_t univ_id){
03749 
03750   std::vector<Expr> tp = d_arrayIndic[trig.head];
03751   for(size_t i=0; i<tp.size(); i++){
03752     const Expr& index = tp[i];
03753     std::vector<Expr> temp;
03754     temp.push_back(index);
03755     enqueueInst(univ_id, temp, index);
03756     //    TRACE("quant inst", "read write rule", univ.toString(), " | with bind: "+vectorExpr2string(temp));  
03757   }
03758 }
03759 
03760 void TheoryQuant::synNewInst(size_t univ_id, const vector<Expr>& bind, const Expr& gterm, const Trigger& trig ){
03761   if(trig.isMulti){
03762     const multTrigsInfo& mtriginfo = d_all_multTrigsInfo[trig.multiId];
03763 
03764     vector<Expr> actual_bind;
03765     for(size_t i=0, iend=bind.size(); i<iend; i++){
03766       if(null_expr != bind[i]){
03767   actual_bind.push_back(bind[i]);
03768       }
03769     }
03770     Expr actual_bind_expr = Expr(RAW_LIST, actual_bind);
03771     
03772     size_t index = trig.multiIndex;
03773     CDMap<Expr,bool> * cur_cd_map = mtriginfo.var_binds_found[index];
03774     CDMap<Expr,bool>::iterator cur_iter = cur_cd_map->find(actual_bind_expr);
03775 
03776     if (cur_cd_map->end() != cur_iter){
03777       return; 
03778     }
03779  
03780     (*cur_cd_map)[actual_bind_expr] = true;
03781     
03782     const vector<size_t>& comm_pos = mtriginfo.common_pos[0];
03783     size_t comm_pos_size = comm_pos.size();
03784 
03785     Expr comm_expr;
03786     vector<Expr> comm_expr_vec;
03787     for(size_t i = 0; i < comm_pos_size; i++){
03788       comm_expr_vec.push_back(bind[comm_pos[i]]);
03789       //      cout<<"bind " <<bind[comm_pos[i]]<<endl;
03790     }
03791     if(0 == comm_pos_size){
03792       comm_expr = null_expr;
03793     }
03794     else{
03795       comm_expr = Expr(RAW_LIST, comm_expr_vec);
03796     }
03797     Expr uncomm_expr;
03798     vector<Expr> uncomm_expr_vec;
03799     
03800     const vector<size_t>& uncomm_pos = mtriginfo.var_pos[index];
03801     size_t uncomm_pos_size = uncomm_pos.size();
03802     for(size_t i = 0; i< uncomm_pos_size; i++){
03803       uncomm_expr_vec.push_back(bind[uncomm_pos[i]]);
03804     }
03805     uncomm_expr = Expr(RAW_LIST, uncomm_expr_vec);
03806     
03807     CDList<Expr>* add_into_list ;
03808     CDList<Expr>* iter_list;
03809     ExprMap<CDList<Expr>* >::iterator add_into_iter;
03810     ExprMap<CDList<Expr>* >::iterator iter_iter;
03811 
03812     size_t other_index = 0;
03813     if(0 == index){
03814       other_index =1;
03815     }
03816     else if (1 == index){
03817       other_index = 0;
03818     }
03819     else{
03820       FatalAssert(false, "wrong ");
03821     }
03822 
03823     //    cout<<"comm expr"<<comm_expr<<endl;
03824     add_into_iter = mtriginfo.uncomm_list[index]->find(comm_expr);
03825     iter_iter = mtriginfo.uncomm_list[other_index]->find(comm_expr);
03826     
03827     if(mtriginfo.uncomm_list[index]->end() == add_into_iter){
03828       add_into_list = new (true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext());
03829       (*mtriginfo.uncomm_list[index])[comm_expr] = add_into_list;
03830     }
03831     else{
03832       add_into_list = add_into_iter->second;
03833     }
03834     //    cout<<"uncomm expr"<<uncomm_expr<<endl;
03835     add_into_list->push_back(uncomm_expr);
03836 
03837     if(mtriginfo.uncomm_list[other_index]->end() == iter_iter){
03838       return;
03839     }
03840     else{
03841       iter_list = iter_iter->second;
03842     }
03843 
03844     const vector<size_t>& uncomm_iter_pos = mtriginfo.var_pos[other_index];
03845     size_t uncomm_iter_pos_size = uncomm_iter_pos.size();
03846       
03847     for(size_t i =0, iend = iter_list->size(); i<iend; i++){
03848       const Expr& cur_iter_expr = (*iter_list)[i];
03849       vector<Expr> new_bind(bind);
03850       for(size_t j=0; j<uncomm_iter_pos_size; j++){
03851   new_bind[uncomm_iter_pos[j]] = cur_iter_expr[j];
03852       }
03853       enqueueInst(univ_id, new_bind, gterm);    
03854     }
03855     return;
03856   }
03857   //  cout<<"synnewinst "<<univ_id<<endl;
03858   {//code for trans2
03859     if(trig.hasT2){
03860       vector<Expr> actual_bind;
03861       for(size_t i=0; i<bind.size(); i++){
03862   if(bind[i] != null_expr){
03863     actual_bind.push_back(bind[i]);
03864   }
03865       }
03866       if(actual_bind.size() != 2){
03867   cout<<"2 != bind.size()" <<endl;
03868       }
03869       
03870       Expr acb1 = simplifyExpr(actual_bind[0]);
03871       Expr acb2 = simplifyExpr(actual_bind[1]);
03872       actual_bind[0]=acb1;
03873       actual_bind[1]=acb2;
03874       if(acb1 != acb2){
03875   Expr comb = Expr(RAW_LIST,acb1, acb2);
03876   if(!trans2Found(comb)){
03877     setTrans2Found(comb);
03878     Expr comb_rev = Expr(RAW_LIST,acb2, acb1);
03879     if(trans2Found(comb_rev)){
03880       enqueueInst(univ_id, actual_bind, gterm);
03881     }
03882   }
03883       } 
03884     return;
03885     }
03886   }
03887   
03888   {//code for trans pred
03889     if(trig.hasTrans){
03890       vector<Expr> actual_bind;
03891       for(size_t i=0; i<bind.size(); i++){
03892   if(bind[i] != null_expr){
03893     actual_bind.push_back(simplifyExpr(bind[i]));
03894   }
03895       }
03896       if(simplifyExpr(actual_bind[0]) != simplifyExpr(actual_bind[1])){
03897   Expr comb = Expr(RAW_LIST,actual_bind[0], actual_bind[1]);
03898       
03899   if(!transFound(comb)){
03900     setTransFound(comb);
03901     
03902     Expr sr(actual_bind[0]);
03903     Expr dt(actual_bind[1]);
03904         
03905     const CDList<Expr>& dtForw = forwList(dt);
03906     const CDList<Expr>& srBack = backList(sr);
03907     
03908     for(size_t k=0; k<dtForw.size(); k++){
03909       vector<Expr> tri_bind;
03910       tri_bind.push_back(sr);
03911       tri_bind.push_back(dt);
03912       tri_bind.push_back(dtForw[k]);
03913       
03914       enqueueInst(univ_id, tri_bind, gterm);
03915     }
03916     
03917     for(size_t k=0; k<srBack.size(); k++){
03918       vector<Expr> tri_bind;
03919       tri_bind.push_back(srBack[k]);
03920       tri_bind.push_back(sr);
03921       tri_bind.push_back(dt);
03922       
03923       enqueueInst(univ_id, tri_bind, gterm);
03924       //      TRACE("quant inst", "trans pred rule ", univ.toString(), " | with bind: "+vectorExpr2string(bind));
03925       //      TRACE("quant trans", "trans res back: ", vectorExpr2string(bind), "");
03926     }
03927     
03928     pushForwList(sr,dt);
03929     pushBackList(dt,sr);
03930   }
03931       } 
03932       return;
03933     }
03934   }
03935   //  cout<<"before enqueueisnt"<<endl;
03936   enqueueInst(univ_id, bind, gterm); 
03937   //      if(!d_allout || *d_useLazyInst){
03938 
03939 }
03940 
03941 
03942 /*
03943 
03944 void TheoryQuant::synNewInst(size_t univ_id, const vector<Expr>& bind, const Expr& gterm, const Trigger& trig ){
03945   //  cout<<"synnewinst "<<univ_id<<endl;
03946   {//code for trans2
03947     if(trig.hasT2){
03948       vector<Expr> actual_bind;
03949       for(size_t i=0; i<bind.size(); i++){
03950   if(bind[i] != null_expr){
03951     actual_bind.push_back(bind[i]);
03952   }
03953       }
03954       if(actual_bind.size() != 2){
03955   cout<<"2 != bind.size()" <<endl;
03956       }
03957       if(simplifyExpr(actual_bind[0]) != simplifyExpr(actual_bind[1])){
03958   Expr comb = Expr(RAW_LIST,actual_bind[0], actual_bind[1]);
03959   if(!trans2Found(comb)){
03960     setTrans2Found(comb);
03961     Expr comb_rev = Expr(RAW_LIST,actual_bind[1], actual_bind[0]);
03962     if(trans2Found(comb_rev)){
03963       enqueueInst(univ_id, actual_bind, gterm);
03964     }
03965   }
03966       } 
03967     return;
03968     }
03969   }
03970   
03971   {//code for trans pred
03972     if(trig.hasTrans){
03973       vector<Expr> actual_bind;
03974       for(size_t i=0; i<bind.size(); i++){
03975   if(bind[i] != null_expr){
03976     actual_bind.push_back(bind[i]);
03977   }
03978       }
03979       if(simplifyExpr(actual_bind[0]) != simplifyExpr(actual_bind[1])){
03980   Expr comb = Expr(RAW_LIST,actual_bind[0], actual_bind[1]);
03981       
03982   if(!transFound(comb)){
03983     setTransFound(comb);
03984     
03985     Expr sr(actual_bind[0]);
03986     Expr dt(actual_bind[1]);
03987         
03988     const CDList<Expr>& dtForw = forwList(dt);
03989     const CDList<Expr>& srBack = backList(sr);
03990     
03991     for(size_t k=0; k<dtForw.size(); k++){
03992       vector<Expr> tri_bind;
03993       tri_bind.push_back(sr);
03994       tri_bind.push_back(dt);
03995       tri_bind.push_back(dtForw[k]);
03996       
03997       enqueueInst(univ_id, tri_bind, gterm);
03998     }
03999     
04000     for(size_t k=0; k<srBack.size(); k++){
04001       vector<Expr> tri_bind;
04002       tri_bind.push_back(srBack[k]);
04003       tri_bind.push_back(sr);
04004       tri_bind.push_back(dt);
04005       
04006       enqueueInst(univ_id, tri_bind, gterm);
04007       //      TRACE("quant inst", "trans pred rule ", univ.toString(), " | with bind: "+vectorExpr2string(bind));
04008       //      TRACE("quant trans", "trans res back: ", vectorExpr2string(bind), "");
04009     }
04010     
04011     pushForwList(sr,dt);
04012     pushBackList(dt,sr);
04013   }
04014       } 
04015       return;
04016     }
04017   }
04018   //  cout<<"before enqueueisnt"<<endl;
04019   enqueueInst(univ_id, bind, gterm); 
04020       
04021   //      if(!d_allout || *d_useLazyInst){
04022   if(!d_allout){
04023     if(trig.hasRWOp ){
04024       
04025       if(1 == trig.bvs.size()){
04026   std::vector<Expr> tp = d_arrayIndic[trig.head];
04027   for(size_t i=0; i<tp.size(); i++){
04028     std::vector<Expr> tp = d_arrayIndic[trig.head];
04029     
04030     Expr index = tp[i];
04031     std::vector<Expr> temp;
04032     temp.clear();
04033     temp.push_back(index);
04034     
04035     enqueueInst(univ_id, temp, index);
04036     //    TRACE("quant inst", "read write rule", univ.toString(), " | with bind: "+vectorExpr2string(temp));  
04037   }
04038       }
04039       else{
04040       }
04041     }
04042   }
04043 }
04044 */
04045 /*
04046 void TheoryQuant::synMultInst(const Theorem & univ, const CDList<Expr>& allterms, size_t tBegin ){
04047 
04048   const Expr& quantExpr = univ.getExpr();
04049   
04050   if(d_multTriggers[quantExpr].size() <= 0) return ;
04051 
04052   TRACE("quant inst", "try muli with:|", quantExpr.toString() , " ");
04053   const std::vector<Expr>& bVarsThm = quantExpr.getVars();
04054 
04055   std::vector<std::vector<Expr> > instSetThm; //set of instantiations for the thm
04056   std::vector<std::vector<Expr> > termInst; //terminst are bindings, in the order of bVarsTrig
04057   std::vector<Expr> bVarsTrig; 
04058 
04059 
04060   if(hasGoodSynMultiInst(quantExpr, bVarsTrig, termInst, allterms, tBegin)) {
04061     genInstSetThm(bVarsThm, bVarsTrig, termInst, instSetThm);
04062   }  
04063   {
04064     for(std::vector<std::vector<Expr> >::iterator i=instSetThm.begin(), iend=instSetThm.end(); i!=iend; ++i) {
04065       enqueueInst(univ, *i, null_expr);//fix the null_expr here asap
04066       TRACE("quant inst", "insert mult inst", univ.toString(), " | with bind: "+vectorExpr2string(*i));  
04067     }
04068   }
04069   
04070 }
04071 */
04072 /*
04073 void TheoryQuant::synPartInst(const Theorem & univ, const CDList<Expr>& allterms,  size_t tBegin ){
04074   
04075   const Expr& quantExpr = univ.getExpr();
04076   TRACE("quant inst", "try part with ", quantExpr.toString() , " ");
04077   
04078   const std::vector<Trigger>& triggers = d_partTrigs[quantExpr];
04079 
04080   std::vector<std::vector<Expr> > instSetThm; //set of instantiations for the thm
04081   std::vector<std::vector<Expr> > termInst; //terminst are bindings, in the order of bVarsTrig
04082   std::vector<Expr> bVarsTrig; 
04083   std::vector<Expr> instGterms;
04084 
04085   for( std::vector<Trigger>::const_iterator i= triggers.begin(), iend=triggers.end();i!=iend;++i)  {
04086   
04087     Trigger trig = *i;
04088     TRACE("quant inst","handle part trigger", trig.getEx().toString(),"");
04089     termInst.clear();
04090     bVarsTrig.clear();
04091     instSetThm.clear();
04092     //    if(hasGoodSynInstNewTrig(trig, bVarsTrig, termInst, instGterms,allterms, tBegin)) {
04093     if(hasGoodSynInstNewTrig(trig, trig.getBVs(), termInst, instGterms,allterms, tBegin)) {
04094       TRACE("quant syninst", "has good ", termInst.size(),"");
04095       TRACE("quant syninst", "after good ",instSetThm.size(), "");
04096 
04097       Theorem newUniv = d_rules->adjustVarUniv(univ, trig.getBVs());
04098       
04099       TRACE("quant syninst", " new univ:" ,newUniv.toString(),"");
04100       {
04101   for(size_t i = 0; i< termInst.size(); i++){
04102     const std::vector<Expr>& binds = termInst[i];
04103     const Expr& gterm = instGterms[i];
04104     enqueueInst(newUniv, binds, gterm);
04105     TRACE("quant yeting inst", "instantiating =========", "" , "");  
04106     TRACE("quant yeting inst", "instantiating", newUniv.getExpr().toString(), " | with bind: "+vectorExpr2string(binds));  
04107     TRACE("quant yeting inst", "instantiating org ", univ.getExpr().toString(), " | with gterm "+gterm.toString());  
04108   }
04109       }
04110     }
04111   }
04112 }
04113 
04114 */
04115 void TheoryQuant::semInst(const Theorem & univ, size_t tBegin){
04116 }
04117 
04118 void TheoryQuant::checkSat(bool fullEffort){
04119   if(*d_translate) return;
04120   if(d_rawUnivs.size() <=0 ) return;
04121 
04122   DebugAssert(d_univsQueue.size() == 0, "something left in d_univsQueue");
04123   DebugAssert(d_simplifiedThmQueue.size() == 0, "something left in d_univsQueue");
04124 
04125 #ifdef DEBUG  
04126   if(fullEffort){
04127     if( CVC3::debugger.trace("quant assertfact")  ){
04128       cout<<"===========all cached univs =========="<<endl;
04129       //      for (ExprMap<Theorem>::iterator i=d_simpUnivs.begin(), iend=d_simpUnivs.end(); i!=iend;  i++){
04130       //  cout<<"------------------------------------"<<endl;
04131       //  cout<<(i->first).toString()<<endl;
04132       //  cout<<"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"<<endl;
04133       //  cout<<(i->second).getExpr().toString()<<endl;
04134       //}
04135     }
04136     if( CVC3::debugger.trace("quant samehead")  ){
04137       cout<<"===========all cached  =========="<<endl;
04138       for (ExprMap< CDList<Expr>*>::iterator i=d_same_head_expr.begin(), iend=d_same_head_expr.end(); i!=iend;  i++){
04139   cout<<"------------------------------------"<<endl; 
04140   cout<<(i->first)<<endl;
04141   cout<<"_______________________"<<endl;
04142   CDList<Expr> * terms= i->second;
04143   for(size_t i =0; i<terms->size(); i++){
04144     cout<<(*terms)[i]<<endl;
04145   }
04146       }
04147     }
04148   }  
04149 #endif
04150 
04151 #ifdef DEBUG  
04152   if( CVC3::debugger.trace("quant checksat")  ){
04153     const CDList<Expr>& allpreds = theoryCore()->getPredicates();
04154     cout<<"=========== cur pred & terms =========="<<endl;
04155     
04156     for (size_t i=d_lastPredsPos; i<allpreds.size(); i++){
04157       cout<<"i="<<allpreds[i].getIndex()<<" :"<<findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
04158     }
04159     
04160     const CDList<Expr>&  allterms = theoryCore()->getTerms();
04161     
04162     for (size_t i=d_lastTermsPos; i<allterms.size(); i++){
04163       cout<<"i="<<allterms[i].getIndex()<<" :"<<findExpr(allterms[i])<<"|"<<allterms[i]<<endl;
04164     }
04165     cout<<"=========== cur quant =========="<<endl;
04166     for (size_t i=0; i<d_univs.size(); i++){
04167       cout<<"i="<<d_univs[i].getExpr().getIndex()<<" :"<<findExpr(d_univs[i].getExpr())<<"|"<<d_univs[i]<<endl;
04168     }
04169   }
04170   
04171 
04172   if( CVC3::debugger.trace("quant checksat equ") ){
04173     const CDList<Expr>& allpreds = theoryCore()->getPredicates();
04174     cout<<"=========== cur pred equ =========="<<endl;
04175     
04176     for (size_t i=d_lastPredsPos; i<allpreds.size(); i++){
04177       if(allpreds[i].isEq()){
04178   cout<<"i="<<allpreds[i].getIndex()<<" :"<<findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
04179       }
04180     }
04181     cout<<"=========== cur pred equ end  =========="<<endl;
04182   }
04183   
04184 #endif
04185   
04186   if((*d_useLazyInst && !fullEffort) ) return;
04187 
04188   {//for the same head list
04189    const CDList<Expr>&  allterms = theoryCore()->getTerms();
04190    for(size_t i=d_lastTermsPos; i<allterms.size(); i++){
04191      Expr t = allterms[i];
04192      if(canGetHead(t)){
04193        if(d_same_head_expr.count(getHead(t)) >0){
04194    d_same_head_expr[getHead(t)]->push_back(t);
04195        }
04196        else{
04197    d_same_head_expr[getHead(t)]= 
04198      new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
04199    d_same_head_expr[getHead(t)]->push_back(t);
04200        }
04201      }
04202    }
04203 
04204    const CDList<Expr>&  allpreds = theoryCore()->getPredicates();
04205    for(size_t i=d_lastPredsPos; i<allpreds.size(); i++){
04206      Expr t = allpreds[i];
04207      if(canGetHead(t)){
04208        if(d_same_head_expr.count(getHead(t)) >0){
04209    d_same_head_expr[getHead(t)]->push_back(t);
04210        }
04211        else{
04212    d_same_head_expr[getHead(t)]= 
04213      new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
04214    d_same_head_expr[getHead(t)]->push_back(t);
04215        }
04216      }
04217    }
04218   }
04219     
04220   {//for the equalities list
04221     const CDList<Expr>&  allpreds = theoryCore()->getPredicates();
04222     for(size_t i=d_lastPredsPos; i<allpreds.size(); i++){
04223       const Expr& t = allpreds[i];
04224       if(t.isEq()){
04225   //  cout<<"EQ: "<<t<<endl;
04226   const Expr lterm = t[0];
04227   const Expr rterm = t[1];
04228   d_eqs.push_back(lterm);
04229   d_eqs.push_back(rterm);
04230     
04231   /*   
04232   ExprMap<CDList<Expr>* >::iterator iter = d_eq_list.find(lterm);
04233   if(d_eq_list.end() == iter){
04234     d_eq_list[lterm] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
04235     d_eq_list[lterm]->push_back(rterm);
04236   }
04237   else{
04238     iter->second->push_back(rterm);
04239   }
04240 
04241   //  cout<<"LTERM: " <<rterm<<endl;
04242   iter = d_eq_list.find(rterm);
04243   if(d_eq_list.end() == iter){
04244     d_eq_list[rterm] = new(true) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
04245     d_eq_list[rterm]->push_back(lterm);
04246   }
04247   else{
04248     iter->second->push_back(lterm);
04249   }
04250   //  cout<<"RTERM: " <<lterm<<endl;
04251   */
04252       }
04253     }
04254   }
04255   
04256 
04257   {//for rw heuristic
04258    const CDList<Expr>&  allterms = theoryCore()->getTerms();
04259    for(size_t i=d_lastTermsPos; i<allterms.size(); i++){
04260      const Expr& cur=allterms[i];
04261      if(READ == cur.getKind() || WRITE == cur.getKind()){
04262        arrayIndexName(cur);
04263      }
04264    }
04265   }
04266  
04267   d_instThisRound = 0;
04268   d_useMultTrig=*d_useMult;
04269   d_usePartTrig=*d_usePart;
04270   d_useFullTrig=true;
04271 
04272   if(fullEffort) {
04273     d_inEnd=true;
04274   }
04275   else{
04276     d_inEnd=false;
04277   }
04278 
04279 
04280   ExprMap<ExprMap<vector<dynTrig>* >* > new_trigs;
04281   for(size_t i=d_univs.size(); i<d_rawUnivs.size(); i++){
04282     setupTriggers(new_trigs, d_rawUnivs[i], i);
04283   }
04284 
04285   try {
04286     if (!(*d_useNew)){
04287       naiveCheckSat(fullEffort);
04288     }
04289     else if (*d_useSemMatch){
04290       semCheckSat(fullEffort);
04291     }
04292     else {
04293       synCheckSat(new_trigs, fullEffort);
04294     }
04295   }
04296   
04297   catch (int x){
04298 
04299      while(!d_simplifiedThmQueue.empty()){
04300        d_simplifiedThmQueue.pop();
04301      }
04302     d_tempBinds.clear();
04303     saveContext();
04304     delNewTrigs(new_trigs);
04305     return;
04306   }
04307   
04308   sendInstNew();   
04309 
04310   saveContext();
04311 
04312   try{
04313     if((*d_useNew) && (0 == d_instThisRound) && fullEffort && theoryCore()->getTerms().size()< (size_t)(*d_maxNaiveCall) ) {
04314       //    cout<<"naive called"<<endl;
04315       if (0== theoryCore()->getTerms().size()){
04316   static int counter =0;
04317 
04318   std::set<Expr> types;
04319   for(size_t i = 0; i<d_univs.size(); i++){
04320     const Expr& cur_quant = d_univs[i].getExpr();
04321     const std::vector<Expr> cur_vars = cur_quant.getVars();
04322     for(size_t j =0; j<cur_vars.size(); j++){
04323       types.insert(cur_vars[j].getType().getExpr());
04324     }
04325   }
04326       
04327   std::string base("_naiveInst");
04328   for(std::set<Expr>::iterator i=types.begin(), iend = types.end(); i != iend; i++){
04329     counter++;
04330     std::stringstream tempout;
04331     tempout << counter;
04332     std::string out_str = base + tempout.str();
04333     Expr newExpr = theoryCore()->getEM()->newVarExpr(out_str);
04334 
04335     newExpr.setType(Type(*i));
04336     
04337     Proof pf;
04338     
04339     Expr newExpr2 = theoryCore()->getEM()->newVarExpr(out_str+"extra");
04340     newExpr2.setType(Type(*i));
04341     
04342     Expr newConstThm;
04343 
04344     if(Type(*i) == theoryCore()->getEM()->newRatExpr(0).getType()){
04345       //somehow theory_arith will complain if we use expr2 to form the eq here
04346       newConstThm = newExpr.eqExpr(theoryCore()->getEM()->newRatExpr(0));
04347     }
04348     else{
04349       newConstThm = newExpr.eqExpr(newExpr2);
04350     }
04351     Theorem newThm  = d_rules->addNewConst(newConstThm);
04352     
04353     enqueueFact(newThm);
04354     d_tempBinds.clear();
04355     return;
04356   }
04357   
04358       }
04359     naiveCheckSat(fullEffort);
04360     }
04361   }//end of try
04362   
04363   catch (int x){
04364     //    d_simplifiedThmQueue.clear();
04365      while(!d_simplifiedThmQueue.empty()){
04366        d_simplifiedThmQueue.pop();
04367      }
04368     d_tempBinds.clear();
04369     saveContext();
04370     delNewTrigs(new_trigs);
04371     return;
04372   }
04373   
04374   if(fullEffort) {
04375     sendInstNew();
04376   }
04377 
04378   combineOldNewTrigs(new_trigs);
04379   delNewTrigs(new_trigs);
04380 }
04381 
04382 void TheoryQuant::saveContext(){
04383   d_lastArrayPos.set(d_arrayTrigs.size());
04384   d_univsSavedPos.set(d_univs.size());
04385   d_rawUnivsSavedPos.set(d_rawUnivs.size());
04386   d_lastTermsPos.set(theoryCore()->getTerms().size());
04387   d_lastPredsPos.set(theoryCore()->getPredicates().size());
04388   d_lastUsefulGtermsPos.set(d_usefulGterms.size());
04389 }
04390 
04391 /*void TheoryQuant::synCheckSat(bool fullEffort){
04392 }
04393 */
04394 void TheoryQuant::synCheckSat(ExprMap<ExprMap<vector<dynTrig>* >* >&  new_trigs, bool fullEffort){
04395   
04396   d_allout=false;
04397 
04398   if(fullEffort)   {
04399     setIncomplete("Quantifier instantiation");
04400   }
04401 
04402   size_t uSize = d_univs.size() ;
04403   const CDList<Expr>& allterms = theoryCore()->getTerms();
04404   const CDList<Expr>& allpreds = theoryCore()->getPredicates();
04405   size_t tSize = allterms.size();
04406   size_t pSize = allpreds.size();
04407 
04408   TRACE("quant",uSize, " uSize and univsSavedPOS ", d_univsSavedPos);
04409   TRACE("quant",tSize, " tSize and termsLastPos ", d_lastTermsPos);
04410   TRACE("quant",pSize, " pSize and predsLastPos ", d_lastPredsPos);
04411   TRACE("quant", fullEffort, " fulleffort:scope ",theoryCore()->getCM()->scopeLevel() );
04412     
04413   for(size_t i=d_lastTermsPos; i<tSize; i++){
04414     const Expr& cur(allterms[i]);
04415     if(usefulInMatch(cur)){
04416       if(*d_useExprScore){
04417   int score = getExprScore(cur);
04418   if(score <= d_curMaxExprScore && 0 <= score ){
04419     d_usefulGterms.push_back(cur);
04420     add_parent(cur);
04421   } 
04422       }
04423       else{
04424   d_usefulGterms.push_back(cur);
04425   add_parent(cur);
04426       }
04427     }
04428     else{
04429     }
04430   }
04431 
04432   for(size_t i=d_lastPredsPos; i<pSize; i++){
04433     const Expr& cur=allpreds[i];
04434     if( usefulInMatch(cur)){
04435       if(*d_useExprScore ){
04436   int score = getExprScore(cur);
04437   if(score <= d_curMaxExprScore && 0 <= score){
04438     d_usefulGterms.push_back(cur);
04439     add_parent(cur);
04440   } 
04441       }
04442       else{
04443   d_usefulGterms.push_back(cur);
04444   add_parent(cur);
04445       }
04446     }
04447     else{
04448     }
04449   }
04450   
04451 
04452   if(d_useFullTrig && d_inEnd && *d_useInstEnd ){
04453 
04454     if(*d_useExprScore){
04455 
04456       matchListOld(d_usefulGterms, d_lastUsefulGtermsPos, d_usefulGterms.size() ); //new terms to old list
04457       matchListNew(new_trigs, d_usefulGterms, 0, d_usefulGterms.size()); //new and old terms to new list
04458       
04459       if(sendInstNew() > 0){
04460   TRACE("inend", "debug 1", "" ,"" );
04461   return;
04462       } 
04463       
04464       d_allout = true;
04465       {
04466   CDList<Expr>* changed_terms = new (false) CDList<Expr> (theoryCore()->getCM()->getCurrentContext()) ;
04467   collectChangedTerms(*changed_terms);
04468   
04469   matchListOld(*changed_terms, 0, changed_terms->size());
04470   matchListNew(new_trigs, *changed_terms, 0 , changed_terms->size());
04471   delete changed_terms;
04472       }
04473 
04474       int n;
04475       if( ( n = sendInstNew()) > 0){
04476   TRACE("inend",  "debug 2", " # ",n );
04477   return;
04478       }
04479       d_allout = false;      
04480 
04481 
04482       int numNewTerm=0;
04483       int oldNum=d_usefulGterms.size();
04484 
04485       for(size_t i=0; i<tSize; i++){
04486   const Expr& cur(allterms[i]);
04487   if(!(usefulInMatch(cur))) continue;
04488   int score = getExprScore(cur);
04489   if( score > d_curMaxExprScore){
04490     if((d_curMaxExprScore + 1) == score){
04491       d_usefulGterms.push_back(cur);
04492       add_parent(cur);
04493       numNewTerm++;
04494     }
04495     else{
04496       TRACE("inend", "is this good? ", cur.toString()+" #-# " , score);
04497       d_usefulGterms.push_back(cur);
04498       add_parent(cur);
04499       numNewTerm++;
04500     }
04501   }
04502       }
04503 
04504       for(size_t i=0; i<pSize; i++){
04505   const Expr& cur(allpreds[i]);
04506   if(!(usefulInMatch(cur))) continue;
04507   int score = getExprScore(cur);
04508   if( score > d_curMaxExprScore){
04509     if((d_curMaxExprScore + 1) == score){
04510       d_usefulGterms.push_back(cur);
04511       add_parent(cur);
04512       numNewTerm++;
04513     }
04514     else{
04515       TRACE("inend", "is this good? ", cur.toString()+" #-# " , score);
04516       d_usefulGterms.push_back(cur);
04517       add_parent(cur);
04518       numNewTerm++;
04519     }
04520   }
04521       }
04522 
04523       if(numNewTerm >0 ){
04524 
04525   if(d_curMaxExprScore >=0 ){
04526 
04527     d_curMaxExprScore =  d_curMaxExprScore+1;;
04528   }
04529   else {
04530     d_curMaxExprScore =  d_curMaxExprScore+1;
04531   }
04532   
04533   matchListOld(d_usefulGterms, oldNum, d_usefulGterms.size() );
04534   matchListNew(new_trigs, d_usefulGterms, oldNum, d_usefulGterms.size());
04535   
04536   if(sendInstNew() > 0){
04537     TRACE("inend",  "debug 3", "" , "" );
04538     return;
04539   }
04540       }
04541       for(size_t array_index = 0; array_index < d_arrayTrigs.size(); array_index++){
04542   arrayHeuristic(d_arrayTrigs[array_index].trig, d_arrayTrigs[array_index].univ_id); 
04543       }
04544       
04545       return ;
04546     }
04547     
04548     TRACE("inend", "debug 3 0", "", "");
04549     TRACE("quant","this round; ",d_callThisRound,"");
04550 
04551     return;
04552   }
04553         
04554 
04555   if ((uSize == d_univsSavedPos) && 
04556       (tSize == d_lastTermsPos) && 
04557       (pSize == d_lastPredsPos) ) return;
04558   
04559 
04560   matchListOld(d_usefulGterms, d_lastUsefulGtermsPos,d_usefulGterms.size() ); //new terms to old list
04561   
04562   matchListNew(new_trigs, d_usefulGterms, 0, d_usefulGterms.size() ); //new and old terms to new list
04563 
04564   for(size_t array_index = d_lastArrayPos; array_index < d_arrayTrigs.size(); array_index++){
04565     arrayHeuristic(d_arrayTrigs[array_index].trig, d_arrayTrigs[array_index].univ_id); 
04566   }
04567 
04568   TRACE("quant","this round; ",d_callThisRound,"");
04569   
04570   return;
04571 }
04572 
04573 
04574 void TheoryQuant::semCheckSat(bool fullEffort){
04575 }
04576 
04577 //the following is old code and I did not modify much, Yeting
04578 void TheoryQuant::naiveCheckSat(bool fullEffort){
04579   TRACE("quant", "checkSat ", fullEffort, "{");
04580   IF_DEBUG(int instCount = d_instCount);
04581   size_t uSize = d_univs.size(), stSize = d_savedTerms.size();
04582   if(true || (fullEffort && uSize > 0)) {
04583     // First of all, this algorithm is incomplete
04584     setIncomplete("Quantifier instantiation");
04585     
04586     if(d_instCount>=*d_maxQuantInst)
04587       return;
04588     //first attempt to instantiate with the saved terms
04589     //only do this if there are new saved terms or new theroems and 
04590     // at least some saved terms
04591     bool savedOnly = ((uSize > d_univsSavedPos.get()  && stSize > 0) ||
04592           (stSize > d_savedTermsPos.get()));
04593     int origCount = d_instCount;
04594     if(savedOnly)
04595       {
04596   TRACE("quant", "checkSat [saved insts]: univs size = ", uSize , " ");
04597   for(size_t i=0, pos = d_univsSavedPos.get(); i<uSize; i++) {
04598     if(d_instCount>= *d_maxQuantInst)
04599       break;
04600     else
04601       instantiate(d_univs[i], i>=pos, true,  d_savedTermsPos.get());
04602   }
04603   d_univsSavedPos.set(d_univs.size());
04604   d_savedTermsPos.set(stSize);
04605       }
04606     if(!savedOnly || d_instCount == origCount)
04607       { //instantiate with context dependent assertions terms
04608   TRACE("quant", "checkSat [context insts]: univs size = ", uSize , " ");
04609   const CDList<Expr>& assertions = theoryCore()->getTerms();
04610   int origSize = d_contextTerms.size();
04611 //  for(size_t i=0; i<uSize; i++)
04612 //    assertions.push_back(d_univs[i].getExpr());
04613   //build the map of all terms grouped into vectors by types
04614   TRACE("quant", "checkSat terms size = ", assertions.size() , " ");
04615   mapTermsByType(assertions);
04616   for(size_t i=0, pos = d_univsContextPos.get(); i<uSize; i++) {
04617     if(d_instCount>= *d_maxQuantInst)
04618       break;
04619     else
04620       instantiate(d_univs[i], i>=pos, false, origSize);
04621   }
04622   d_univsContextPos.set(d_univs.size());
04623       }
04624     TRACE("quant terse", "checkSat total insts: ",
04625     d_instCount, ", new "+int2string(d_instCount - instCount));
04626   }
04627   TRACE("quant", "checkSat total insts: ", d_instCount, " ");
04628   TRACE("quant", "checkSat new insts: ", d_instCount - instCount, " ");
04629   TRACE("quant", "checkSat effort:",  fullEffort, " }");
04630 
04631 }
04632 
04633 
04634 /*! \brief Queues up all possible instantiations of bound
04635  * variables.
04636  *
04637  * The savedMap boolean indicates whether to use savedMap or
04638  * d_contextMap the all boolean indicates weather to use all
04639  * instantiation or only new ones and newIndex is the index where
04640  * new instantiations begin.
04641  */
04642 void TheoryQuant::instantiate(Theorem univ, bool all, bool savedMap, 
04643             size_t newIndex)
04644 {
04645   
04646   if(!all && ((savedMap &&  newIndex == d_savedTerms.size())
04647         ||(!savedMap && newIndex == d_contextTerms.size())))
04648     return;
04649 
04650   TRACE("quant", "instanitate", all , "{");
04651   std::vector<Expr> varReplacements;
04652   recInstantiate(univ, all, savedMap, newIndex, varReplacements);
04653   TRACE("quant", "instanitate", "", "}");
04654   
04655 }
04656 
04657  //! does most of the work of the instantiate function.
04658 void TheoryQuant::recInstantiate(Theorem& univ, bool all, bool savedMap,
04659          size_t newIndex, 
04660          std::vector<Expr>& varReplacements)
04661 {
04662   Expr quantExpr = univ.getExpr();
04663   const vector<Expr>& boundVars = quantExpr.getVars();
04664   
04665   size_t curPos = varReplacements.size(); 
04666   TRACE("quant", "recInstantiate: ", boundVars.size() - curPos, "");
04667   //base case: a full vector of instantiations exists
04668   if(curPos == boundVars.size()) {
04669     if(!all)
04670       return;
04671     Theorem t = d_rules->universalInst(univ, varReplacements);
04672     d_insts[t.getExpr()] = varReplacements;
04673     TRACE("quant", "recInstantiate => " , t.toString(), "");
04674     if(d_instCount< *d_maxQuantInst) {
04675       d_instCount=d_instCount+1;
04676       enqueueInst(univ, varReplacements, null_expr);
04677       //            enqueueInst(univ, t);
04678       // enqueueFact(t);
04679     }
04680     return;
04681   }
04682   //recursively add all possible instantiations in the next 
04683   //available space of the vector
04684   else {
04685     Type t = getBaseType(boundVars[curPos]);
04686     int iendC=0, iendS=0, iend;
04687     std::vector<size_t>* typeVec = NULL; // = d_savedMap[t];
04688     CDList<size_t>* typeList = NULL; // = *d_contextMap[t];
04689     if(d_savedMap.count(t) > 0) {
04690       typeVec = &(d_savedMap[t]);
04691       iendS = typeVec->size();
04692       TRACE("quant", "adding from savedMap: ", iendS, "");
04693     }
04694     if(!savedMap) {
04695       if(d_contextMap.count(t) > 0) {
04696   typeList = d_contextMap[t];
04697   iendC = typeList->size();
04698   TRACE("quant", "adding from contextMap:", iendC , "");
04699       }
04700     }
04701     iend = iendC + iendS;
04702     for(int i =0; i<iend; i++) {
04703       TRACE("quant", "I must have gotten here!", "", "");
04704       size_t index;
04705       if(i<iendS){
04706   index = (*typeVec)[i];
04707   varReplacements.push_back(d_savedTerms[index]);
04708       }
04709       else {
04710   index = (*typeList)[i-iendS];
04711   varReplacements.push_back(d_contextTerms[index]);
04712       }
04713       if((index <  newIndex) || (!savedMap && i<iendS))
04714   recInstantiate(univ, all, savedMap, newIndex,  varReplacements);
04715       else
04716   recInstantiate(univ, true, savedMap, newIndex,  varReplacements);
04717       varReplacements.pop_back();   
04718     }
04719 
04720 
04721   }
04722 }
04723 
04724 /*! \brief categorizes all the terms contained in a vector of  expressions by
04725  * type.
04726  *
04727  * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
04728  */
04729 void TheoryQuant::mapTermsByType(const CDList<Expr>& terms)
04730 {
04731   Expr trExpr=trueExpr(), flsExpr = falseExpr();
04732   Type boolT = boolType();
04733   if(d_contextMap.count(boolT) == 0)
04734     {
04735       d_contextMap[boolT] =
04736         new(true) CDList<size_t>(theoryCore()->getCM()->getCurrentContext());
04737       size_t pos = d_contextTerms.size();
04738       d_contextTerms.push_back(trExpr);
04739       d_contextTerms.push_back(flsExpr);
04740       (*d_contextMap[boolT]).push_back(pos);
04741       (*d_contextMap[boolT]).push_back(pos+1);
04742     }
04743   for(size_t i=0; i<terms.size(); i++)
04744     recursiveMap(terms[i]);
04745   // Add all our saved universals to the pool
04746   for(size_t i=0; i<d_univs.size(); i++)
04747     recursiveMap(d_univs[i].getExpr());
04748 }
04749 
04750 /*! \brief categorizes all the terms contained in an expressions by
04751  * type. 
04752  *
04753  * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
04754  * returns true if the expression does not contain bound variables, false
04755  * otherwise.
04756  */
04757 bool TheoryQuant::recursiveMap(const Expr& e)
04758 {
04759   if(d_contextCache.count(e)>0) {
04760     return(d_contextCache[e]);
04761   }
04762   if(e.arity()>0)  {
04763     for(Expr::iterator it = e.begin(), iend = e.end(); it!=iend; ++it)
04764       //maps the children and returns a bool
04765       if(recursiveMap(*it) == false) {
04766   d_contextCache[e] = false;
04767       }
04768   }
04769   else if(e.getKind() == EXISTS || e.getKind() == FORALL){
04770     //maps the body
04771     if(recursiveMap(e.getBody())==false) {
04772       d_contextCache[e]=false;
04773     }
04774   }
04775   //found a bound variable in the children
04776   if(d_contextCache.count(e)>0) {
04777     return false;
04778   }
04779   
04780   if(d_savedCache.count(e) > 0) {
04781     return true;
04782   }
04783   
04784   Type type = getBaseType(e);
04785   
04786   if(!type.isBool() && !(e.getKind()==BOUND_VAR)){
04787      TRACE("quant", "recursiveMap: found ", 
04788      e.toString() + " of type " + type.toString(), "");
04789     int pos = d_contextTerms.size();
04790     d_contextTerms.push_back(e);
04791     if(d_contextMap.count(type)==0)
04792       d_contextMap[type] =
04793         new(true) CDList<size_t>(theoryCore()->getCM()->getCurrentContext());
04794     (*d_contextMap[type]).push_back(pos);
04795   }
04796 
04797   if(e.getKind() == BOUND_VAR) {
04798     d_contextCache[e] = false;
04799     return false;
04800   }
04801   else {
04802     d_contextCache[e] = true;
04803     return true;
04804   }
04805   //need  to implement: 
04806   //insert all instantiations if type is finite and reasonable
04807   //also need to implement instantiations of subtypes
04808 }
04809 
04810 /*!\brief Used to notify the quantifier algorithm of possible 
04811  * instantiations that were used in proving a context inconsistent.
04812  */
04813 void TheoryQuant::notifyInconsistent(const Theorem& thm){
04814 #ifdef DEBUG
04815 
04816   if( CVC3::debugger.trace("quant inscon")  ){
04817 
04818     cout<<"the one caused incsonsistency"<<endl;
04819     cout<<thm.getAssumptionsRef().toString()<<endl;
04820     std::vector<Expr> assump;
04821     thm.getLeafAssumptions(assump);
04822 
04823     cout<<"===========leaf assumptions; =========="<<endl;
04824     for(std::vector<Expr>::iterator i=assump.begin(), iend=assump.end(); i!=iend; i++){
04825       cout<<">>"<<i->toString()<<endl;
04826     }
04827   }
04828 #endif
04829 
04830   if(d_univs.size() == 0)
04831     return;
04832   DebugAssert(thm.getExpr().isFalse(), "notifyInconsistent called with"
04833   " theorem: " + thm.toString() + " which is not a derivation of false");
04834   TRACE("quant", "notifyInconsistent: { " , thm.toString(), "}");
04835   //  thm.clearAllFlags();
04836   //  findInstAssumptions(thm);
04837   TRACE("quant terse", "notifyInconsistent: savedTerms size = ",
04838   d_savedTerms.size(), "");
04839   TRACE("quant terse", "last term: ", 
04840   d_savedTerms.size()? d_savedTerms.back() : Expr(), "");
04841 }
04842 /*! \brief A recursive function used to find instantiated universals
04843  * in the hierarchy of assumptions.
04844  */
04845 void TheoryQuant::findInstAssumptions(const Theorem& thm)
04846 {
04847   if(thm.isNull() || thm.isRefl() || thm.isFlagged())
04848     return;
04849   thm.setFlag();
04850   const Expr& e = thm.getExpr();
04851   if(d_insts.count(e) > 0) {
04852     vector<Expr>& insts = d_insts[e];
04853     int pos;
04854     for(vector<Expr>::iterator it = insts.begin(), iend = insts.end(); it!=iend
04855     ; ++it)
04856       {
04857   if(d_savedCache.count(*it) ==  0) {
04858     TRACE("quant", "notifyInconsistent: found:", (*it).toString(), "");
04859     d_savedCache[*it] = true;
04860     pos = d_savedTerms.size();
04861     d_savedTerms.push_back(*it);
04862     d_savedMap[getBaseType(*it)].push_back(pos);
04863   }
04864       }
04865   }
04866   if(thm.isAssump())
04867     return;
04868   const Assumptions& a = thm.getAssumptionsRef();
04869   for(Assumptions::iterator it =a.begin(), iend = a.end(); it!=iend; ++it){
04870     findInstAssumptions(*it);
04871   }
04872 }
04873 
04874 //! computes the type of a quantified term. Always a  boolean.
04875 void TheoryQuant::computeType(const Expr& e)
04876 {
04877   switch (e.getKind()) {
04878   case FORALL:
04879   case EXISTS: {
04880     if(!e.getBody().getType().isBool())
04881       throw TypecheckException("Type mismatch for expression:\n\n   "
04882             + e.getBody().toString()
04883             + "\n\nhas the following type:\n\n  "
04884             + e.getBody().getType().toString()
04885             + "\n\nbut the expected type is Boolean:\n\n  ");
04886     else
04887       
04888       e.setType(e.getBody().getType());
04889     break;
04890   }
04891   default:
04892     DebugAssert(false,"Unexpected kind in Quantifier Theory: " 
04893     + e.toString());
04894     break;
04895   }
04896 }
04897 
04898 /*!
04899  * TCC(forall x.phi(x)) = (forall x. TCC(phi(x)))
04900  *                         OR (exists x. TCC(phi(x)) & !phi(x))
04901  * TCC(exists x.phi(x)) = (forall x. TCC(phi(x)))
04902  *                         OR (exists x. TCC(phi(x)) & phi(x))
04903  */
04904 
04905 
04906 Expr TheoryQuant::computeTCC(const Expr& e) {
04907   DebugAssert(e.isQuantifier(), "Unexpected expression in Quantifier Theory: " 
04908         + e.toString());
04909 
04910   bool forall(e.getKind() == FORALL);
04911   const Expr& phi = e.getBody();
04912   Expr tcc_phi = getTCC(phi);
04913   Expr forall_tcc = getEM()->newClosureExpr(FORALL, e.getVars(), tcc_phi);
04914   Expr exists_tcc = getEM()->newClosureExpr(EXISTS, e.getVars(),
04915                                             tcc_phi && (forall? !phi : phi));
04916   return (forall_tcc || exists_tcc);  
04917 }
04918 
04919 
04920 ExprStream&
04921 TheoryQuant::print(ExprStream& os, const Expr& e) {
04922   switch(os.lang()) {
04923   case SIMPLIFY_LANG:
04924     {
04925       switch(e.getKind()){
04926       case FORALL:
04927       case EXISTS: {
04928   if(!e.isQuantifier()) {
04929     e.print(os);
04930     break;
04931   }
04932   os << "(" << ((e.getKind() == FORALL)? "FORALL" : "EXISTS");
04933   const vector<Expr>& vars = e.getVars();
04934   bool first(true);
04935   os << "(" ;
04936   for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
04937       i!=iend; ++i) {
04938     if(first) first = false;
04939     else os << " " ;
04940     os << *i;
04941     // The quantifier may be in a raw parsed form, in which case
04942     // the type is not assigned yet
04943     //if(i->isVar())  // simplify do not need type
04944     //  os << ":" << space << pushdag << (*i).getType() << popdag;
04945   }
04946   os << ") "  << e.getBody() <<  ")";
04947       }
04948   break;
04949       default:
04950   e.print(os);
04951   break;
04952       }
04953       break;
04954     }
04955 
04956   case PRESENTATION_LANG: {
04957     switch(e.getKind()){
04958     case FORALL:
04959     case EXISTS: {
04960       if(!e.isQuantifier()) {
04961   e.print(os);
04962   break;
04963       }
04964       os << "(" << push << ((e.getKind() == FORALL)? "FORALL" : "EXISTS")
04965    << space << push;
04966       const vector<Expr>& vars = e.getVars();
04967       bool first(true);
04968       os << "(" << push;
04969       for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
04970     i!=iend; ++i) {
04971   if(first) first = false;
04972   else os << push << "," << pop << space;
04973   os << *i;
04974   // The quantifier may be in a raw parsed form, in which case
04975   // the type is not assigned yet
04976   // the following lines are changed for a neat output / by yeting
04977   if(*d_translate || true){
04978     if(i->isVar())
04979       os << ":" << space << pushdag << (*i).getType() << popdag;
04980   }
04981       }
04982       os << push << "): " << pushdag << push
04983    << e.getBody() << push << ")";
04984     }
04985       break;
04986     default:
04987       e.print(os);
04988       break;
04989     }
04990     break;
04991   }
04992   case SMTLIB_LANG: {
04993     d_theoryUsed = true;
04994     switch(e.getKind()){
04995       case FORALL:
04996       case EXISTS: {
04997         if(!e.isQuantifier()) {
04998           e.print(os);
04999           break;
05000         }
05001         os << "(" << push << ((e.getKind() == FORALL)? "forall" : "exists")
05002            << space;
05003         const vector<Expr>& vars = e.getVars();
05004         bool first(true);
05005         //      os << "(" << push;
05006         for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
05007             i!=iend; ++i) {
05008           if(first) first = false;
05009           else os << space;
05010           os << "(" << push << *i;
05011           // The quantifier may be in a raw parsed form, in which case
05012           // the type is not assigned yet
05013           if(i->isVar())
05014             os << space << pushdag << (*i).getType() << popdag;
05015           os << push << ")" << pop << pop;
05016         }
05017         os << space << pushdag
05018            << e.getBody() << push << ")";
05019         break;
05020       }
05021       default:
05022         throw SmtlibException("TheoryQuant::print: SMTLIB_LANG: Unexpected expression: "
05023                               +getEM()->getKindName(e.getKind()));
05024         break;
05025     }
05026     break;
05027   } // End of SMTLIB_LANG
05028   case LISP_LANG: {
05029     switch(e.getKind()){
05030     case FORALL:
05031     case EXISTS: {
05032       if(!e.isQuantifier()) {
05033   e.print(os);
05034   break;
05035       }
05036       os << "(" << push << ((e.getKind() == FORALL)? "FORALL" : "EXISTS")
05037    << space;
05038       const vector<Expr>& vars = e.getVars();
05039       bool first(true);
05040       os << "(" << push;
05041       for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
05042     i!=iend; ++i) {
05043   if(first) first = false;
05044   else os << space;
05045   os << "(" << push << *i;
05046   // The quantifier may be in a raw parsed form, in which case
05047   // the type is not assigned yet
05048   if(i->isVar())
05049     os << space << pushdag << (*i).getType() << popdag;
05050   os << push << ")" << pop << pop;
05051       }
05052       os << push << ")" << pop << pop << pushdag
05053    << e.getBody() << push << ")";
05054     }
05055       break;
05056     default:
05057       e.print(os);
05058       break;
05059     }
05060     break;
05061   }
05062   default:
05063     e.print(os);
05064     break;
05065   }
05066   return os;
05067 }
05068 
05069 ///////////////////////////////////////////////////////////////////////////////
05070 //parseExprOp:
05071 //translating special Exprs to regular EXPR??
05072 ///////////////////////////////////////////////////////////////////////////////
05073 Expr
05074 TheoryQuant::parseExprOp(const Expr& e) {
05075   TRACE("parser", "TheoryQuant::parseExprOp(", e, ")");
05076   // If the expression is not a list, it must have been already
05077   // parsed, so just return it as is.
05078   if(RAW_LIST != e.getKind()) return e;
05079 
05080   DebugAssert(e.arity() > 0,
05081         "TheoryQuant::parseExprOp:\n e = "+e.toString());
05082   
05083   const Expr& c1 = e[0][0];
05084   const string& opName(c1.getString());
05085   int kind = getEM()->getKind(opName);
05086   switch(kind) {
05087   case FORALL:
05088   case EXISTS: { // (OP ((v1 ... vn tp1) ...) body)
05089     if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() > 0))
05090       throw ParserException("Bad "+opName+" expression: "+e.toString());
05091     // Iterate through the groups of bound variables
05092     vector<pair<string,Type> > vars; // temporary stack of bound variables
05093     for(Expr::iterator i=e[1].begin(), iend=e[1].end(); i!=iend; ++i) {
05094       if(i->getKind() != RAW_LIST || i->arity() < 2)
05095   throw ParserException("Bad variable declaration block in "+opName
05096           +" expression: "+i->toString()
05097           +"\n e = "+e.toString());
05098       // Iterate through individual bound vars in the group.  The
05099       // last element is the type, which we have to rebuild and
05100       // parse, since it is used in the creation of bound variables.
05101       Type tp(parseExpr((*i)[i->arity()-1]));
05102       if (tp == boolType()) {
05103         throw ParserException("A quantified variable may not be of type BOOLEAN");
05104       }
05105       for(int j=0, jend=i->arity()-1; j<jend; ++j) {
05106   if((*i)[j].getKind() != ID)
05107     throw ParserException("Bad variable declaration in "+opName+""
05108             " expression: "+(*i)[j].toString()+
05109             "\n e = "+e.toString());
05110   vars.push_back(pair<string,Type>((*i)[j][0].getString(), tp));
05111       }
05112     }
05113     // Create all the bound vars and save them in a vector
05114     vector<Expr> boundVars;
05115     for(vector<pair<string,Type> >::iterator i=vars.begin(), iend=vars.end();
05116   i!=iend; ++i)
05117       boundVars.push_back(addBoundVar(i->first, i->second));
05118     // Rebuild the body
05119     Expr body(parseExpr(e[2]));
05120     // Build the resulting Expr as (OP (vars) body)
05121     Expr res = getEM()->newClosureExpr((kind == FORALL) ? FORALL : EXISTS,
05122                                        boundVars, body);
05123     return res;
05124     break;
05125   }
05126   default:
05127     DebugAssert(false,
05128     "TheoryQuant::parseExprOp: invalid command or expression: " + e.toString());
05129     break;
05130   }
05131   return e;
05132 }
05133 

Generated on Tue Jul 3 14:33:41 2007 for CVC3 by  doxygen 1.5.1