CVC3
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
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