00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #ifndef _cvc3__expr_h_
00023 #define _cvc3__expr_h_
00024
00025 #include <stdlib.h>
00026 #include <sstream>
00027 #include <set>
00028 #include <functional>
00029 #include <iterator>
00030 #include <map>
00031
00032 #include "os.h"
00033 #include "compat_hash_map.h"
00034 #include "compat_hash_set.h"
00035 #include "rational.h"
00036 #include "kinds.h"
00037 #include "cdo.h"
00038 #include "cdflags.h"
00039 #include "lang.h"
00040 #include "memory_manager.h"
00041
00042 class CInterface;
00043
00044 namespace CVC3 {
00045
00046 class NotifyList;
00047 class Theory;
00048 class Op;
00049 class Type;
00050 class Theorem;
00051
00052 template<class Data>
00053 class ExprHashMap;
00054
00055 class ExprManager;
00056
00057 class ExprValue;
00058 class ExprNode;
00059
00060 class ExprStream;
00061
00062
00063
00064
00065 typedef enum {
00066 EXPR_VALUE,
00067 EXPR_NODE,
00068 EXPR_APPLY,
00069 EXPR_STRING,
00070 EXPR_RATIONAL,
00071 EXPR_SKOLEM,
00072 EXPR_UCONST,
00073 EXPR_SYMBOL,
00074 EXPR_BOUND_VAR,
00075 EXPR_CLOSURE,
00076 EXPR_VALUE_TYPE_LAST
00077 } ExprValueType;
00078
00079
00080 typedef enum {
00081 CARD_FINITE,
00082 CARD_INFINITE,
00083 CARD_UNKNOWN
00084 } Cardinality;
00085
00086
00087 typedef long unsigned ExprIndex;
00088
00089
00090
00091
00092
00093
00094
00095
00096
00097
00098
00099
00100
00101
00102
00103
00104
00105
00106
00107
00108
00109
00110
00111
00112
00113
00114
00115
00116
00117
00118
00119
00120
00121
00122
00123
00124
00125
00126
00127
00128
00129
00130
00131
00132
00133 class CVC_DLL Expr {
00134 friend class ExprHasher;
00135 friend class ExprManager;
00136 friend class Op;
00137 friend class ExprValue;
00138 friend class ExprNode;
00139 friend class ExprClosure;
00140 friend class ::CInterface;
00141 friend class Theorem;
00142
00143
00144
00145
00146
00147 typedef enum {
00148
00149 VALID_TYPE = 0x1,
00150
00151 VALID_IS_ATOMIC = 0x2,
00152
00153 IS_ATOMIC = 0x4,
00154
00155 REWRITE_NORMAL = 0x8,
00156
00157 IS_FINITE = 0x400,
00158
00159 WELL_FOUNDED = 0x800,
00160
00161 COMPUTE_TRANS_CLOSURE = 0x1000,
00162
00163 CONTAINS_BOUND_VAR = 0x00020000,
00164
00165 USES_CC = 0x00080000,
00166
00167 VALID_TERMINALS_CONST = 0x00100000,
00168
00169 TERMINALS_CONST = 0x00200000
00170 } StaticFlagsEnum;
00171
00172
00173
00174 typedef enum {
00175
00176 IMPLIED_LITERAL = 0x10,
00177 IS_USER_ASSUMPTION = 0x20,
00178 IS_INT_ASSUMPTION = 0x40,
00179 IS_JUSTIFIED = 0x80,
00180 IS_TRANSLATED = 0x100,
00181 IS_USER_REGISTERED_ATOM = 0x200,
00182 IS_SELECTED = 0x2000,
00183 IS_STORED_PREDICATE = 0x4000,
00184 IS_REGISTERED_ATOM = 0x8000,
00185 IN_USER_ASSUMPTION = 0x00010000,
00186
00187 NOT_ARRAY_NORMALIZED = 0x00040000
00188 } DynamicFlagsEnum;
00189
00190
00191 static Expr s_null;
00192
00193
00194
00195
00196
00197 ExprValue* d_expr;
00198
00199
00200
00201
00202
00203
00204 Expr(ExprValue* expr);
00205
00206 Expr recursiveSubst(const ExprHashMap<Expr>& subst,
00207 ExprHashMap<Expr>& visited) const;
00208
00209 Expr recursiveQuantSubst(ExprHashMap<Expr>& subst,
00210 ExprHashMap<Expr>& visited) const;
00211 public:
00212
00213
00214
00215
00216
00217
00218
00219
00220
00221
00222
00223
00224
00225
00226 class CVC_DLL iterator
00227 : public std::iterator<std::input_iterator_tag,Expr,ptrdiff_t>
00228 {
00229 friend class Expr;
00230 private:
00231 std::vector<Expr>::const_iterator d_it;
00232
00233
00234
00235 iterator(std::vector<Expr>::const_iterator it): d_it(it) { }
00236
00237 public:
00238
00239 iterator() { }
00240
00241
00242
00243 bool operator==(const iterator& i) const {
00244 return d_it == i.d_it;
00245 }
00246
00247 bool operator!=(const iterator& i) const { return !(*this == i); }
00248
00249 const Expr& operator*() const { return *d_it; }
00250
00251 const Expr* operator->() const { return &(operator*()); }
00252
00253 iterator& operator++() {
00254 d_it++;
00255 return *this;
00256 }
00257
00258
00259 class Proxy {
00260 const Expr* d_e;
00261 public:
00262 Proxy(const Expr& e) : d_e(&e) { }
00263 Expr operator*() { return *d_e; }
00264 };
00265
00266
00267
00268
00269
00270
00271
00272 Proxy operator++(int) {
00273 Proxy e(*(*this));
00274 ++(*this);
00275 return e;
00276 }
00277 };
00278
00279
00280
00281
00282
00283
00284 Expr(): d_expr(NULL) {}
00285
00286
00287
00288 Expr(const Expr& e);
00289
00290 Expr& operator=(const Expr& e);
00291
00292
00293
00294
00295 Expr(const Op& op, const Expr& child);
00296 Expr(const Op& op, const Expr& child0, const Expr& child1);
00297 Expr(const Op& op, const Expr& child0, const Expr& child1,
00298 const Expr& child2);
00299 Expr(const Op& op, const Expr& child0, const Expr& child1,
00300 const Expr& child2, const Expr& child3);
00301 Expr(const Op& op, const std::vector<Expr>& children,
00302 ExprManager* em = NULL);
00303
00304
00305 ~Expr();
00306
00307
00308 Expr eqExpr(const Expr& right) const;
00309 Expr notExpr() const;
00310 Expr negate() const;
00311 Expr andExpr(const Expr& right) const;
00312 Expr orExpr(const Expr& right) const;
00313 Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
00314 Expr iffExpr(const Expr& right) const;
00315 Expr impExpr(const Expr& right) const;
00316 Expr xorExpr(const Expr& right) const;
00317
00318 Expr skolemExpr(int i) const;
00319
00320
00321
00322 Expr rebuild(ExprManager* em) const;
00323
00324
00325 Expr substExpr(const std::vector<Expr>& oldTerms,
00326 const std::vector<Expr>& newTerms) const;
00327 Expr substExpr(const ExprHashMap<Expr>& oldToNew) const;
00328
00329
00330 Expr substExprQuant(const std::vector<Expr>& oldTerms,
00331 const std::vector<Expr>& newTerms) const;
00332
00333
00334 Expr operator!() const { return notExpr(); }
00335 Expr operator&&(const Expr& right) const { return andExpr(right); }
00336 Expr operator||(const Expr& right) const { return orExpr(right); }
00337
00338
00339
00340
00341
00342 static size_t hash(const Expr& e);
00343
00344
00345
00346
00347
00348 size_t hash() const;
00349
00350
00351
00352 bool isFalse() const { return getKind() == FALSE_EXPR; }
00353 bool isTrue() const { return getKind() == TRUE_EXPR; }
00354 bool isBoolConst() const { return isFalse() || isTrue(); }
00355 bool isVar() const;
00356 bool isBoundVar() const { return getKind() == BOUND_VAR; }
00357 bool isString() const;
00358 bool isClosure() const;
00359 bool isQuantifier() const;
00360 bool isLambda() const;
00361 bool isApply() const;
00362 bool isSymbol() const;
00363 bool isTheorem() const;
00364
00365 bool isConstant() const { return getOpKind() <= MAX_CONST; }
00366
00367 bool isRawList() const {return getKind() == RAW_LIST;}
00368
00369
00370 bool isType() const;
00371
00372
00373
00374
00375
00376
00377
00378
00379 const ExprValue* getExprValue() const;
00380
00381
00382 bool isTerm() const;
00383
00384
00385
00386
00387 bool isAtomic() const;
00388
00389
00390
00391
00392
00393 bool isAtomicFormula() const;
00394
00395 bool isAbsAtomicFormula() const
00396 { return isQuantifier() || isAtomicFormula(); }
00397
00398
00399
00400 bool isLiteral() const
00401 { return (isAtomicFormula() || (isNot() && (*this)[0].isAtomicFormula())); }
00402
00403 bool isAbsLiteral() const
00404 { return (isAbsAtomicFormula() || (isNot() && (*this)[0].isAbsAtomicFormula())); }
00405
00406 bool isBoolConnective() const;
00407
00408 bool isPropAtom() const { return !isTerm() && !isBoolConnective(); }
00409
00410 bool isPropLiteral() const
00411 { return (isNot() && (*this)[0].isPropAtom()) || isPropAtom(); }
00412
00413 bool containsTermITE() const;
00414
00415
00416 bool isEq() const { return getKind() == EQ; }
00417 bool isNot() const { return getKind() == NOT; }
00418 bool isAnd() const { return getKind() == AND; }
00419 bool isOr() const { return getKind() == OR; }
00420 bool isITE() const { return getKind() == ITE; }
00421 bool isIff() const { return getKind() == IFF; }
00422 bool isImpl() const { return getKind() == IMPLIES; }
00423 bool isXor() const { return getKind() == XOR;}
00424
00425 bool isForall() const { return getKind() == FORALL; }
00426 bool isExists() const { return getKind() == EXISTS; }
00427
00428 bool isRational() const { return getKind() == RATIONAL_EXPR; }
00429 bool isSkolem() const { return getKind() == SKOLEM_VAR;}
00430
00431
00432
00433
00434
00435 const std::string& getName() const;
00436
00437 const std::string& getUid() const;
00438
00439
00440 const std::string& getString() const;
00441
00442 const std::vector<Expr>& getVars() const;
00443
00444 const Expr& getExistential() const;
00445
00446 int getBoundIndex() const;
00447
00448
00449 const Expr& getBody() const;
00450
00451
00452 void setTriggers(const std::vector<std::vector<Expr> >& triggers) const;
00453
00454
00455 const std::vector<std::vector<Expr> >& getTrigs() const;
00456
00457
00458 const Rational& getRational() const;
00459
00460 const Theorem& getTheorem() const;
00461
00462
00463 ExprManager *getEM() const;
00464
00465
00466 const std::vector<Expr>& getKids() const;
00467
00468
00469 int getKind() const;
00470
00471
00472 ExprIndex getIndex() const;
00473
00474
00475 bool hasLastIndex() const;
00476
00477
00478 Op mkOp() const;
00479
00480
00481 Op getOp() const;
00482
00483
00484 Expr getOpExpr() const;
00485
00486
00487 int getOpKind() const;
00488
00489
00490
00491
00492
00493 int arity() const;
00494
00495
00496
00497 const Expr& operator[](int i) const;
00498
00499
00500 const Expr& unnegate() const { return isNot() ? (*this)[0] : *this; }
00501
00502
00503 iterator begin() const;
00504
00505
00506 iterator end() const;
00507
00508
00509 bool isNull() const;
00510
00511
00512 bool isInitialized() const { return d_expr != NULL; }
00513
00514 size_t getMMIndex() const;
00515
00516
00517
00518
00519 bool hasFind() const;
00520
00521
00522
00523
00524 const Theorem& getFind() const;
00525 int getFindLevel() const;
00526 const Theorem& getEqNext() const;
00527
00528
00529 NotifyList* getNotify() const;
00530
00531
00532 Type getType() const;
00533
00534 Type lookupType() const;
00535
00536 Cardinality typeCard() const;
00537
00538
00539
00540 Expr typeEnumerateFinite(Unsigned n) const;
00541
00542 Unsigned typeSizeFinite() const;
00543
00544
00545
00546 bool validSimpCache() const;
00547
00548
00549 const Theorem& getSimpCache() const;
00550
00551
00552 bool isValidType() const;
00553
00554
00555 bool validIsAtomicFlag() const;
00556
00557
00558 bool validTerminalsConstFlag() const;
00559
00560
00561 bool getIsAtomicFlag() const;
00562
00563
00564 bool getTerminalsConstFlag() const;
00565
00566
00567 bool isRewriteNormal() const;
00568
00569
00570 bool isFinite() const;
00571
00572
00573 bool isWellFounded() const;
00574
00575
00576 bool computeTransClosure() const;
00577
00578
00579 bool containsBoundVar() const;
00580
00581
00582 bool usesCC() const;
00583
00584
00585 bool notArrayNormalized() const;
00586
00587
00588 bool isImpliedLiteral() const;
00589
00590
00591 bool isUserAssumption() const;
00592
00593
00594 bool inUserAssumption() const;
00595
00596
00597 bool isIntAssumption() const;
00598
00599
00600 bool isJustified() const;
00601
00602
00603 bool isTranslated() const;
00604
00605
00606 bool isUserRegisteredAtom() const;
00607
00608
00609 bool isRegisteredAtom() const;
00610
00611
00612 bool isSelected() const;
00613
00614
00615 bool isStoredPredicate() const;
00616
00617
00618 bool getFlag() const;
00619
00620 void setFlag() const;
00621
00622 void clearFlags() const;
00623
00624
00625
00626
00627 std::string toString() const;
00628
00629 std::string toString(InputLanguage lang) const;
00630
00631 void print(InputLanguage lang, bool dagify = true) const;
00632
00633
00634 void print() const { print(AST_LANG); }
00635
00636 void printnodag() const;
00637
00638
00639 void pprint() const;
00640
00641 void pprintnodag() const;
00642
00643
00644
00645
00646
00647 ExprStream& print(ExprStream& os) const;
00648
00649
00650
00651 ExprStream& printAST(ExprStream& os) const;
00652
00653
00654
00655
00656
00657 Expr& indent(int n, bool permanent = false);
00658
00659
00660
00661
00662
00663
00664
00665
00666 void setFind(const Theorem& e) const;
00667
00668
00669 void setEqNext(const Theorem& e) const;
00670
00671
00672 void addToNotify(Theory* i, const Expr& e) const;
00673
00674
00675 void setType(const Type& t) const;
00676
00677
00678 void setSimpCache(const Theorem& e) const;
00679
00680
00681 void setValidType() const;
00682
00683
00684 void setIsAtomicFlag(bool value) const;
00685
00686
00687 void setTerminalsConstFlag(bool value) const;
00688
00689
00690 void setRewriteNormal() const;
00691 void clearRewriteNormal() const;
00692
00693
00694 void setFinite() const;
00695
00696
00697 void setWellFounded() const;
00698
00699
00700 void setComputeTransClosure() const;
00701
00702
00703 void setContainsBoundVar() const;
00704
00705
00706 void setUsesCC() const;
00707
00708
00709 void setNotArrayNormalized() const;
00710
00711
00712 void setImpliedLiteral() const;
00713
00714
00715 void setUserAssumption(int scope = -1) const;
00716
00717
00718 void setInUserAssumption(int scope = -1) const;
00719
00720
00721 void setIntAssumption() const;
00722
00723
00724 void setJustified() const;
00725
00726
00727 void setTranslated(int scope = -1) const;
00728
00729
00730 void setUserRegisteredAtom() const;
00731
00732
00733 void setRegisteredAtom() const;
00734
00735
00736 void setSelected() const;
00737
00738
00739 void setStoredPredicate() const;
00740
00741
00742 bool subExprOf(const Expr& e) const;
00743
00744
00745
00746 inline Unsigned getSize() const;
00747
00748
00749
00750
00751
00752
00753
00754
00755
00756
00757
00758
00759
00760 bool hasSig() const;
00761 bool hasRep() const;
00762 const Theorem& getSig() const;
00763 const Theorem& getRep() const;
00764 void setSig(const Theorem& e) const;
00765 void setRep(const Theorem& e) const;
00766
00767
00768
00769
00770
00771 friend CVC_DLL std::ostream& operator<<(std::ostream& os, const Expr& e);
00772
00773
00774
00775
00776
00777 friend int compare(const Expr& e1, const Expr& e2);
00778
00779 friend bool operator==(const Expr& e1, const Expr& e2);
00780 friend bool operator!=(const Expr& e1, const Expr& e2);
00781
00782 friend bool operator<(const Expr& e1, const Expr& e2);
00783 friend bool operator<=(const Expr& e1, const Expr& e2);
00784 friend bool operator>(const Expr& e1, const Expr& e2);
00785 friend bool operator>=(const Expr& e1, const Expr& e2);
00786
00787
00788
00789 };
00790
00791 }
00792
00793
00794
00795 #ifndef DOXYGEN
00796 #include "expr_op.h"
00797 #include "expr_manager.h"
00798 #endif
00799 namespace CVC3 {
00800
00801 inline Expr::Expr(ExprValue* expr) : d_expr(expr) { d_expr->incRefcount(); }
00802
00803 inline Expr::Expr(const Expr& e) : d_expr(e.d_expr) {
00804 if (d_expr != NULL) d_expr->incRefcount();
00805 }
00806
00807 inline Expr& Expr::operator=(const Expr& e) {
00808 if(&e == this) return *this;
00809 ExprValue* tmp = e.d_expr;
00810 if (tmp == NULL) {
00811 if (d_expr == NULL) {
00812 return *this;
00813 }
00814 d_expr->decRefcount();
00815 }
00816 else {
00817 tmp->incRefcount();
00818 if(d_expr != NULL) {
00819 d_expr->decRefcount();
00820 }
00821 }
00822 d_expr = tmp;
00823 return *this;
00824 }
00825
00826 inline Expr::Expr(const Op& op, const Expr& child) {
00827 ExprManager* em = child.getEM();
00828 if (op.getKind() != APPLY) {
00829 ExprNode ev(em, op.getKind());
00830 std::vector<Expr>& kids = ev.getKids1();
00831 kids.push_back(child);
00832 d_expr = em->newExprValue(&ev);
00833 } else {
00834 ExprApply ev(em, op);
00835 std::vector<Expr>& kids = ev.getKids1();
00836 kids.push_back(child);
00837 d_expr = em->newExprValue(&ev);
00838 }
00839 d_expr->incRefcount();
00840 }
00841
00842 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1) {
00843 ExprManager* em = child0.getEM();
00844 if (op.getKind() != APPLY) {
00845 ExprNode ev(em, op.getKind());
00846 std::vector<Expr>& kids = ev.getKids1();
00847 kids.push_back(child0);
00848 kids.push_back(child1);
00849 d_expr = em->newExprValue(&ev);
00850 } else {
00851 ExprApply ev(em, op);
00852 std::vector<Expr>& kids = ev.getKids1();
00853 kids.push_back(child0);
00854 kids.push_back(child1);
00855 d_expr = em->newExprValue(&ev);
00856 }
00857 d_expr->incRefcount();
00858 }
00859
00860 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1,
00861 const Expr& child2) {
00862 ExprManager* em = child0.getEM();
00863 if (op.getKind() != APPLY) {
00864 ExprNode ev(em, op.getKind());
00865 std::vector<Expr>& kids = ev.getKids1();
00866 kids.push_back(child0);
00867 kids.push_back(child1);
00868 kids.push_back(child2);
00869 d_expr = em->newExprValue(&ev);
00870 } else {
00871 ExprApply ev(em, op);
00872 std::vector<Expr>& kids = ev.getKids1();
00873 kids.push_back(child0);
00874 kids.push_back(child1);
00875 kids.push_back(child2);
00876 d_expr = em->newExprValue(&ev);
00877 }
00878 d_expr->incRefcount();
00879 }
00880
00881 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1,
00882 const Expr& child2, const Expr& child3) {
00883 ExprManager* em = child0.getEM();
00884 if (op.getKind() != APPLY) {
00885 ExprNode ev(em, op.getKind());
00886 std::vector<Expr>& kids = ev.getKids1();
00887 kids.push_back(child0);
00888 kids.push_back(child1);
00889 kids.push_back(child2);
00890 kids.push_back(child3);
00891 d_expr = em->newExprValue(&ev);
00892 } else {
00893 ExprApply ev(em, op);
00894 std::vector<Expr>& kids = ev.getKids1();
00895 kids.push_back(child0);
00896 kids.push_back(child1);
00897 kids.push_back(child2);
00898 kids.push_back(child3);
00899 d_expr = em->newExprValue(&ev);
00900 }
00901 d_expr->incRefcount();
00902 }
00903
00904 inline Expr::Expr(const Op& op, const std::vector<Expr>& children,
00905 ExprManager* em) {
00906 if (em == NULL) {
00907 if (op.getKind() == APPLY) em = op.getExpr().getEM();
00908 else {
00909 DebugAssert(children.size() > 0,
00910 "Expr::Expr(Op, children): op's EM is NULL and "
00911 "no children given");
00912 em = children[0].getEM();
00913 }
00914 }
00915 if (op.getKind() != APPLY) {
00916 ExprNodeTmp ev(em, op.getKind(), children);
00917 d_expr = em->newExprValue(&ev);
00918 } else {
00919 ExprApplyTmp ev(em, op, children);
00920 d_expr = em->newExprValue(&ev);
00921 }
00922 d_expr->incRefcount();
00923 }
00924
00925 inline Expr Expr::eqExpr(const Expr& right) const {
00926 return Expr(EQ, *this, right);
00927 }
00928
00929 inline Expr Expr::notExpr() const {
00930 return Expr(NOT, *this);
00931 }
00932
00933 inline Expr Expr::negate() const {
00934 return isNot() ? (*this)[0] : this->notExpr();
00935 }
00936
00937 inline Expr Expr::andExpr(const Expr& right) const {
00938 return Expr(AND, *this, right);
00939 }
00940
00941 inline Expr andExpr(const std::vector <Expr>& children) {
00942 DebugAssert(children.size()>0 && !children[0].isNull(),
00943 "Expr::andExpr(kids)");
00944 return Expr(AND, children);
00945 }
00946
00947 inline Expr Expr::orExpr(const Expr& right) const {
00948 return Expr(OR, *this, right);
00949 }
00950
00951 inline Expr orExpr(const std::vector <Expr>& children) {
00952 DebugAssert(children.size()>0 && !children[0].isNull(),
00953 "Expr::andExpr(kids)");
00954 return Expr(OR, children);
00955 }
00956
00957 inline Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
00958 return Expr(ITE, *this, thenpart, elsepart);
00959 }
00960
00961 inline Expr Expr::iffExpr(const Expr& right) const {
00962 return Expr(IFF, *this, right);
00963 }
00964
00965 inline Expr Expr::impExpr(const Expr& right) const {
00966 return Expr(IMPLIES, *this, right);
00967 }
00968
00969 inline Expr Expr::xorExpr(const Expr& right) const {
00970 return Expr(XOR, *this, right);
00971 }
00972
00973 inline Expr Expr::skolemExpr(int i) const {
00974 return getEM()->newSkolemExpr(*this, i);
00975 }
00976
00977 inline Expr Expr::rebuild(ExprManager* em) const {
00978 return em->rebuild(*this);
00979 }
00980
00981 inline Expr::~Expr() {
00982 if(d_expr != NULL) {
00983 IF_DEBUG(FatalAssert(d_expr->d_refcount > 0, "Mis-handled the ref. counting");)
00984 if (--(d_expr->d_refcount) == 0) d_expr->d_em->gc(d_expr);
00985 }
00986 }
00987
00988 inline size_t Expr::hash(const Expr& e) { return e.getEM()->hash(e); }
00989
00990
00991
00992
00993
00994 inline size_t Expr::hash() const { return getEM()->hash(*this); }
00995
00996 inline const ExprValue* Expr::getExprValue() const
00997 { return d_expr->getExprValue(); }
00998
00999
01000
01001 inline bool Expr::isVar() const { return d_expr->isVar(); }
01002 inline bool Expr::isString() const { return d_expr->isString(); }
01003 inline bool Expr::isClosure() const { return d_expr->isClosure(); }
01004 inline bool Expr::isQuantifier() const {
01005 return (isClosure() && (getKind() == FORALL || getKind() == EXISTS));
01006 }
01007 inline bool Expr::isLambda() const {
01008 return (isClosure() && getKind() == LAMBDA);
01009 }
01010 inline bool Expr::isApply() const
01011 { DebugAssert((getKind() != APPLY || d_expr->isApply()) &&
01012 (!d_expr->isApply() || getKind() == APPLY), "APPLY mismatch");
01013 return getKind() == APPLY; }
01014 inline bool Expr::isSymbol() const { return d_expr->isSymbol(); }
01015 inline bool Expr::isTheorem() const { return d_expr->isTheorem(); }
01016 inline bool Expr::isType() const { return getEM()->isTypeKind(getOpKind()); }
01017 inline bool Expr::isTerm() const { return !getType().isBool(); }
01018 inline bool Expr::isBoolConnective() const {
01019 if (!getType().isBool()) return false;
01020 switch (getKind()) {
01021 case NOT: case AND: case OR: case IMPLIES: case IFF: case XOR: case ITE:
01022 return true; }
01023 return false;
01024 }
01025
01026 inline Unsigned Expr::getSize() const {
01027 if (d_expr->d_size == 0) {
01028 clearFlags();
01029 const_cast<ExprValue*>(d_expr)->d_size = d_expr->getSize();
01030 }
01031 return d_expr->d_size;
01032 }
01033
01034
01035
01036
01037
01038
01039
01040
01041
01042
01043
01044
01045
01046 inline const std::string& Expr::getName() const {
01047 DebugAssert(!isNull(), "Expr::getName() on Null expr");
01048 return d_expr->getName();
01049 }
01050
01051 inline const std::string& Expr::getString() const {
01052 DebugAssert(isString(),
01053 "CVC3::Expr::getString(): not a string Expr:\n "
01054 + toString(AST_LANG));
01055 return d_expr->getString();
01056 }
01057
01058 inline const std::vector<Expr>& Expr::getVars() const {
01059 DebugAssert(isClosure(),
01060 "CVC3::Expr::getVars(): not a closure Expr:\n "
01061 + toString(AST_LANG));
01062 return d_expr->getVars();
01063 }
01064
01065 inline const Expr& Expr::getBody() const {
01066 DebugAssert(isClosure(),
01067 "CVC3::Expr::getBody(): not a closure Expr:\n "
01068 + toString(AST_LANG));
01069 return d_expr->getBody();
01070 }
01071
01072 inline void Expr::setTriggers(const std::vector< std::vector<Expr> >& triggers) const {
01073 DebugAssert(isClosure(),
01074 "CVC3::Expr::setTriggers(): not a closure Expr:\n "
01075 + toString(AST_LANG));
01076 d_expr->setTriggers(triggers);
01077 }
01078
01079 inline const std::vector<std::vector<Expr> >& Expr::getTrigs() const {
01080 DebugAssert(isClosure(),
01081 "CVC3::Expr::getTrigs(): not a closure Expr:\n "
01082 + toString(AST_LANG));
01083 return d_expr->getTrigs();
01084 }
01085
01086 inline const Expr& Expr::getExistential() const {
01087 DebugAssert(isSkolem(),
01088 "CVC3::Expr::getExistential() not a skolem variable");
01089 return d_expr->getExistential();
01090 }
01091 inline int Expr::getBoundIndex() const {
01092 DebugAssert(isSkolem(),
01093 "CVC3::Expr::getBoundIndex() not a skolem variable");
01094 return d_expr->getBoundIndex();
01095 }
01096
01097
01098 inline const Rational& Expr::getRational() const {
01099 DebugAssert(isRational(),
01100 "CVC3::Expr::getRational(): not a rational Expr:\n "
01101 + toString(AST_LANG));
01102 return d_expr->getRational();
01103 }
01104
01105 inline const Theorem& Expr::getTheorem() const {
01106 DebugAssert(isTheorem(),
01107 "CVC3::Expr::getTheorem(): not a Theorem Expr:\n "
01108 + toString(AST_LANG));
01109 return d_expr->getTheorem();
01110 }
01111
01112 inline const std::string& Expr::getUid() const {
01113 DebugAssert(getKind() == BOUND_VAR,
01114 "CVC3::Expr::getUid(): not a BOUND_VAR Expr:\n "
01115 + toString(AST_LANG));
01116 return d_expr->getUid();
01117 }
01118
01119 inline ExprManager* Expr::getEM() const {
01120 DebugAssert(d_expr != NULL,
01121 "CVC3::Expr:getEM: on Null Expr (not initialized)");
01122 return d_expr->d_em;
01123 }
01124
01125 inline const std::vector<Expr>& Expr::getKids() const {
01126 DebugAssert(d_expr != NULL, "Expr::getKids on Null Expr");
01127 if(isNull()) return getEM()->getEmptyVector();
01128 else return d_expr->getKids();
01129 }
01130
01131 inline int Expr::getKind() const {
01132 if(d_expr == NULL) return NULL_KIND;
01133 return d_expr->d_kind;
01134 }
01135
01136 inline ExprIndex Expr::getIndex() const { return d_expr->d_index; }
01137
01138 inline bool Expr::hasLastIndex() const
01139 { return d_expr->d_em->lastIndex() == getIndex(); }
01140
01141 inline Op Expr::mkOp() const {
01142 DebugAssert(!isNull(), "Expr::mkOp() on Null expr");
01143 return Op(*this);
01144 }
01145
01146 inline Op Expr::getOp() const {
01147 DebugAssert(!isNull(), "Expr::getOp() on Null expr");
01148 if (isApply()) return d_expr->getOp();
01149 DebugAssert(arity() > 0,
01150 "Expr::getOp() called on non-apply expr with no children");
01151 return Op(getKind());
01152 }
01153
01154 inline Expr Expr::getOpExpr() const {
01155 DebugAssert(isApply(), "getOpExpr() called on non-apply");
01156 return getOp().getExpr();
01157 }
01158
01159 inline int Expr::getOpKind() const {
01160 if (!isApply()) return getKind();
01161 return getOp().getExpr().getKind();
01162 }
01163
01164 inline int Expr::arity() const {
01165 if(isNull()) return 0;
01166 else return d_expr->arity();
01167 }
01168
01169 inline const Expr& Expr::operator[](int i) const {
01170 DebugAssert(i < arity(), "out of bounds access");
01171 return (d_expr->getKids())[i];
01172 }
01173
01174 inline Expr::iterator Expr::begin() const {
01175 if (isNull() || d_expr->arity() == 0)
01176 return Expr::iterator(getEM()->getEmptyVector().begin());
01177 else return Expr::iterator(d_expr->getKids().begin());
01178 }
01179
01180 inline Expr::iterator Expr::end() const {
01181 if (isNull() || d_expr->arity() == 0)
01182 return Expr::iterator(getEM()->getEmptyVector().end());
01183 else return Expr::iterator(d_expr->getKids().end());
01184 }
01185
01186 inline bool Expr::isNull() const {
01187 return (d_expr == NULL) || (d_expr->d_kind == NULL_KIND);
01188 }
01189
01190 inline size_t Expr::getMMIndex() const {
01191 DebugAssert(!isNull(), "Expr::getMMIndex()");
01192 return d_expr->getMMIndex();
01193 }
01194
01195 inline bool Expr::hasFind() const {
01196 DebugAssert(!isNull(), "hasFind called on NULL Expr");
01197 return (d_expr->d_find && !(d_expr->d_find->get().isNull()));
01198 }
01199
01200 inline const Theorem& Expr::getFind() const {
01201 DebugAssert(hasFind(), "Should only be called if find is valid");
01202 return d_expr->d_find->get();
01203 }
01204
01205 inline int Expr::getFindLevel() const {
01206 DebugAssert(hasFind(), "Should only be called if find is valid");
01207 return d_expr->d_find->level();
01208 }
01209
01210 inline const Theorem& Expr::getEqNext() const {
01211 DebugAssert(!isNull(), "getEqNext called on NULL Expr");
01212 DebugAssert(hasFind(), "Should only be called if find is valid");
01213 DebugAssert(d_expr->d_eqNext, "getEqNext: d_eqNext is NULL");
01214 return d_expr->d_eqNext->get();
01215 }
01216
01217 inline NotifyList* Expr::getNotify() const {
01218 if(isNull()) return NULL;
01219 else return d_expr->d_notifyList;
01220 }
01221
01222 inline Type Expr::getType() const {
01223 if (isNull()) return s_null;
01224 if (d_expr->d_type.isNull()) getEM()->computeType(*this);
01225 return d_expr->d_type;
01226 }
01227
01228 inline Type Expr::lookupType() const {
01229 if (isNull()) return s_null;
01230 return d_expr->d_type;
01231 }
01232
01233 inline Cardinality Expr::typeCard() const {
01234 DebugAssert(!isNull(), "typeCard called on NULL Expr");
01235 Expr e(*this);
01236 Unsigned n;
01237 return getEM()->finiteTypeInfo(e, n, false, false);
01238 }
01239
01240 inline Expr Expr::typeEnumerateFinite(Unsigned n) const {
01241 DebugAssert(!isNull(), "typeEnumerateFinite called on NULL Expr");
01242 Expr e(*this);
01243 Cardinality card = getEM()->finiteTypeInfo(e, n, true, false);
01244 if (card != CARD_FINITE) e = Expr();
01245 return e;
01246 }
01247
01248 inline Unsigned Expr::typeSizeFinite() const {
01249 DebugAssert(!isNull(), "typeCard called on NULL Expr");
01250 Expr e(*this);
01251 Unsigned n;
01252 Cardinality card = getEM()->finiteTypeInfo(e, n, false, true);
01253 if (card != CARD_FINITE) n = 0;
01254 return n;
01255 }
01256
01257 inline bool Expr::validSimpCache() const {
01258 return d_expr->d_simpCacheTag == getEM()->getSimpCacheTag();
01259 }
01260
01261 inline const Theorem& Expr::getSimpCache() const {
01262 return d_expr->d_simpCache;
01263 }
01264
01265 inline bool Expr::isValidType() const {
01266 return d_expr->d_dynamicFlags.get(VALID_TYPE);
01267 }
01268
01269 inline bool Expr::validIsAtomicFlag() const {
01270 return d_expr->d_dynamicFlags.get(VALID_IS_ATOMIC);
01271 }
01272
01273 inline bool Expr::validTerminalsConstFlag() const {
01274 return d_expr->d_dynamicFlags.get(VALID_TERMINALS_CONST);
01275 }
01276
01277 inline bool Expr::getIsAtomicFlag() const {
01278 return d_expr->d_dynamicFlags.get(IS_ATOMIC);
01279 }
01280
01281 inline bool Expr::getTerminalsConstFlag() const {
01282 return d_expr->d_dynamicFlags.get(TERMINALS_CONST);
01283 }
01284
01285 inline bool Expr::isRewriteNormal() const {
01286 return d_expr->d_dynamicFlags.get(REWRITE_NORMAL);
01287 }
01288
01289 inline bool Expr::isFinite() const {
01290 return d_expr->d_dynamicFlags.get(IS_FINITE);
01291 }
01292
01293 inline bool Expr::isWellFounded() const {
01294 return d_expr->d_dynamicFlags.get(WELL_FOUNDED);
01295 }
01296
01297 inline bool Expr::computeTransClosure() const {
01298 return d_expr->d_dynamicFlags.get(COMPUTE_TRANS_CLOSURE);
01299 }
01300
01301 inline bool Expr::containsBoundVar() const {
01302 return d_expr->d_dynamicFlags.get(CONTAINS_BOUND_VAR);
01303 }
01304
01305 inline bool Expr::usesCC() const {
01306 return d_expr->d_dynamicFlags.get(USES_CC);
01307 }
01308
01309 inline bool Expr::notArrayNormalized() const {
01310 return d_expr->d_dynamicFlags.get(NOT_ARRAY_NORMALIZED);
01311 }
01312
01313 inline bool Expr::isImpliedLiteral() const {
01314 return d_expr->d_dynamicFlags.get(IMPLIED_LITERAL);
01315 }
01316
01317 inline bool Expr::isUserAssumption() const {
01318 return d_expr->d_dynamicFlags.get(IS_USER_ASSUMPTION);
01319 }
01320
01321 inline bool Expr::inUserAssumption() const {
01322 return d_expr->d_dynamicFlags.get(IN_USER_ASSUMPTION);
01323 }
01324
01325 inline bool Expr::isIntAssumption() const {
01326 return d_expr->d_dynamicFlags.get(IS_INT_ASSUMPTION);
01327 }
01328
01329 inline bool Expr::isJustified() const {
01330 return d_expr->d_dynamicFlags.get(IS_JUSTIFIED);
01331 }
01332
01333 inline bool Expr::isTranslated() const {
01334 return d_expr->d_dynamicFlags.get(IS_TRANSLATED);
01335 }
01336
01337 inline bool Expr::isUserRegisteredAtom() const {
01338 return d_expr->d_dynamicFlags.get(IS_USER_REGISTERED_ATOM);
01339 }
01340
01341 inline bool Expr::isRegisteredAtom() const {
01342 return d_expr->d_dynamicFlags.get(IS_REGISTERED_ATOM);
01343 }
01344
01345 inline bool Expr::isSelected() const {
01346 return d_expr->d_dynamicFlags.get(IS_SELECTED);
01347 }
01348
01349 inline bool Expr::isStoredPredicate() const {
01350 return d_expr->d_dynamicFlags.get(IS_STORED_PREDICATE);
01351 }
01352
01353 inline bool Expr::getFlag() const {
01354 DebugAssert(!isNull(), "Expr::getFlag() on Null Expr");
01355 return (d_expr->d_flag == getEM()->getFlag());
01356 }
01357
01358 inline void Expr::setFlag() const {
01359 DebugAssert(!isNull(), "Expr::setFlag() on Null Expr");
01360 d_expr->d_flag = getEM()->getFlag();
01361 }
01362
01363 inline void Expr::clearFlags() const {
01364 DebugAssert(!isNull(), "Expr::clearFlags() on Null Expr");
01365 getEM()->clearFlags();
01366 }
01367
01368 inline void Expr::setFind(const Theorem& e) const {
01369 DebugAssert(!isNull(), "Expr::setFind() on Null expr");
01370 DebugAssert(e.getLHS() == *this, "bad call to setFind");
01371 if (d_expr->d_find) d_expr->d_find->set(e);
01372 else {
01373 CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
01374 d_expr->d_find = tmp;
01375 IF_DEBUG(tmp->setName("CDO[Expr.find]");)
01376 }
01377 }
01378
01379 inline void Expr::setEqNext(const Theorem& e) const {
01380 DebugAssert(!isNull(), "Expr::setEqNext() on Null expr");
01381 DebugAssert(e.getLHS() == *this, "bad call to setEqNext");
01382 if (d_expr->d_eqNext) d_expr->d_eqNext->set(e);
01383 else {
01384 CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
01385 d_expr->d_eqNext = tmp;
01386 IF_DEBUG(tmp->setName("CDO[Expr.eqNext]");)
01387 }
01388 }
01389
01390 inline void Expr::setType(const Type& t) const {
01391 DebugAssert(!isNull(), "Expr::setType() on Null expr");
01392 d_expr->d_type = t;
01393 }
01394
01395 inline void Expr::setSimpCache(const Theorem& e) const {
01396 DebugAssert(!isNull(), "Expr::setSimpCache() on Null expr");
01397 d_expr->d_simpCache = e;
01398 d_expr->d_simpCacheTag = getEM()->getSimpCacheTag();
01399 }
01400
01401 inline void Expr::setValidType() const {
01402 DebugAssert(!isNull(), "Expr::setValidType() on Null expr");
01403 d_expr->d_dynamicFlags.set(VALID_TYPE, 0);
01404 }
01405
01406 inline void Expr::setIsAtomicFlag(bool value) const {
01407 DebugAssert(!isNull(), "Expr::setIsAtomicFlag() on Null expr");
01408 d_expr->d_dynamicFlags.set(VALID_IS_ATOMIC, 0);
01409 if (value) d_expr->d_dynamicFlags.set(IS_ATOMIC, 0);
01410 else d_expr->d_dynamicFlags.clear(IS_ATOMIC, 0);
01411 }
01412
01413 inline void Expr::setTerminalsConstFlag(bool value) const {
01414 DebugAssert(!isNull(), "Expr::setTerminalsConstFlag() on Null expr");
01415 d_expr->d_dynamicFlags.set(VALID_TERMINALS_CONST, 0);
01416 if (value) d_expr->d_dynamicFlags.set(TERMINALS_CONST, 0);
01417 else d_expr->d_dynamicFlags.clear(TERMINALS_CONST, 0);
01418 }
01419
01420 inline void Expr::setRewriteNormal() const {
01421 DebugAssert(!isNull(), "Expr::setRewriteNormal() on Null expr");
01422 TRACE("setRewriteNormal", "setRewriteNormal(", *this, ")");
01423 d_expr->d_dynamicFlags.set(REWRITE_NORMAL, 0);
01424 }
01425
01426 inline void Expr::setFinite() const {
01427 DebugAssert(!isNull(), "Expr::setFinite() on Null expr");
01428 d_expr->d_dynamicFlags.set(IS_FINITE, 0);
01429 }
01430
01431 inline void Expr::setWellFounded() const {
01432 DebugAssert(!isNull(), "Expr::setWellFounded() on Null expr");
01433 d_expr->d_dynamicFlags.set(WELL_FOUNDED, 0);
01434 }
01435
01436 inline void Expr::setComputeTransClosure() const {
01437 DebugAssert(!isNull(), "Expr::setComputeTransClosure() on Null expr");
01438 d_expr->d_dynamicFlags.set(COMPUTE_TRANS_CLOSURE, 0);
01439 }
01440
01441 inline void Expr::setContainsBoundVar() const {
01442 DebugAssert(!isNull(), "Expr::setContainsBoundVar() on Null expr");
01443 d_expr->d_dynamicFlags.set(CONTAINS_BOUND_VAR, 0);
01444 }
01445
01446 inline void Expr::setUsesCC() const {
01447 DebugAssert(!isNull(), "Expr::setUsesCC() on Null expr");
01448 d_expr->d_dynamicFlags.set(USES_CC, 0);
01449 }
01450
01451 inline void Expr::setNotArrayNormalized() const {
01452 DebugAssert(!isNull(), "Expr::setContainsBoundVar() on Null expr");
01453 d_expr->d_dynamicFlags.set(NOT_ARRAY_NORMALIZED);
01454 }
01455
01456 inline void Expr::setImpliedLiteral() const {
01457 DebugAssert(!isNull(), "Expr::setImpliedLiteral() on Null expr");
01458 d_expr->d_dynamicFlags.set(IMPLIED_LITERAL);
01459 }
01460
01461 inline void Expr::setUserAssumption(int scope) const {
01462 DebugAssert(!isNull(), "Expr::setUserAssumption() on Null expr");
01463 d_expr->d_dynamicFlags.set(IS_USER_ASSUMPTION, scope);
01464 }
01465
01466 inline void Expr::setInUserAssumption(int scope) const {
01467 DebugAssert(!isNull(), "Expr::setInUserAssumption() on Null expr");
01468 d_expr->d_dynamicFlags.set(IN_USER_ASSUMPTION, scope);
01469 }
01470
01471 inline void Expr::setIntAssumption() const {
01472 DebugAssert(!isNull(), "Expr::setIntAssumption() on Null expr");
01473 d_expr->d_dynamicFlags.set(IS_INT_ASSUMPTION);
01474 }
01475
01476 inline void Expr::setJustified() const {
01477 DebugAssert(!isNull(), "Expr::setJustified() on Null expr");
01478 d_expr->d_dynamicFlags.set(IS_JUSTIFIED);
01479 }
01480
01481 inline void Expr::setTranslated(int scope) const {
01482 DebugAssert(!isNull(), "Expr::setTranslated() on Null expr");
01483 d_expr->d_dynamicFlags.set(IS_TRANSLATED, scope);
01484 }
01485
01486 inline void Expr::setUserRegisteredAtom() const {
01487 DebugAssert(!isNull(), "Expr::setUserRegisteredAtom() on Null expr");
01488 d_expr->d_dynamicFlags.set(IS_USER_REGISTERED_ATOM);
01489 }
01490
01491 inline void Expr::setRegisteredAtom() const {
01492 DebugAssert(!isNull(), "Expr::setUserRegisteredAtom() on Null expr");
01493 d_expr->d_dynamicFlags.set(IS_REGISTERED_ATOM);
01494 }
01495
01496 inline void Expr::setSelected() const {
01497 DebugAssert(!isNull(), "Expr::setSelected() on Null expr");
01498 d_expr->d_dynamicFlags.set(IS_SELECTED);
01499 }
01500
01501 inline void Expr::setStoredPredicate() const {
01502 DebugAssert(!isNull(), "Expr::setStoredPredicate() on Null expr");
01503 d_expr->d_dynamicFlags.set(IS_STORED_PREDICATE);
01504 }
01505
01506 inline void Expr::clearRewriteNormal() const {
01507 DebugAssert(!isNull(), "Expr::clearRewriteNormal() on Null expr");
01508 d_expr->d_dynamicFlags.clear(REWRITE_NORMAL, 0);
01509 }
01510
01511 inline bool Expr::hasSig() const {
01512 return (!isNull()
01513 && d_expr->getSig() != NULL
01514 && !(d_expr->getSig()->get().isNull()));
01515 }
01516
01517 inline bool Expr::hasRep() const {
01518 return (!isNull()
01519 && d_expr->getRep() != NULL
01520 && !(d_expr->getRep()->get().isNull()));
01521 }
01522
01523 inline const Theorem& Expr::getSig() const {
01524 static Theorem nullThm;
01525 DebugAssert(!isNull(), "Expr::getSig() on Null expr");
01526 if(d_expr->getSig() != NULL)
01527 return d_expr->getSig()->get();
01528 else
01529 return nullThm;
01530 }
01531
01532 inline const Theorem& Expr::getRep() const {
01533 static Theorem nullThm;
01534 DebugAssert(!isNull(), "Expr::getRep() on Null expr");
01535 if(d_expr->getRep() != NULL)
01536 return d_expr->getRep()->get();
01537 else
01538 return nullThm;
01539 }
01540
01541 inline void Expr::setSig(const Theorem& e) const {
01542 DebugAssert(!isNull(), "Expr::setSig() on Null expr");
01543 CDO<Theorem>* sig = d_expr->getSig();
01544 if(sig != NULL) sig->set(e);
01545 else {
01546 CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
01547 d_expr->setSig(tmp);
01548 IF_DEBUG(tmp->setName("CDO[Expr.sig] in "+toString());)
01549 }
01550 }
01551
01552 inline void Expr::setRep(const Theorem& e) const {
01553 DebugAssert(!isNull(), "Expr::setRep() on Null expr");
01554 CDO<Theorem>* rep = d_expr->getRep();
01555 if(rep != NULL) rep->set(e);
01556 else {
01557 CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
01558 d_expr->setRep(tmp);
01559 IF_DEBUG(tmp->setName("CDO[Expr.rep] in "+toString());)
01560 }
01561 }
01562
01563 inline bool operator==(const Expr& e1, const Expr& e2) {
01564
01565 return e1.d_expr == e2.d_expr;
01566 }
01567
01568 inline bool operator!=(const Expr& e1, const Expr& e2)
01569 { return !(e1 == e2); }
01570
01571
01572
01573 inline bool operator<(const Expr& e1, const Expr& e2)
01574 { return compare(e1,e2) < 0; }
01575 inline bool operator<=(const Expr& e1, const Expr& e2)
01576 { return compare(e1,e2) <= 0; }
01577 inline bool operator>(const Expr& e1, const Expr& e2)
01578 { return compare(e1,e2) > 0; }
01579 inline bool operator>=(const Expr& e1, const Expr& e2)
01580 { return compare(e1,e2) >= 0; }
01581
01582 }
01583
01584 #endif