CVC3  2.4.1
theory_quant.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_quant.h
4  *
5  * Author: Sergey Berezin, Yeting Ge
6  *
7  * Created: Jun 24 21:13:59 GMT 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  * ! Author: Daniel Wichs
19  * ! Created: Wednesday July 2, 2003
20  *
21  *
22  */
23 /*****************************************************************************/
24 #ifndef _cvc3__include__theory_quant_h_
25 #define _cvc3__include__theory_quant_h_
26 
27 #include "theory.h"
28 #include "cdmap.h"
29 #include "statistics.h"
30 #include<queue>
31 
32 namespace CVC3 {
33 
34 class QuantProofRules;
35 
36 /*****************************************************************************/
37 /*!
38  *\class TheoryQuant
39  *\ingroup Theories
40  *\brief This theory handles quantifiers.
41  *
42  * Author: Daniel Wichs
43  *
44  * Created: Wednesday July 2, 2003
45  */
46 /*****************************************************************************/
47 
48  typedef enum{ Ukn, Pos, Neg, PosNeg} Polarity;
49 
50  class Trigger {
51  public:
54 
55  std::vector<Expr> bvs;
57  bool hasRWOp;
58  bool hasTrans;
59  bool hasT2; //if has trans of 2,
60  bool isSimple; //if of the form g(x,a);
61  bool isSuperSimple; //if of the form g(x,y);
62  bool isMulti;
63  size_t multiIndex;
64  size_t multiId;
65 
66  Trigger(TheoryCore* core, Expr e, Polarity pol, std::set<Expr>);
67  bool isPos();
68  bool isNeg();
69  Expr getEx();
70  std::vector<Expr> getBVs();
71  void setHead(Expr h);
72  Expr getHead();
73  void setRWOp(bool b);
74  bool hasRW();
75  void setTrans(bool b);
76  bool hasTr();
77  void setTrans2(bool b);
78  bool hasTr2();
79  void setSimp();
80  bool isSimp();
81  void setSuperSimp();
82  bool isSuperSimp();
83  void setMultiTrig();
84  bool isMultiTrig();
85 
86 
87  };
88 
89  typedef struct dynTrig{
91  size_t univ_id;
93  dynTrig(Trigger t, ExprMap<Expr> b, size_t id);
94  } dynTrig;
95 
96 
98 
99  TheoryCore* d_theoryCore; //needed by plusOne and minusOne;
101 
102  std::set<Expr> d_allIndex; //a set contains all index
103 
104  ExprMap<Polarity> d_expr_pol ;//map a expr to its polarity
105 
106  ExprMap<Expr> d_quant_equiv_map ; //map a quant to its equivalent form
107 
108  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.
109 
110  ExprMap<bool> d_is_macro_def;//if a quant is a macro quant
111 
112  ExprMap<Expr> d_macro_quant;//map a macro to its macro quant.
113 
114  ExprMap<Expr> d_macro_def;//map a macro head to its def.
115 
116  ExprMap<Expr> d_macro_lhs;//map a macro to its lhs.
117 
118  //! if all formulas checked so far are good
119  bool d_all_good ;
120 
121  //! if e satisfies the shiled property, that is all bound vars are parameters of uninterpreted functions/predicates and array reads/writes
122  bool isShield(const Expr& e);
123 
124  bool hasShieldVar(const Expr& e);
125 
126  //! insert an index
127  void addIndex(const Expr& e);
128 
129  void collect_shield_index(const Expr& e);
130 
131  void collect_forall_index(const Expr& forall_quant);
132 
133  //! if e is a quant in the array property fragmenet
134  bool isGoodQuant(const Expr& e);
135 
136  //! return e+1
137  Expr plusOne(const Expr& e);
138 
139  //! return e-1
140  Expr minusOne(const Expr& e);
141 
142  void collectHeads(const Expr& assert, std::set<Expr>& heads);
143 
144  //! if assert is a macro definition
145  bool isMacro(const Expr& assert);
146 
147  Expr recInstMacros(const Expr& assert);
148 
149  Expr substMacro(const Expr&);
150 
152 
153  //! rewrite neg polarity forall / exists to pos polarity
154  Expr rewriteNot(const Expr &);
155 
157 
158  Expr pullVarOut(const Expr&);
159 
160  public :
161 
163 
164  //! if e is a formula in the array property fragment
165  bool isGood(const Expr& e);
166 
167  //! collect index for instantiation
168  void collectIndex(const Expr & e);
169 
170  //! inst forall quant using index from collectIndex
171  Expr inst(const Expr & e);
172 
173  //! if there are macros
174  bool hasMacros(const std::vector<Expr>& asserts);
175 
176  //! substitute a macro in assert
177  Expr instMacros(const Expr& , const Expr );
178 
179  //! simplify a=a to True
180  Expr simplifyEq(const Expr &);
181 
182  //! put all quants in postive form and then skolemize all exists
183  Expr simplifyQuant(const Expr &);
184  };
185 
186  class TheoryQuant :public Theory {
187 
188  Theorem rewrite(const Expr& e);
189 
190  Theorem theoryPreprocess(const Expr& e);
191 
192  class TypeComp { //!< needed for typeMap
193  public:
194  bool operator() (const Type t1, const Type t2) const
195  {return (t1.getExpr() < t2.getExpr()); }
196  };
197 
198  //! used to facilitate instantiation of universal quantifiers
199  typedef std::map<Type, std::vector<size_t>, TypeComp > typeMap;
200 
201  //! database of universally quantified theorems
203 
205 
208 
209  //! 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
210  std::queue<Theorem> d_univsQueue;
211 
212  std::queue<Theorem> d_simplifiedThmQueue;
213 
214  std::queue<Theorem> d_gUnivQueue;
215 
216  std::queue<Expr> d_gBindQueue;
217 
218 
220 
221  //!tracks the possition of preds
223  //!tracks the possition of terms
225 
226  //!tracks the positions of preds for partial instantiation
228  //!tracks the possition of terms for partial instantiation
230  //!tracks a possition in the database of universals for partial instantiation
232 
233  //! the last decision level on which partial instantion is called
235 
237 
238  //! the max instantiation level reached
240 
241 
242 
243  //!useful gterms for matching
245 
246  //!tracks the position in d_usefulGterms
248 
249  //!tracks a possition in the savedTerms map
251  //!tracks a possition in the database of universals
254  //!tracks a possition in the database of universals
256  //!tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed when fulleffort=0 only.
257 
259 
260 
261  CDO<int> d_instCount; //!< number of instantiations made in given context
262 
263  //! set if the fullEffort = 1
264  int d_inEnd;
265 
266  int d_allout;
267 
268  //! a map of types to posisitions in the d_contextTerms list
269  std::map<Type, CDList<size_t>* ,TypeComp> d_contextMap;
270  //! a list of all the terms appearing in the current context
272  //!< chache of expressions
274 
275  //! a map of types to positions in the d_savedTerms vector
276  typeMap d_savedMap;
277  ExprMap<bool> d_savedCache; //!< cache of expressions
278  //! a vector of all of the terms that have produced conflicts.
279  std::vector<Expr> d_savedTerms;
280 
281  //! a map of instantiated universals to a vector of their instantiations
283 
284  //! quantifier theorem production rules
286 
287  const int* d_maxQuantInst; //!< Command line option
288 
289  /*! \brief categorizes all the terms contained in an expressions by
290  *type.
291  *
292  * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
293  * returns true if the expression does not contain bound variables, false
294  * otherwise.
295  */
296  bool recursiveMap(const Expr& term);
297 
298  /*! \brief categorizes all the terms contained in a vector of expressions by
299  * type.
300  *
301  * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
302  */
303  void mapTermsByType(const CDList<Expr>& terms);
304 
305  /*! \brief Queues up all possible instantiations of bound
306  * variables.
307  *
308  * The savedMap boolean indicates whether to use savedMap or
309  * d_contextMap the all boolean indicates weather to use all
310  * instantiation or only new ones and newIndex is the index where
311  * new instantiations begin.
312  */
313  void instantiate(Theorem univ, bool all, bool savedMap,
314  size_t newIndex);
315  //! does most of the work of the instantiate function.
316  void recInstantiate(Theorem& univ , bool all, bool savedMap,size_t newIndex,
317  std::vector<Expr>& varReplacements);
318 
319  /*! \brief A recursive function used to find instantiated universals
320  * in the hierarchy of assumptions.
321  */
322  void findInstAssumptions(const Theorem& thm);
323 
324  // CDO<bool> usedup;
325  const bool* d_useNew;//!use new way of instantiation
326  const bool* d_useLazyInst;//!use lazy instantiation
327  const bool* d_useSemMatch;//!use semantic matching
328  const bool* d_useCompleteInst; //! Try complete instantiation
329  const bool* d_translate;//!translate only
330 
331  const bool* d_usePart;//!use partial instantiaion
332  const bool* d_useMult;//use
333  // const bool* d_useInstEnd;
334  const bool* d_useInstLCache;
335  const bool* d_useInstGCache;
336  const bool* d_useInstThmCache;
337  const bool* d_useInstTrue;
338  const bool* d_usePullVar;
339  const bool* d_useExprScore;
340  const int* d_useTrigLoop;
341  const int* d_maxInst;
342  // const int* d_maxUserScore;
343  const int* d_maxIL;
344  const bool* d_useTrans;
345  const bool* d_useTrans2;
346  const bool* d_useManTrig;
347  const bool* d_useGFact;
348  const int* d_gfactLimit;
349  const bool* d_useInstAll;
350  const bool* d_usePolarity;
351  const bool* d_useEqu;
352  const bool* d_useNewEqu;
353  const int* d_maxNaiveCall;
354  const bool* d_useNaiveInst;
355 
356 
358 
362 
363  //ExprMap<std::vector<Expr> > d_arrayIndic; //map array name to a list of indics
364  CDMap<Expr, std::vector<Expr> > d_arrayIndic; //map array name to a list of indics
365  void arrayIndexName(const Expr& e);
366 
367  std::vector<Expr> d_allInsts; //! all instantiations
368 
371 
374 
376 
377  // ExprMap<std::vector<Expr> > d_fullTriggers;
378  //for multi-triggers, now we only have one set of multi-triggers.
379 
380 
383 
385  //for multi-triggers, now we only have one set of multi-triggers.
388 
389 
390  CDO<size_t> d_exprLastUpdatedPos ;//the position of the last expr updated in d_exprUpdate
391 
392  std::map<ExprIndex, int> d_indexScore;
393 
394  std::map<ExprIndex, Expr> d_indexExpr;
395 
396  int getExprScore(const Expr& e);
397 
398  //!the score for a full trigger
399 
402 
405 
406  typedef struct{
407  std::vector<std::vector<size_t> > common_pos;
408  std::vector<std::vector<size_t> > var_pos;
409 
410  std::vector<CDMap<Expr, bool>* > var_binds_found;
411 
412  std::vector<ExprMap<CDList<Expr>* >* > uncomm_list; //
413  Theorem univThm; // for test only
414  size_t univ_id; // for test only
415  } multTrigsInfo ;
416 
418  std::vector<multTrigsInfo> d_all_multTrigsInfo;
419 
424 
425 
426  inline bool transFound(const Expr& comb);
427 
428  inline void setTransFound(const Expr& comb);
429 
430  inline bool trans2Found(const Expr& comb);
431 
432  inline void setTrans2Found(const Expr& comb);
433 
434 
435  inline CDList<Expr> & backList(const Expr& ex);
436 
437  inline CDList<Expr> & forwList(const Expr& ex);
438 
439  void inline iterFWList(const Expr& sr, const Expr& dt, size_t univ_id, const Expr& gterm);
440  void inline iterBKList(const Expr& sr, const Expr& dt, size_t univ_id, const Expr& gterm);
441 
449 
450  Expr getHead(const Expr& e) ;
451  Expr getHeadExpr(const Expr& e) ;
452 
453 
454 
456 
458 
459  inline void pushBackList(const Expr& node, Expr ex);
460  inline void pushForwList(const Expr& node, Expr ex);
461 
462 
463  ExprMap<CDList<std::vector<Expr> >* > d_mtrigs_inst; //map expr to bindings
464 
465  ExprMap<CDList<Expr>* > d_same_head_expr; //map an expr to a list of expres shard the same head
466  ExprMap<CDList<Expr>* > d_eq_list; //the equalities list
467 
468  CDList<Theorem> d_eqsUpdate; //the equalities list collected from update()
470 
471  CDList<Expr > d_eqs; //the equalities list
472  CDO<size_t > d_eqs_pos; //the equalities list
473 
475 
477  void collectChangedTerms(CDList<Expr>& changed_terms);
479 
480  int loc_gterm(const std::vector<Expr>& border,
481  const Expr& gterm,
482  int pos);
483 
484  void recSearchCover(const std::vector<Expr>& border,
485  const std::vector<Expr>& mtrigs,
486  int cur_depth,
487  std::vector<std::vector<Expr> >& instSet,
488  std::vector<Expr>& cur_inst
489  );
490 
491  void searchCover(const Expr& thm,
492  const std::vector<Expr>& border,
493  std::vector<std::vector<Expr> >& instSet
494  );
495 
496 
497  std::map<Type, std::vector<Expr>,TypeComp > d_typeExprMap;
498  std::set<std::string> cacheHead;
499 
500  StatCounter d_allInstCount ; //the number instantiations asserted in SAT
502  StatCounter d_totalInstCount ;// the total number of instantiations.
503  StatCounter d_trueInstCount;//the number of instantiation simplified to be true.
505 
506  // size_t d_totalInstCount;
507  // size_t d_trueInstCount;
508  // size_t d_abInstCount;
509 
510 
511 
512  std::vector<Theorem> d_cacheTheorem;
514 
515  void addNotify(const Expr& e);
516 
517  int sendInstNew();
518 
519  CDMap<Expr, std::set<std::vector<Expr> > > d_instHistory;//the history of instantiations
520  //map univ to the trig, gterm and result
521 
524 
525  ExprMap<CDMap<Expr, bool>* > d_bindHistory; //the history of instantiations
526  ExprMap<std::hash_map<Expr, bool>* > d_bindGlobalHistory; //the history of instantiations
527 
529 
530  ExprMap<std::set<std::vector<Expr> > > d_instHistoryGlobal;//the history of instantiations
531 
532 
534  //std::map<Expr, std::vector<Expr> > d_subTermsMap;
535  const std::vector<Expr>& getSubTerms(const Expr& e);
536 
537 
538  void simplifyExprMap(ExprMap<Expr>& orgExprMap);
539  void simplifyVectorExprMap(std::vector<ExprMap<Expr> >& orgVectorExprMap);
540  std::string exprMap2string(const ExprMap<Expr>& vec);
541  std::string exprMap2stringSimplify(const ExprMap<Expr>& vec);
542  std::string exprMap2stringSig(const ExprMap<Expr>& vec);
543 
544  //ExprMap<int > d_thmTimes;
545  void enqueueInst(const Theorem, const Theorem);
546  void enqueueInst(const Theorem& univ, const std::vector<Expr>& bind, const Expr& gterm);
547  void enqueueInst(size_t univ_id , const std::vector<Expr>& bind, const Expr& gterm);
548  void enqueueInst(const Theorem& univ,
549  Trigger& trig,
550  const std::vector<Expr>& binds,
551  const Expr& gterm
552  );
553 
554  void synCheckSat(ExprMap<ExprMap<std::vector<dynTrig>* >* >& , bool);
555  void synCheckSat(bool);
556  void semCheckSat(bool);
557  void naiveCheckSat(bool);
558 
559  bool insted(const Theorem & univ, const std::vector<Expr>& binds);
560  void synInst(const Theorem & univ, const CDList<Expr>& allterms, size_t tBegin);
561 
562  void synFullInst(const Theorem & univ, const CDList<Expr>& allterms, size_t tBegin);
563 
564  void arrayHeuristic(const Trigger& trig, size_t univid);
565 
566  Expr simpRAWList(const Expr& org);
567 
568  void synNewInst(size_t univ_id, const std::vector<Expr>& binds, const Expr& gterm, const Trigger& trig );
569  void synMultInst(const Theorem & univ, const CDList<Expr>& allterms, size_t tBegin);
570 
571  void synPartInst(const Theorem & univ, const CDList<Expr>& allterms, size_t tBegin);
572 
573  void semInst(const Theorem & univ, size_t tBegin);
574 
575 
576  void goodSynMatch(const Expr& e,
577  const std::vector<Expr> & boundVars,
578  std::vector<std::vector<Expr> >& instBindsTerm,
579  std::vector<Expr>& instGterm,
580  const CDList<Expr>& allterms,
581  size_t tBegin);
582  void goodSynMatchNewTrig(const Trigger& trig,
583  const std::vector<Expr> & boundVars,
584  std::vector<std::vector<Expr> >& instBinds,
585  std::vector<Expr>& instGterms,
586  const CDList<Expr>& allterms,
587  size_t tBegin);
588 
589  bool goodSynMatchNewTrig(const Trigger& trig,
590  const std::vector<Expr> & boundVars,
591  std::vector<std::vector<Expr> >& instBinds,
592  std::vector<Expr>& instGterms,
593  const Expr& gterm);
594 
595  void matchListOld(const CDList<Expr>& list, size_t gbegin, size_t gend);
596  // void matchListOld(const Expr& gterm);
597  void matchListNew(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs,
598  const CDList<Expr>& list,
599  size_t gbegin,
600  size_t gend);
601 
602  void delNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs);
603  void combineOldNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs);
604 
605  inline void add_parent(const Expr& parent);
606 
607  void newTopMatch(const Expr& gterm,
608  const Expr& vterm,
609  std::vector<ExprMap<Expr> >& binds,
610  const Trigger& trig);
611 
612  void newTopMatchSig(const Expr& gterm,
613  const Expr& vterm,
614  std::vector<ExprMap<Expr> >& binds,
615  const Trigger& trig);
616 
617  void newTopMatchNoSig(const Expr& gterm,
618  const Expr& vterm,
619  std::vector<ExprMap<Expr> >& binds,
620  const Trigger& trig);
621 
622 
623 
624  void newTopMatchBackupOnly(const Expr& gterm,
625  const Expr& vterm,
626  std::vector<ExprMap<Expr> >& binds,
627  const Trigger& trig);
628 
629 
630  bool synMatchTopPred(const Expr& gterm, const Trigger trig, ExprMap<Expr>& env);
631 
632  // inline bool matchChild(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env);
633  // inline void matchChild(const Expr& gterm, const Expr& vterm, std::vector<ExprMap<Expr> >& env);
634 
635  bool recSynMatch(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env);
636 
637  bool recMultMatch(const Expr& gterm,const Expr& vterm, std::vector<ExprMap<Expr> >& binds);
638  bool recMultMatchDebug(const Expr& gterm,const Expr& vterm, std::vector<ExprMap<Expr> >& binds);
639  bool recMultMatchNewWay(const Expr& gterm,const Expr& vterm, std::vector<ExprMap<Expr> >& binds);
640  bool recMultMatchOldWay(const Expr& gterm,const Expr& vterm, std::vector<ExprMap<Expr> >& binds);
641 
642  inline bool multMatchChild(const Expr& gterm, const Expr& vterm, std::vector<ExprMap<Expr> >& binds, bool top=false);
643  inline bool multMatchTop(const Expr& gterm, const Expr& vterm, std::vector<ExprMap<Expr> >& binds);
644 
645 
646  bool recSynMatchBackupOnly(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env);
647 
648  bool hasGoodSynInstNewTrigOld(Trigger& trig,
649  std::vector<Expr> & boundVars,
650  std::vector<std::vector<Expr> >& instBinds,
651  std::vector<Expr>& instGterms,
652  const CDList<Expr>& allterms,
653  size_t tBegin);
654 
655  bool hasGoodSynInstNewTrig(Trigger& trig,
656  const std::vector<Expr> & boundVars,
657  std::vector<std::vector<Expr> >& instBinds,
658  std::vector<Expr>& instGterms,
659  const CDList<Expr>& allterms,
660  size_t tBegin);
661 
662 
663  bool hasGoodSynMultiInst(const Expr& e,
664  std::vector<Expr>& bVars,
665  std::vector<std::vector<Expr> >& instSet,
666  const CDList<Expr>& allterms,
667  size_t tBegin);
668 
669  void recGoodSemMatch(const Expr& e,
670  const std::vector<Expr>& bVars,
671  std::vector<Expr>& newInst,
672  std::set<std::vector<Expr> >& instSet);
673 
674  bool hasGoodSemInst(const Expr& e,
675  std::vector<Expr>& bVars,
676  std::set<std::vector<Expr> >& instSet,
677  size_t tBegin);
678 
679  bool isTransLike (const std::vector<Expr>& cur_trig);
680  bool isTrans2Like (const std::vector<Expr>& all_terms, const Expr& tr2);
681 
682 
683  static const size_t MAX_TRIG_BVS=15;
685 
686  Expr recGeneralTrig(const Expr& trig, ExprMap<Expr>& bvs, size_t& mybvs_count);
687  Expr generalTrig(const Expr& trig, ExprMap<Expr>& bvs);
688 
690 
692 
693  void registerTrig(ExprMap<ExprMap<std::vector<dynTrig>* >* >& cur_trig_map,
694  Trigger trig,
695  const std::vector<Expr> thmBVs,
696  size_t univ_id);
697 
698  void registerTrigReal(Trigger trig, const std::vector<Expr>, size_t univ_id);
699 
700  bool canMatch(const Expr& t1, const Expr& t2, ExprMap<Expr>& env);
701  void setGround(const Expr& gterm, const Expr& trig, const Theorem& univ, const std::vector<Expr>& subTerms) ;
702 
703  // std::string getHead(const Expr& e) ;
704  void setupTriggers(ExprMap<ExprMap<std::vector<dynTrig>* >*>& trig_maps,
705  const Theorem& thm,
706  size_t univs_id);
707 
708  void saveContext();
709 
710 
711  /*! \brief categorizes all the terms contained in an expressions by
712  *type.
713  *
714  * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
715  * returns true if the expression does not contain bound variables, false
716  * otherwise.
717  */
718 
719 
720  public:
721  TheoryQuant(TheoryCore* core); //!< Constructor
722  ~TheoryQuant(); //! Destructor
723 
725 
726 
727 
728  void addSharedTerm(const Expr& e) {} //!< Theory interface
729 
730  /*! \brief Theory interface function to assert quantified formulas
731  *
732  * pushes in negations and converts to either universally or existentially
733  * quantified theorems. Universals are stored in a database while
734  * existentials are enqueued to be handled by the search engine.
735  */
736  void assertFact(const Theorem& e);
737 
738 
739  /* \brief Checks the satisfiability of the universal theorems stored in a
740  * databse by instantiating them.
741  *
742  * There are two algorithms that the checkSat function uses to find
743  * instnatiations. The first algortihm looks for instanitations in a saved
744  * database of previous instantiations that worked in proving an earlier
745  * theorem unsatifiable. All of the class variables with the word saved in
746  * them are for the use of this algorithm. The other algorithm uses terms
747  * found in the assertions that exist in the particular context when
748  * checkSat is called. All of the class variables with the word context in
749  * them are used for the second algorithm.
750  */
751  void checkSat(bool fullEffort);
752  void setup(const Expr& e);
753 
754  int help(int i);
755 
756  void update(const Theorem& e, const Expr& d);
757  /*!\brief Used to notify the quantifier algorithm of possible
758  * instantiations that were used in proving a context inconsistent.
759  */
760  void debug(int i);
761  void notifyInconsistent(const Theorem& thm);
762  //! computes the type of a quantified term. Always a boolean.
763  void computeType(const Expr& e);
764  Expr computeTCC(const Expr& e);
765 
766  virtual Expr parseExprOp(const Expr& e);
767 
768  ExprStream& print(ExprStream& os, const Expr& e);
769  };
770 
771 }
772 
773 #endif
ExprMap< bool > d_hasMoreBVs
Definition: theory_quant.h:401
ExprMap< std::set< std::vector< Expr > > > d_instHistoryGlobal
Definition: theory_quant.h:530
std::string exprMap2string(const ExprMap< Expr > &vec)
std::queue< Theorem > d_univsQueue
universally quantified formulas to be instantiated, the var bindings is in d_bingQueue and the ground...
Definition: theory_quant.h:210
CDO< int > d_instCount
number of instantiations made in given context
Definition: theory_quant.h:261
std::vector< std::vector< size_t > > var_pos
Definition: theory_quant.h:408
Trigger trig
Definition: theory_quant.h:90
void collectChangedTerms(CDList< Expr > &changed_terms)
void newTopMatchNoSig(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
bool synMatchTopPred(const Expr &gterm, const Trigger trig, ExprMap< Expr > &env)
Data structure of expressions in CVC3.
Definition: expr.h:133
ExprMap< CDMap< Expr, bool > * > d_bindHistory
Definition: theory_quant.h:525
typeMap d_savedMap
a map of types to positions in the d_savedTerms vector
Definition: theory_quant.h:276
QuantProofRules * d_quant_rules
Definition: theory_quant.h:100
void recGoodSemMatch(const Expr &e, const std::vector< Expr > &bVars, std::vector< Expr > &newInst, std::set< std::vector< Expr > > &instSet)
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
~TheoryQuant()
Destructor.
QuantProofRules * d_rules
quantifier theorem production rules
Definition: theory_quant.h:285
std::map< ExprIndex, Expr > d_indexExpr
Definition: theory_quant.h:394
Expr getHeadExpr(const Expr &e)
void matchListNew(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs, const CDList< Expr > &list, size_t gbegin, size_t gend)
CDList< Expr > d_eqs
Definition: theory_quant.h:471
StatCounter d_totalInstCount
Definition: theory_quant.h:502
void collect_shield_index(const Expr &e)
void pushBackList(const Expr &node, Expr ex)
const bool * d_useManTrig
Definition: theory_quant.h:346
const bool * d_useInstLCache
Definition: theory_quant.h:334
dynTrig(Trigger t, ExprMap< Expr > b, size_t id)
ExprMap< std::hash_map< Expr, bool > * > d_bindGlobalHistory
Definition: theory_quant.h:526
CompleteInstPreProcessor(TheoryCore *, QuantProofRules *)
TheoryQuant(TheoryCore *core)
categorizes all the terms contained in an expressions by type.
const bool * d_useExprScore
Definition: theory_quant.h:339
Expr recInstMacros(const Expr &assert)
void synMultInst(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)
void combineOldNewTrigs(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs)
void newTopMatchSig(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
ExprMap< CDList< Expr > * > d_eq_list
Definition: theory_quant.h:466
bool hasGoodSemInst(const Expr &e, std::vector< Expr > &bVars, std::set< std::vector< Expr > > &instSet, size_t tBegin)
CDList< Expr > & backList(const Expr &ex)
Expr instMacros(const Expr &, const Expr)
substitute a macro in assert
CDO< bool > d_partCalled
Definition: theory_quant.h:236
Trigger(TheoryCore *core, Expr e, Polarity pol, std::set< Expr >)
bool operator()(const Type t1, const Type t2) const
< needed for typeMap
Definition: theory_quant.h:194
CDO< size_t > d_univsContextPos
tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed wh...
Definition: theory_quant.h:258
std::string exprMap2stringSig(const ExprMap< Expr > &vec)
const bool * d_useEqu
Definition: theory_quant.h:351
std::vector< Expr > d_allInsts
Definition: theory_quant.h:367
void synFullInst(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)
struct CVC3::dynTrig dynTrig
void matchListOld(const CDList< Expr > &list, size_t gbegin, size_t gend)
void collectIndex(const Expr &e)
collect index for instantiation
Expr recSkolemize(const Expr &, ExprMap< Polarity > &)
CDList< Expr > null_cdlist
Definition: theory_quant.h:455
ExprMap< CDList< Expr > * > d_parent_list
Definition: theory_quant.h:476
CDList< Expr > & forwList(const Expr &ex)
CDO< size_t > d_lastPartPredsPos
tracks the positions of preds for partial instantiation
Definition: theory_quant.h:227
const bool * d_usePolarity
Definition: theory_quant.h:350
size_t univ_id
Definition: theory_quant.h:91
CDO< size_t > d_savedTermsPos
tracks a possition in the savedTerms map
Definition: theory_quant.h:250
CDO< int > d_curMaxExprScore
Definition: theory_quant.h:357
std::map< Type, CDList< size_t > *,TypeComp > d_contextMap
a map of types to posisitions in the d_contextTerms list
Definition: theory_quant.h:269
void collect_forall_index(const Expr &forall_quant)
Expr recRewriteNot(const Expr &, ExprMap< Polarity > &)
ExprMap< CDList< std::vector< Expr > > * > d_mtrigs_inst
Definition: theory_quant.h:463
const int * d_useTrigLoop
Definition: theory_quant.h:340
MS C++ specific settings.
Definition: type.h:42
void debug(int i)
Used to notify the quantifier algorithm of possible instantiations that were used in proving a contex...
Base class for theories.
Definition: theory.h:64
void add_parent(const Expr &parent)
ExprMap< CDList< Expr > * > d_trans_forw
Definition: theory_quant.h:421
Expr computeTCC(const Expr &e)
void naiveCheckSat(bool)
void semInst(const Theorem &univ, size_t tBegin)
const bool * d_useSemMatch
use lazy instantiation
Definition: theory_quant.h:327
void synPartInst(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)
ExprMap< std::vector< Trigger > > d_multTrigs
Definition: theory_quant.h:386
const bool * d_useGFact
Definition: theory_quant.h:347
bool recMultMatchNewWay(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
ExprMap< std::vector< Expr > > d_insts
a map of instantiated universals to a vector of their instantiations
Definition: theory_quant.h:282
const bool * d_useTrans
Definition: theory_quant.h:344
std::string exprMap2stringSimplify(const ExprMap< Expr > &vec)
const bool * d_useInstTrue
Definition: theory_quant.h:337
bool isSuperSimple
Definition: theory_quant.h:61
void assertFact(const Theorem &e)
Theory interface function to assert quantified formulas.
std::vector< std::vector< size_t > > common_pos
Definition: theory_quant.h:407
Description: Counters and flags for collecting run-time statistics.
CDList< Theorem > d_rawUnivs
Definition: theory_quant.h:204
std::vector< CDMap< Expr, bool > * > var_binds_found
Definition: theory_quant.h:410
void simplifyVectorExprMap(std::vector< ExprMap< Expr > > &orgVectorExprMap)
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
const bool * d_useInstAll
Definition: theory_quant.h:349
bool multMatchChild(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, bool top=false)
void addIndex(const Expr &e)
insert an index
void setTrans2Found(const Expr &comb)
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
ExprMap< Expr > binds
Definition: theory_quant.h:92
CDMap< Expr, std::set< std::vector< Expr > > > d_instHistory
Definition: theory_quant.h:519
const bool * d_useNewEqu
Definition: theory_quant.h:352
CDList< dynTrig > d_arrayTrigs
Definition: theory_quant.h:206
Expr d_mybvs[MAX_TRIG_BVS]
Definition: theory_quant.h:684
ExprMap< Polarity > d_expr_pol
Definition: theory_quant.h:104
ExprMap< std::hash_map< Expr, Theorem > * > d_bindGlobalThmHistory
Definition: theory_quant.h:528
void setTrans(bool b)
const bool * d_translate
Try complete instantiation.
Definition: theory_quant.h:329
void recSearchCover(const std::vector< Expr > &border, const std::vector< Expr > &mtrigs, int cur_depth, std::vector< std::vector< Expr > > &instSet, std::vector< Expr > &cur_inst)
ExprMap< CDO< size_t > * > d_eq_pos
Definition: theory_quant.h:474
std::queue< Theorem > d_simplifiedThmQueue
Definition: theory_quant.h:212
void setTrans2(bool b)
std::vector< ExprMap< CDList< Expr > * > * > uncomm_list
Definition: theory_quant.h:412
void recInstantiate(Theorem &univ, bool all, bool savedMap, size_t newIndex, std::vector< Expr > &varReplacements)
does most of the work of the instantiate function.
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
StatCounter d_allInstCount
Definition: theory_quant.h:500
CDO< size_t > d_lastUsefulGtermsPos
tracks the position in d_usefulGterms
Definition: theory_quant.h:247
CDO< size_t > d_lastArrayPos
Definition: theory_quant.h:207
const Expr & getExpr() const
Definition: type.h:52
std::vector< Expr > getBVs()
std::map< Type, std::vector< Expr >, TypeComp > d_typeExprMap
Definition: theory_quant.h:497
CDO< size_t > d_univsSavedPos
tracks a possition in the database of universals
Definition: theory_quant.h:252
CDO< size_t > d_rawUnivsSavedPos
Definition: theory_quant.h:253
void registerTrig(ExprMap< ExprMap< std::vector< dynTrig > * > * > &cur_trig_map, Trigger trig, const std::vector< Expr > thmBVs, size_t univ_id)
const bool * d_useLazyInst
use new way of instantiation
Definition: theory_quant.h:326
CDList< Theorem > d_univs
database of universally quantified theorems
Definition: theory_quant.h:202
std::vector< Expr > d_savedTerms
a vector of all of the terms that have produced conflicts.
Definition: theory_quant.h:279
Expr simplifyEq(const Expr &)
simplify a=a to True
const int * d_maxInst
Definition: theory_quant.h:341
Expr generalTrig(const Expr &trig, ExprMap< Expr > &bvs)
int getExprScore(const Expr &e)
ExprMap< CDList< Expr > * > d_trans_back
Definition: theory_quant.h:420
const bool * d_useCompleteInst
use semantic matching
Definition: theory_quant.h:328
void setGround(const Expr &gterm, const Expr &trig, const Theorem &univ, const std::vector< Expr > &subTerms)
bool canMatch(const Expr &t1, const Expr &t2, ExprMap< Expr > &env)
Expr minusOne(const Expr &e)
return e-1
const bool * d_useTrans2
Definition: theory_quant.h:345
const bool * d_useInstGCache
Definition: theory_quant.h:335
bool recSynMatch(const Expr &gterm, const Expr &vterm, ExprMap< Expr > &env)
int loc_gterm(const std::vector< Expr > &border, const Expr &gterm, int pos)
void goodSynMatch(const Expr &e, const std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBindsTerm, std::vector< Expr > &instGterm, const CDList< Expr > &allterms, size_t tBegin)
ExprMap< std::set< std::vector< Expr > > > d_tempBinds
Definition: theory_quant.h:219
Expr simplifyQuant(const Expr &)
put all quants in postive form and then skolemize all exists
Expr inst(const Expr &e)
inst forall quant using index from collectIndex
std::map< Type, std::vector< size_t >, TypeComp > typeMap
used to facilitate instantiation of universal quantifiers
Definition: theory_quant.h:199
void notifyInconsistent(const Theorem &thm)
Used to notify the quantifier algorithm of possible instantiations that were used in proving a contex...
void addSharedTerm(const Expr &e)
Theory interface.
Definition: theory_quant.h:728
size_t multiIndex
Definition: theory_quant.h:63
bool isMacro(const Expr &assert)
if assert is a macro definition
void collectHeads(const Expr &assert, std::set< Expr > &heads)
std::vector< Expr > bvs
Definition: theory_quant.h:55
std::queue< Expr > d_gBindQueue
Definition: theory_quant.h:216
void newTopMatch(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
void synCheckSat(ExprMap< ExprMap< std::vector< dynTrig > * > * > &, bool)
void arrayHeuristic(const Trigger &trig, size_t univid)
int d_initMaxScore
all instantiations
Definition: theory_quant.h:369
std::vector< Expr > d_gnd_cache
Definition: theory_quant.h:108
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
void semCheckSat(bool)
ExprMap< CDList< Expr > * > d_same_head_expr
Definition: theory_quant.h:465
CDMap< Expr, bool > d_trans_found
Definition: theory_quant.h:422
ExprMap< Expr > d_quant_equiv_map
Definition: theory_quant.h:106
static const size_t MAX_TRIG_BVS
Definition: theory_quant.h:683
const bool * d_useInstThmCache
Definition: theory_quant.h:336
const int * d_gfactLimit
Definition: theory_quant.h:348
Theorem theoryPreprocess(const Expr &e)
Theory-specific preprocessing.
static int parent(int i)
Definition: minisat_heap.h:55
CDMap< Expr, bool > d_trans2_found
Definition: theory_quant.h:423
void enqueueInst(const Theorem, const Theorem)
void registerTrigReal(Trigger trig, const std::vector< Expr >, size_t univ_id)
void computeType(const Expr &e)
computes the type of a quantified term. Always a boolean.
bool hasShieldVar(const Expr &e)
CDList< Trigger > d_alltrig_list
Definition: theory_quant.h:691
CDO< size_t > d_univsPartSavedPos
tracks a possition in the database of universals for partial instantiation
Definition: theory_quant.h:231
int d_inEnd
set if the fullEffort = 1
Definition: theory_quant.h:264
bool hasGoodSynInstNewTrigOld(Trigger &trig, std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const CDList< Expr > &allterms, size_t tBegin)
std::map< ExprIndex, int > d_indexScore
Definition: theory_quant.h:392
StatCounter d_trueInstCount
Definition: theory_quant.h:503
void iterBKList(const Expr &sr, const Expr &dt, size_t univ_id, const Expr &gterm)
bool hasMacros(const std::vector< Expr > &asserts)
if there are macros
ExprMap< std::vector< Expr > > d_mtrigs_bvorder
Definition: theory_quant.h:478
bool hasGoodSynMultiInst(const Expr &e, std::vector< Expr > &bVars, std::vector< std::vector< Expr > > &instSet, const CDList< Expr > &allterms, size_t tBegin)
bool recMultMatchDebug(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
CDList< Expr > d_contextTerms
a list of all the terms appearing in the current context
Definition: theory_quant.h:271
ExprMap< size_t > d_totalThmCount
Definition: theory_quant.h:523
bool hasGoodSynInstNewTrig(Trigger &trig, const std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const CDList< Expr > &allterms, size_t tBegin)
const std::vector< Expr > & getSubTerms(const Expr &e)
void newTopMatchBackupOnly(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
Expr simpRAWList(const Expr &org)
CDO< size_t > d_lastPartTermsPos
tracks the possition of terms for partial instantiation
Definition: theory_quant.h:229
std::set< std::string > cacheHead
Definition: theory_quant.h:498
bool transFound(const Expr &comb)
void mapTermsByType(const CDList< Expr > &terms)
categorizes all the terms contained in a vector of expressions by type.
CDMap< Expr, std::vector< Expr > > d_arrayIndic
Definition: theory_quant.h:364
Expr getHead(const Expr &e)
std::vector< multTrigsInfo > d_all_multTrigsInfo
Definition: theory_quant.h:418
bool isGood(const Expr &e)
if e is a formula in the array property fragment
bool multMatchTop(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
void setRWOp(bool b)
void pushForwList(const Expr &node, Expr ex)
CDList< Theorem > d_eqsUpdate
Definition: theory_quant.h:468
ExprMap< bool > d_hasTriggers
the score for a full trigger
Definition: theory_quant.h:400
Generic API for Theories plus methods commonly used by theories.
StatCounter d_abInstCount
Definition: theory_quant.h:504
bool isShield(const Expr &e)
if e satisfies the shiled property, that is all bound vars are parameters of uninterpreted functions/...
const int * d_maxQuantInst
Command line option.
Definition: theory_quant.h:287
void iterFWList(const Expr &sr, const Expr &dt, size_t univ_id, const Expr &gterm)
bool d_all_good
if all formulas checked so far are good
Definition: theory_quant.h:119
CDO< size_t > d_lastEqsUpdatePos
Definition: theory_quant.h:469
CDO< bool > d_maxILReached
the max instantiation level reached
Definition: theory_quant.h:239
void simplifyExprMap(ExprMap< Expr > &orgExprMap)
void delNewTrigs(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs)
const bool * d_usePart
translate only
Definition: theory_quant.h:331
void findInstAssumptions(const Theorem &thm)
A recursive function used to find instantiated universals in the hierarchy of assumptions.
CDO< size_t > d_eqs_pos
Definition: theory_quant.h:472
const int * d_maxIL
Definition: theory_quant.h:343
const bool * d_usePullVar
Definition: theory_quant.h:338
void setupTriggers(ExprMap< ExprMap< std::vector< dynTrig > * > * > &trig_maps, const Theorem &thm, size_t univs_id)
void synInst(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)
void addNotify(const Expr &e)
ExprMap< bool > d_savedCache
Definition: theory_quant.h:277
bool isGoodQuant(const Expr &e)
if e is a quant in the array property fragmenet
void searchCover(const Expr &thm, const std::vector< Expr > &border, std::vector< std::vector< Expr > > &instSet)
CDList< Expr > d_usefulGterms
useful gterms for matching
Definition: theory_quant.h:244
bool recursiveMap(const Expr &term)
categorizes all the terms contained in an expressions by type.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Expr rewriteNot(const Expr &)
rewrite neg polarity forall / exists to pos polarity
QuantProofRules * createProofRules()
Destructor.
CDO< size_t > d_exprLastUpdatedPos
Definition: theory_quant.h:390
void setTransFound(const Expr &comb)
bool trans2Found(const Expr &comb)
const bool * d_useNaiveInst
Definition: theory_quant.h:354
CDO< size_t > d_univsPosFull
tracks a possition in the database of universals
Definition: theory_quant.h:255
Expr plusOne(const Expr &e)
return e+1
Polarity polarity
Definition: theory_quant.h:53
CDMap< Expr, bool > d_contextCache
Definition: theory_quant.h:273
bool isTransLike(const std::vector< Expr > &cur_trig)
CDO< size_t > d_lastPartLevel
the last decision level on which partial instantion is called
Definition: theory_quant.h:234
void synNewInst(size_t univ_id, const std::vector< Expr > &binds, const Expr &gterm, const Trigger &trig)
Definition: expr.cpp:35
const int * d_maxNaiveCall
Definition: theory_quant.h:353
bool isTrans2Like(const std::vector< Expr > &all_terms, const Expr &tr2)
ExprMap< std::vector< Expr > > d_partTriggers
Definition: theory_quant.h:382
Expr recGeneralTrig(const Expr &trig, ExprMap< Expr > &bvs, size_t &mybvs_count)
bool recMultMatch(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
ExprMap< std::vector< Expr > > d_subTermsMap
Definition: theory_quant.h:533
StatCounter d_allInstCount2
Definition: theory_quant.h:501
const bool * d_useMult
use partial instantiaion
Definition: theory_quant.h:332
void setHead(Expr h)
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
bool recMultMatchOldWay(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
CDO< size_t > d_lastTermsPos
tracks the possition of terms
Definition: theory_quant.h:224
ExprMap< CDMap< Expr, CDList< dynTrig > * > * > d_allmap_trigs
Definition: theory_quant.h:689
const bool * d_useNew
Definition: theory_quant.h:325
std::queue< Theorem > d_gUnivQueue
Definition: theory_quant.h:214
void instantiate(Theorem univ, bool all, bool savedMap, size_t newIndex)
Queues up all possible instantiations of bound variables.
bool recSynMatchBackupOnly(const Expr &gterm, const Expr &vterm, ExprMap< Expr > &env)
ExprMap< std::vector< Trigger > > d_partTrigs
Definition: theory_quant.h:387
void arrayIndexName(const Expr &e)
CDO< size_t > d_lastPredsPos
tracks the possition of preds
Definition: theory_quant.h:222
std::vector< Theorem > d_cacheTheorem
Definition: theory_quant.h:512
This theory handles quantifiers.
Definition: theory_quant.h:186
void goodSynMatchNewTrig(const Trigger &trig, const std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const CDList< Expr > &allterms, size_t tBegin)
ExprMap< int > d_thmCount
Definition: theory_quant.h:522
size_t multiId
Definition: theory_quant.h:64
bool insted(const Theorem &univ, const std::vector< Expr > &binds)
ExprMap< multTrigsInfo > d_multitrigs_maps
Definition: theory_quant.h:417
ExprMap< std::vector< Trigger > > d_fullTrigs
Definition: theory_quant.h:384
ExprMap< std::vector< Expr > > d_multTriggers
Definition: theory_quant.h:381
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.