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