CVC3

theory_quant.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_quant.h
00004  * 
00005  * Author: Sergey Berezin, Yeting Ge
00006  * 
00007  * Created: Jun 24 21:13:59 GMT 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  * ! Author: Daniel Wichs
00019  * ! Created: Wednesday July 2, 2003
00020  *
00021  * 
00022  */
00023 /*****************************************************************************/
00024 #ifndef _cvc3__include__theory_quant_h_
00025 #define _cvc3__include__theory_quant_h_
00026 
00027 #include "theory.h"
00028 #include "cdmap.h"
00029 #include "statistics.h"
00030 #include<queue>
00031 
00032 namespace CVC3 {
00033 
00034 class QuantProofRules;
00035 
00036 /*****************************************************************************/
00037 /*!
00038  *\class TheoryQuant
00039  *\ingroup Theories
00040  *\brief This theory handles quantifiers.
00041  *
00042  * Author: Daniel Wichs
00043  *
00044  * Created: Wednesday July 2,  2003
00045  */
00046 /*****************************************************************************/
00047 
00048  typedef enum{ Ukn, Pos, Neg, PosNeg} Polarity;
00049 
00050  class Trigger {
00051  public: 
00052    Expr trig;
00053    Polarity polarity;
00054    
00055    std::vector<Expr> bvs;
00056    Expr head;
00057    bool hasRWOp;
00058    bool hasTrans;
00059    bool hasT2; //if has trans of 2,
00060    bool isSimple; //if of the form g(x,a);
00061    bool isSuperSimple; //if of the form g(x,y);
00062    bool isMulti;
00063    size_t multiIndex; 
00064    size_t multiId;
00065 
00066    Trigger(TheoryCore* core, Expr e, Polarity pol, std::set<Expr>);
00067    bool  isPos();
00068    bool  isNeg();
00069    Expr  getEx();
00070    std::vector<Expr> getBVs(); 
00071    void  setHead(Expr h);
00072    Expr  getHead();
00073    void  setRWOp(bool b);
00074    bool  hasRW(); 
00075    void  setTrans(bool b);
00076    bool  hasTr(); 
00077    void  setTrans2(bool b);
00078    bool  hasTr2(); 
00079    void  setSimp();
00080    bool  isSimp(); 
00081    void  setSuperSimp();
00082    bool  isSuperSimp(); 
00083    void  setMultiTrig();
00084    bool  isMultiTrig(); 
00085 
00086    
00087  };
00088 
00089  typedef struct dynTrig{
00090    Trigger trig;
00091    size_t univ_id;
00092    ExprMap<Expr> binds;
00093    dynTrig(Trigger t, ExprMap<Expr> b, size_t id);
00094  } dynTrig;
00095  
00096 
00097  class CompleteInstPreProcessor {
00098  
00099    TheoryCore* d_theoryCore; //needed by plusOne and minusOne;
00100    QuantProofRules* d_quant_rules;
00101 
00102    std::set<Expr> d_allIndex; //a set contains all index
00103 
00104    ExprMap<Polarity> d_expr_pol ;//map a expr to its polarity
00105 
00106    ExprMap<Expr> d_quant_equiv_map ; //map a quant to its equivalent form
00107 
00108    std::vector<Expr> d_gnd_cache; //cache of all ground formulas, before index can be collected, all such ground terms must be put into d_expr_pol.
00109    
00110    ExprMap<bool> d_is_macro_def;//if a quant is a macro quant
00111 
00112    ExprMap<Expr> d_macro_quant;//map a macro to its macro quant.
00113 
00114    ExprMap<Expr> d_macro_def;//map a macro head to its def.
00115 
00116    ExprMap<Expr> d_macro_lhs;//map a macro to its lhs.
00117    
00118    //! if all formulas checked so far are good
00119    bool d_all_good ;
00120 
00121    //! if e satisfies the shiled property, that is all bound vars are parameters of uninterpreted functions/predicates and array reads/writes
00122    bool isShield(const Expr& e);
00123 
00124    bool hasShieldVar(const Expr& e);
00125 
00126    //! insert an index
00127    void addIndex(const Expr& e);
00128    
00129    void collect_shield_index(const Expr& e);
00130 
00131    void collect_forall_index(const Expr& forall_quant);
00132 
00133    //! if e is a quant in the array property fragmenet
00134    bool isGoodQuant(const Expr& e);
00135 
00136    //! return e+1
00137    Expr plusOne(const Expr& e);
00138 
00139    //! return e-1
00140    Expr minusOne(const Expr& e);
00141 
00142    void collectHeads(const Expr& assert, std::set<Expr>& heads);
00143    
00144    //! if assert is a macro definition
00145    bool isMacro(const Expr& assert);
00146 
00147    Expr recInstMacros(const Expr& assert);
00148 
00149    Expr substMacro(const Expr&);
00150 
00151    Expr recRewriteNot(const Expr&, ExprMap<Polarity>&);
00152 
00153    //! rewrite neg polarity forall / exists to pos polarity
00154    Expr rewriteNot(const Expr &);
00155    
00156    Expr recSkolemize(const Expr &, ExprMap<Polarity>&);
00157 
00158    Expr pullVarOut(const Expr&);
00159 
00160  public :
00161 
00162    CompleteInstPreProcessor(TheoryCore * , QuantProofRules*);
00163 
00164    //! if e is a formula in the array property fragment 
00165    bool isGood(const Expr& e);
00166 
00167    //! collect index for instantiation
00168    void collectIndex(const Expr & e);
00169 
00170    //! inst forall quant using index from collectIndex
00171    Expr inst(const Expr & e);
00172 
00173    //! if there are macros
00174    bool hasMacros(const std::vector<Expr>& asserts);
00175 
00176    //! substitute a macro in assert
00177    Expr instMacros(const Expr& , const Expr );
00178 
00179    //! simplify a=a to True
00180    Expr simplifyEq(const Expr &);
00181    
00182    //! put all quants in postive form and then skolemize all exists 
00183    Expr simplifyQuant(const Expr &);
00184  };
00185  
00186  class TheoryQuant :public Theory {
00187    
00188    Theorem rewrite(const Expr& e);
00189 
00190    Theorem theoryPreprocess(const Expr& e);
00191 
00192    class  TypeComp { //!< needed for typeMap
00193    public:
00194      bool operator() (const Type t1, const Type t2) const
00195      {return (t1.getExpr() < t2.getExpr()); }
00196    };
00197 
00198   //! used to facilitate instantiation of universal quantifiers
00199   typedef std::map<Type, std::vector<size_t>, TypeComp > typeMap; 
00200 
00201   //! database of universally quantified theorems
00202   CDList<Theorem> d_univs; 
00203 
00204   CDList<Theorem> d_rawUnivs; 
00205 
00206   CDList<dynTrig> d_arrayTrigs; 
00207   CDO<size_t> d_lastArrayPos;
00208 
00209   //! universally quantified formulas to be instantiated, the var bindings is in d_bingQueue and the ground term matched with the trigger is in d_gtermQueue 
00210   std::queue<Theorem> d_univsQueue;
00211 
00212   std::queue<Theorem> d_simplifiedThmQueue;
00213 
00214   std::queue<Theorem> d_gUnivQueue;
00215   
00216   std::queue<Expr> d_gBindQueue;
00217 
00218 
00219   ExprMap<std::set<std::vector<Expr> > >  d_tempBinds;
00220 
00221   //!tracks the possition of preds 
00222   CDO<size_t> d_lastPredsPos;
00223   //!tracks the possition of terms 
00224   CDO<size_t> d_lastTermsPos;
00225 
00226   //!tracks the positions of preds for partial instantiation
00227   CDO<size_t> d_lastPartPredsPos;
00228   //!tracks the possition of terms for partial instantiation
00229   CDO<size_t> d_lastPartTermsPos;
00230   //!tracks a possition in the database of universals for partial instantiation
00231   CDO<size_t> d_univsPartSavedPos;
00232   
00233   //! the last decision level on which partial instantion is called
00234   CDO<size_t> d_lastPartLevel;
00235 
00236   CDO<bool> d_partCalled;
00237   
00238   //! the max instantiation level reached
00239   CDO<bool> d_maxILReached;
00240 
00241 
00242   
00243   //!useful gterms for matching
00244   CDList<Expr> d_usefulGterms; 
00245 
00246   //!tracks the position in d_usefulGterms
00247   CDO<size_t> d_lastUsefulGtermsPos;
00248   
00249   //!tracks a possition in the savedTerms map
00250   CDO<size_t> d_savedTermsPos;
00251   //!tracks a possition in the database of universals
00252   CDO<size_t> d_univsSavedPos;
00253   CDO<size_t> d_rawUnivsSavedPos;
00254   //!tracks a possition in the database of universals
00255   CDO<size_t> d_univsPosFull;
00256   //!tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed when fulleffort=0 only.
00257 
00258   CDO<size_t> d_univsContextPos;
00259   
00260   
00261   CDO<int> d_instCount; //!< number of instantiations made in given context
00262 
00263   //! set if the fullEffort = 1
00264   int d_inEnd; 
00265 
00266   int d_allout; 
00267 
00268   //! a map of types to posisitions in the d_contextTerms list
00269   std::map<Type, CDList<size_t>* ,TypeComp> d_contextMap;
00270   //! a list of all the terms appearing in the current context
00271   CDList<Expr> d_contextTerms;
00272   //!< chache of expressions
00273   CDMap<Expr, bool> d_contextCache;
00274   
00275   //! a map of types to positions in the d_savedTerms vector
00276   typeMap d_savedMap;
00277   ExprMap<bool> d_savedCache; //!< cache of expressions
00278   //! a vector of all of the terms that have produced conflicts.
00279   std::vector<Expr> d_savedTerms; 
00280 
00281   //! a map of instantiated universals to a vector of their instantiations
00282   ExprMap<std::vector<Expr> >  d_insts;
00283 
00284   //! quantifier theorem production rules
00285   QuantProofRules* d_rules;
00286   
00287   const int* d_maxQuantInst; //!< Command line option
00288 
00289   /*! \brief categorizes all the terms contained in an expressions by
00290    *type.
00291    *
00292    * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
00293    * returns true if the expression does not contain bound variables, false
00294    * otherwise.
00295    */
00296   bool recursiveMap(const Expr& term);
00297 
00298   /*! \brief categorizes all the terms contained in a vector of  expressions by
00299    * type.
00300    *
00301    * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
00302    */
00303   void mapTermsByType(const CDList<Expr>& terms);
00304   
00305   /*! \brief Queues up all possible instantiations of bound
00306    * variables.
00307    *
00308    * The savedMap boolean indicates whether to use savedMap or
00309    * d_contextMap the all boolean indicates weather to use all
00310    * instantiation or only new ones and newIndex is the index where
00311    * new instantiations begin.
00312    */
00313   void instantiate(Theorem univ, bool all, bool savedMap, 
00314        size_t newIndex);
00315   //! does most of the work of the instantiate function.
00316   void recInstantiate(Theorem& univ , bool all, bool savedMap,size_t newIndex, 
00317            std::vector<Expr>& varReplacements);
00318 
00319   /*! \brief A recursive function used to find instantiated universals
00320    * in the hierarchy of assumptions.
00321    */
00322   void findInstAssumptions(const Theorem& thm);
00323 
00324   //  CDO<bool> usedup;
00325   const bool* d_useNew;//!use new way of instantiation
00326   const bool* d_useLazyInst;//!use lazy instantiation
00327   const bool* d_useSemMatch;//!use semantic matching
00328   const bool* d_useCompleteInst; //! Try complete instantiation 
00329   const bool* d_translate;//!translate only
00330 
00331   const bool* d_usePart;//!use partial instantiaion
00332   const bool* d_useMult;//use 
00333   //  const bool* d_useInstEnd;
00334   const bool* d_useInstLCache;
00335   const bool* d_useInstGCache;
00336   const bool* d_useInstThmCache;
00337   const bool* d_useInstTrue;
00338   const bool* d_usePullVar;
00339   const bool* d_useExprScore;
00340   const int* d_useTrigLoop;
00341   const int* d_maxInst;
00342   //  const int* d_maxUserScore;
00343   const int*  d_maxIL;
00344   const bool* d_useTrans;
00345   const bool* d_useTrans2;
00346   const bool* d_useManTrig;
00347   const bool* d_useGFact;
00348   const int* d_gfactLimit;
00349   const bool* d_useInstAll;
00350   const bool* d_usePolarity;
00351   const bool* d_useEqu;
00352   const bool* d_useNewEqu;
00353   const int* d_maxNaiveCall;
00354   const bool* d_useNaiveInst;
00355 
00356 
00357   CDO<int> d_curMaxExprScore;
00358 
00359   bool d_useFullTrig;
00360   bool d_usePartTrig;
00361   bool d_useMultTrig;
00362 
00363   //ExprMap<std::vector<Expr> > d_arrayIndic; //map array name to a list of indics
00364   CDMap<Expr, std::vector<Expr> > d_arrayIndic; //map array name to a list of indics
00365   void arrayIndexName(const Expr& e);
00366 
00367   std::vector<Expr> d_allInsts; //! all instantiations
00368 
00369   int d_initMaxScore;
00370   int d_offset_multi_trig ;
00371   
00372   int d_instThisRound;
00373   int d_callThisRound;
00374 
00375   int partial_called;
00376 
00377   //  ExprMap<std::vector<Expr> > d_fullTriggers;
00378   //for multi-triggers, now we only have one set of multi-triggers.
00379 
00380 
00381   ExprMap<std::vector<Expr> > d_multTriggers;
00382   ExprMap<std::vector<Expr> > d_partTriggers;
00383 
00384   ExprMap<std::vector<Trigger> > d_fullTrigs;
00385   //for multi-triggers, now we only have one set of multi-triggers.
00386   ExprMap<std::vector<Trigger> > d_multTrigs;
00387   ExprMap<std::vector<Trigger> > d_partTrigs;
00388 
00389  
00390   CDO<size_t> d_exprLastUpdatedPos ;//the position of the last expr updated in d_exprUpdate 
00391 
00392   std::map<ExprIndex, int> d_indexScore;
00393 
00394   std::map<ExprIndex, Expr> d_indexExpr;
00395 
00396   int getExprScore(const Expr& e);
00397 
00398   //!the score for a full trigger
00399   
00400   ExprMap<bool> d_hasTriggers;
00401   ExprMap<bool> d_hasMoreBVs;
00402 
00403   int d_trans_num;
00404   int d_trans2_num;
00405 
00406   typedef struct{
00407     std::vector<std::vector<size_t> > common_pos;
00408     std::vector<std::vector<size_t> > var_pos; 
00409     
00410     std::vector<CDMap<Expr, bool>* > var_binds_found;
00411 
00412     std::vector<ExprMap<CDList<Expr>* >* > uncomm_list; //
00413     Theorem univThm; // for test only
00414     size_t univ_id; // for test only
00415   } multTrigsInfo ;
00416   
00417   ExprMap<multTrigsInfo> d_multitrigs_maps;
00418   std::vector<multTrigsInfo> d_all_multTrigsInfo;
00419   
00420   ExprMap<CDList<Expr>* > d_trans_back;
00421   ExprMap<CDList<Expr>* > d_trans_forw;
00422   CDMap<Expr,bool > d_trans_found;
00423   CDMap<Expr,bool > d_trans2_found;
00424 
00425 
00426   inline  bool transFound(const Expr& comb);
00427   
00428   inline   void setTransFound(const Expr& comb);
00429 
00430   inline  bool trans2Found(const Expr& comb);
00431 
00432   inline  void setTrans2Found(const Expr& comb);
00433 
00434  
00435   inline  CDList<Expr> & backList(const Expr& ex);
00436   
00437   inline  CDList<Expr> & forwList(const Expr& ex);
00438 
00439   void inline iterFWList(const Expr& sr, const Expr& dt, size_t univ_id, const Expr& gterm);
00440   void inline iterBKList(const Expr& sr, const Expr& dt, size_t univ_id, const Expr& gterm);
00441 
00442   Expr defaultWriteExpr;
00443   Expr defaultReadExpr;
00444   Expr defaultPlusExpr;
00445   Expr  defaultMinusExpr ;
00446   Expr  defaultMultExpr ;
00447   Expr  defaultDivideExpr;
00448   Expr  defaultPowExpr ;
00449 
00450   Expr getHead(const Expr& e) ;
00451   Expr getHeadExpr(const Expr& e) ;
00452 
00453 
00454 
00455   CDList<Expr> null_cdlist;
00456 
00457   Theorem d_transThm;
00458 
00459   inline  void  pushBackList(const Expr& node, Expr ex);
00460   inline  void  pushForwList(const Expr& node, Expr ex);
00461   
00462   
00463   ExprMap<CDList<std::vector<Expr> >* > d_mtrigs_inst; //map expr to bindings
00464   
00465   ExprMap<CDList<Expr>* > d_same_head_expr; //map an expr to a list of expres shard the same head
00466   ExprMap<CDList<Expr>* > d_eq_list; //the equalities list
00467 
00468   CDList<Theorem> d_eqsUpdate; //the equalities list collected from update()
00469   CDO<size_t> d_lastEqsUpdatePos;
00470 
00471   CDList<Expr > d_eqs; //the equalities list
00472   CDO<size_t > d_eqs_pos; //the equalities list
00473 
00474   ExprMap<CDO<size_t>* > d_eq_pos;
00475 
00476   ExprMap<CDList<Expr>* > d_parent_list; 
00477   void  collectChangedTerms(CDList<Expr>& changed_terms);
00478   ExprMap<std::vector<Expr> > d_mtrigs_bvorder;
00479 
00480   int loc_gterm(const std::vector<Expr>& border,
00481     const Expr& gterm, 
00482     int pos);
00483 
00484   void  recSearchCover(const std::vector<Expr>& border,
00485            const std::vector<Expr>& mtrigs, 
00486            int cur_depth, 
00487            std::vector<std::vector<Expr> >& instSet,
00488            std::vector<Expr>& cur_inst
00489            );
00490 
00491   void  searchCover(const Expr& thm, 
00492         const std::vector<Expr>& border,
00493         std::vector<std::vector<Expr> >& instSet
00494         );
00495 
00496 
00497   std::map<Type, std::vector<Expr>,TypeComp > d_typeExprMap;
00498   std::set<std::string> cacheHead;
00499 
00500   StatCounter d_allInstCount ; //the number instantiations asserted in SAT
00501   StatCounter d_allInstCount2 ; 
00502   StatCounter d_totalInstCount ;// the total number of instantiations.
00503   StatCounter d_trueInstCount;//the number of instantiation simplified to be true.
00504   StatCounter d_abInstCount;
00505 
00506   //  size_t d_totalInstCount;
00507   //  size_t d_trueInstCount;
00508   //  size_t d_abInstCount;
00509   
00510 
00511 
00512   std::vector<Theorem> d_cacheTheorem;
00513   size_t d_cacheThmPos;
00514 
00515   void addNotify(const Expr& e);
00516 
00517   int sendInstNew();
00518 
00519   CDMap<Expr, std::set<std::vector<Expr> > > d_instHistory;//the history of instantiations
00520   //map univ to the trig, gterm and result
00521 
00522   ExprMap<int> d_thmCount; 
00523   ExprMap<size_t> d_totalThmCount; 
00524 
00525   ExprMap<CDMap<Expr, bool>* > d_bindHistory; //the history of instantiations
00526   ExprMap<std::hash_map<Expr, bool>* > d_bindGlobalHistory; //the history of instantiations
00527 
00528   ExprMap<std::hash_map<Expr, Theorem>* > d_bindGlobalThmHistory; //the history of instantiations
00529 
00530   ExprMap<std::set<std::vector<Expr> > > d_instHistoryGlobal;//the history of instantiations
00531 
00532   
00533   ExprMap<std::vector<Expr> > d_subTermsMap;
00534   //std::map<Expr, std::vector<Expr> > d_subTermsMap;
00535   const std::vector<Expr>& getSubTerms(const Expr& e);
00536 
00537 
00538   void simplifyExprMap(ExprMap<Expr>& orgExprMap);
00539   void simplifyVectorExprMap(std::vector<ExprMap<Expr> >& orgVectorExprMap);
00540   std::string exprMap2string(const ExprMap<Expr>& vec);
00541   std::string exprMap2stringSimplify(const ExprMap<Expr>& vec);
00542   std::string exprMap2stringSig(const ExprMap<Expr>& vec);
00543 
00544   //ExprMap<int > d_thmTimes; 
00545   void enqueueInst(const Theorem, const Theorem); 
00546   void enqueueInst(const Theorem& univ, const std::vector<Expr>& bind, const Expr& gterm);
00547   void enqueueInst(size_t univ_id , const std::vector<Expr>& bind, const Expr& gterm);
00548   void enqueueInst(const Theorem& univ, 
00549        Trigger& trig,
00550        const std::vector<Expr>& binds,  
00551        const Expr& gterm
00552        );
00553     
00554   void synCheckSat(ExprMap<ExprMap<std::vector<dynTrig>* >* >& , bool);
00555   void synCheckSat(bool);
00556   void semCheckSat(bool);
00557   void naiveCheckSat(bool);
00558 
00559   bool insted(const Theorem & univ, const std::vector<Expr>& binds);
00560   void synInst(const Theorem & univ,  const CDList<Expr>& allterms, size_t tBegin);
00561 
00562   void synFullInst(const Theorem & univ,  const CDList<Expr>& allterms, size_t tBegin);
00563 
00564   void arrayHeuristic(const Trigger& trig, size_t univid);
00565   
00566   Expr simpRAWList(const Expr& org);
00567 
00568   void synNewInst(size_t univ_id, const std::vector<Expr>& binds, const Expr& gterm, const Trigger& trig );
00569   void synMultInst(const Theorem & univ,  const CDList<Expr>& allterms,  size_t tBegin);
00570 
00571   void synPartInst(const Theorem & univ,  const CDList<Expr>& allterms,  size_t tBegin);
00572 
00573   void semInst(const Theorem & univ, size_t tBegin);
00574 
00575 
00576   void goodSynMatch(const Expr& e,
00577         const std::vector<Expr> & boundVars,
00578         std::vector<std::vector<Expr> >& instBindsTerm,
00579         std::vector<Expr>& instGterm,
00580         const CDList<Expr>& allterms,          
00581         size_t tBegin);
00582   void goodSynMatchNewTrig(const Trigger& trig,
00583          const std::vector<Expr> & boundVars,
00584          std::vector<std::vector<Expr> >& instBinds,
00585          std::vector<Expr>& instGterms,
00586          const CDList<Expr>& allterms,           
00587          size_t tBegin);
00588 
00589   bool goodSynMatchNewTrig(const Trigger& trig,
00590          const std::vector<Expr> & boundVars,
00591          std::vector<std::vector<Expr> >& instBinds,
00592          std::vector<Expr>& instGterms,
00593          const Expr& gterm);
00594 
00595   void matchListOld(const CDList<Expr>& list, size_t gbegin, size_t gend);
00596     //  void matchListOld(const Expr& gterm);
00597   void matchListNew(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs,
00598         const CDList<Expr>& list,
00599         size_t gbegin,
00600         size_t gend);
00601   
00602   void delNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs);
00603   void combineOldNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs);
00604 
00605   inline void add_parent(const Expr& parent);
00606 
00607   void newTopMatch(const Expr& gterm, 
00608        const Expr& vterm, 
00609        std::vector<ExprMap<Expr> >& binds, 
00610        const Trigger& trig);
00611 
00612   void newTopMatchSig(const Expr& gterm, 
00613           const Expr& vterm, 
00614           std::vector<ExprMap<Expr> >& binds, 
00615           const Trigger& trig);
00616   
00617   void newTopMatchNoSig(const Expr& gterm, 
00618       const Expr& vterm, 
00619       std::vector<ExprMap<Expr> >& binds, 
00620       const Trigger& trig);
00621 
00622 
00623 
00624   void newTopMatchBackupOnly(const Expr& gterm, 
00625            const Expr& vterm, 
00626            std::vector<ExprMap<Expr> >& binds, 
00627            const Trigger& trig);
00628 
00629 
00630   bool synMatchTopPred(const Expr& gterm, const Trigger trig, ExprMap<Expr>& env);
00631 
00632   //  inline bool matchChild(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env);
00633   //  inline void matchChild(const Expr& gterm, const Expr& vterm, std::vector<ExprMap<Expr> >& env);
00634   
00635   bool recSynMatch(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env);
00636 
00637   bool recMultMatch(const Expr& gterm,const Expr& vterm, std::vector<ExprMap<Expr> >& binds);
00638   bool recMultMatchDebug(const Expr& gterm,const Expr& vterm, std::vector<ExprMap<Expr> >& binds);
00639   bool recMultMatchNewWay(const Expr& gterm,const Expr& vterm, std::vector<ExprMap<Expr> >& binds);
00640   bool recMultMatchOldWay(const Expr& gterm,const Expr& vterm, std::vector<ExprMap<Expr> >& binds);
00641 
00642   inline bool multMatchChild(const Expr& gterm, const Expr& vterm, std::vector<ExprMap<Expr> >& binds, bool top=false);
00643   inline bool multMatchTop(const Expr& gterm, const Expr& vterm, std::vector<ExprMap<Expr> >& binds);
00644 
00645 
00646   bool recSynMatchBackupOnly(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env);
00647 
00648   bool hasGoodSynInstNewTrigOld(Trigger& trig, 
00649         std::vector<Expr> & boundVars, 
00650         std::vector<std::vector<Expr> >& instBinds, 
00651         std::vector<Expr>& instGterms, 
00652         const CDList<Expr>& allterms,          
00653         size_t tBegin); 
00654   
00655   bool hasGoodSynInstNewTrig(Trigger& trig, 
00656            const std::vector<Expr> & boundVars, 
00657              std::vector<std::vector<Expr> >& instBinds, 
00658            std::vector<Expr>& instGterms, 
00659            const CDList<Expr>& allterms,           
00660            size_t tBegin); 
00661 
00662 
00663   bool hasGoodSynMultiInst(const Expr& e,
00664          std::vector<Expr>& bVars,
00665          std::vector<std::vector<Expr> >& instSet,
00666          const CDList<Expr>& allterms,           
00667          size_t tBegin);
00668   
00669   void recGoodSemMatch(const Expr& e,
00670            const std::vector<Expr>& bVars,
00671            std::vector<Expr>& newInst,
00672            std::set<std::vector<Expr> >& instSet);
00673   
00674   bool hasGoodSemInst(const Expr& e,
00675        std::vector<Expr>& bVars,
00676        std::set<std::vector<Expr> >& instSet,
00677        size_t tBegin);
00678 
00679   bool isTransLike (const std::vector<Expr>& cur_trig);
00680   bool isTrans2Like (const std::vector<Expr>& all_terms, const Expr& tr2);
00681   
00682 
00683   static const size_t MAX_TRIG_BVS=15;
00684   Expr d_mybvs[MAX_TRIG_BVS];
00685  
00686   Expr recGeneralTrig(const Expr& trig, ExprMap<Expr>& bvs, size_t& mybvs_count);
00687   Expr generalTrig(const Expr& trig, ExprMap<Expr>& bvs);
00688 
00689   ExprMap<CDMap<Expr, CDList<dynTrig>* >* > d_allmap_trigs;
00690   
00691   CDList<Trigger> d_alltrig_list;
00692 
00693   void registerTrig(ExprMap<ExprMap<std::vector<dynTrig>* >* >& cur_trig_map,
00694        Trigger trig, 
00695        const std::vector<Expr> thmBVs, 
00696        size_t univ_id);
00697     
00698   void registerTrigReal(Trigger trig, const std::vector<Expr>, size_t univ_id);
00699 
00700   bool canMatch(const Expr& t1, const Expr& t2, ExprMap<Expr>& env);
00701   void setGround(const Expr& gterm, const Expr& trig, const Theorem& univ, const std::vector<Expr>& subTerms) ;    
00702 
00703   //  std::string getHead(const Expr& e) ;
00704   void setupTriggers(ExprMap<ExprMap<std::vector<dynTrig>* >*>& trig_maps,
00705          const Theorem& thm, 
00706          size_t univs_id);
00707 
00708   void saveContext();
00709 
00710 
00711   /*! \brief categorizes all the terms contained in an expressions by
00712    *type.
00713    *
00714    * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
00715    * returns true if the expression does not contain bound variables, false
00716    * otherwise.
00717    */
00718 
00719   
00720  public:
00721   TheoryQuant(TheoryCore* core); //!< Constructor
00722   ~TheoryQuant(); //! Destructor
00723 
00724   QuantProofRules* createProofRules();
00725   
00726 
00727  
00728   void addSharedTerm(const Expr& e) {} //!< Theory interface
00729   
00730   /*! \brief Theory interface function to assert quantified formulas
00731    *
00732    * pushes in negations and converts to either universally or existentially 
00733    * quantified theorems. Universals are stored in a database while 
00734    * existentials are enqueued to be handled by the search engine.
00735    */
00736   void assertFact(const Theorem& e); 
00737   
00738 
00739   /* \brief Checks the satisfiability of the universal theorems stored in a 
00740    * databse by instantiating them.
00741    *
00742    * There are two algorithms that the checkSat function uses to find 
00743    * instnatiations. The first algortihm looks for instanitations in a saved 
00744    * database of previous instantiations that worked in proving an earlier
00745    * theorem unsatifiable. All of the class variables with the word saved in
00746    * them  are for the use of this algorithm. The other algorithm uses terms 
00747    * found in the assertions that exist in the particular context when 
00748    * checkSat is called. All of the class variables with the word context in
00749    * them are used for the second algorithm.
00750    */
00751   void checkSat(bool fullEffort);
00752   void setup(const Expr& e); 
00753   
00754   int help(int i);
00755   
00756   void update(const Theorem& e, const Expr& d);
00757   /*!\brief Used to notify the quantifier algorithm of possible 
00758    * instantiations that were used in proving a context inconsistent.
00759    */
00760   void debug(int i);
00761   void notifyInconsistent(const Theorem& thm); 
00762   //! computes the type of a quantified term. Always a  boolean.
00763   void computeType(const Expr& e); 
00764   Expr computeTCC(const Expr& e);
00765   
00766   virtual Expr parseExprOp(const Expr& e);
00767 
00768   ExprStream& print(ExprStream& os, const Expr& e);
00769  };
00770  
00771 }
00772 
00773 #endif