CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file expr.h 00004 * \brief Definition of the API to expression package. See class Expr for details. 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Tue Nov 26 00:27:40 2002 00009 * 00010 * <hr> 00011 * 00012 * License to use, copy, modify, sell and/or distribute this software 00013 * and its documentation for any purpose is hereby granted without 00014 * royalty, subject to the terms and conditions defined in the \ref 00015 * LICENSE file provided with this distribution. 00016 * 00017 * <hr> 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 // Internal data-holding classes 00057 class ExprValue; 00058 class ExprNode; 00059 // Printing 00060 class ExprStream; 00061 00062 //! Type ID of each ExprValue subclass. 00063 /*! It is defined in expr.h, so that ExprManager can use it before loading 00064 expr_value.h */ 00065 typedef enum { 00066 EXPR_VALUE, 00067 EXPR_NODE, 00068 EXPR_APPLY, //!< Application of functions and predicates 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 // The end of list; don't assign it to any subclass 00077 } ExprValueType; 00078 00079 //! Enum for cardinality of types 00080 typedef enum { 00081 CARD_FINITE, 00082 CARD_INFINITE, 00083 CARD_UNKNOWN 00084 } Cardinality; 00085 00086 //! Expression index type 00087 typedef long unsigned ExprIndex; 00088 00089 /**************************************************************************/ 00090 /*! \defgroup ExprPkg Expression Package 00091 * \ingroup BuildingBlocks 00092 */ 00093 /**************************************************************************/ 00094 /*! \defgroup Expr_SmartPointer Smart Pointer Functionality in Expr 00095 * \ingroup ExprPkg 00096 */ 00097 /**************************************************************************/ 00098 00099 /**************************************************************************/ 00100 //! Data structure of expressions in CVC3 00101 /*! \ingroup ExprPkg 00102 * Class: Expr <br> 00103 * Author: Clark Barrett <br> 00104 * Created: Mon Nov 25 15:29:37 2002 00105 * 00106 * This class is the main data structure for expressions that all 00107 * other components should use. It is actually a <em>smart 00108 * pointer</em> to the actual data holding class ExprValue and its 00109 * subclasses. 00110 * 00111 * Expressions are represented as DAGs with maximal sharing of 00112 * subexpressions. Therefore, testing for equality is a constant time 00113 * operation (simply compare the pointers). 00114 * 00115 * Unused expressions are automatically garbage-collected. The use is 00116 * determined by a reference counting mechanism. In particular, this 00117 * means that if there is a circular dependency among expressions 00118 * (e.g. an attribute points back to the expression itself), these 00119 * expressions will not be garbage-collected, even if no one else is 00120 * using them. 00121 * 00122 * The most frequently used operations are getKind() (determining the 00123 * kind of the top level node of the expression), arity() (how many 00124 * children an Expr has), operator[]() for accessing a child, and 00125 * various testers and methods for constructing new expressions. 00126 * 00127 * In addition, a total ordering operator<() is provided. It is 00128 * guaranteed to remain the same for the lifetime of the expressions 00129 * (it may change, however, if the expression is garbage-collected and 00130 * reborn). 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 /*! \addtogroup ExprPkg 00144 * @{ 00145 */ 00146 //! bit-masks for static flags 00147 typedef enum { 00148 //! Whether is valid TYPE expr 00149 VALID_TYPE = 0x1, 00150 //! Whether IS_ATOMIC flag is valid (initialized) 00151 VALID_IS_ATOMIC = 0x2, 00152 //! Whether the expression is an atomic term or formula 00153 IS_ATOMIC = 0x4, 00154 //! Expression is the result of a "normal" (idempotent) rewrite 00155 REWRITE_NORMAL = 0x8, 00156 //! Finite type 00157 IS_FINITE = 0x400, 00158 //! Well-founded (used in datatypes) 00159 WELL_FOUNDED = 0x800, 00160 //! Compute transitive closure (for binary uninterpreted predicates) 00161 COMPUTE_TRANS_CLOSURE = 0x1000, 00162 //! Whether expr contains a bounded variable (for quantifier instantiation) 00163 CONTAINS_BOUND_VAR = 0x00020000, 00164 //! Whether expr uses CC algorithm that relies on not simplifying an expr that has a find 00165 USES_CC = 0x00080000, 00166 //! Whether TERMINALS_CONST flag is valid (initialized) 00167 VALID_TERMINALS_CONST = 0x00100000, 00168 //! Whether expr contains only numerical constants at all possible ite terminals 00169 TERMINALS_CONST = 0x00200000 00170 } StaticFlagsEnum; 00171 00172 //! bit-masks for dynamic flags 00173 // TODO: Registered flags instead of hard-wired 00174 typedef enum { 00175 //! Whether expr has been added as an implied literal 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 //! Whether expr is normalized (in array theory) 00187 NOT_ARRAY_NORMALIZED = 0x00040000 00188 } DynamicFlagsEnum; 00189 00190 //! Convenient null expr 00191 static Expr s_null; 00192 00193 ///////////////////////////////////////////////////////////////////////////// 00194 // Private Dynamic Data // 00195 ///////////////////////////////////////////////////////////////////////////// 00196 //! The value. This is the only data member in this class. 00197 ExprValue* d_expr; 00198 00199 ///////////////////////////////////////////////////////////////////////////// 00200 // Private methods // 00201 ///////////////////////////////////////////////////////////////////////////// 00202 00203 //! Private constructor, simply wraps around the pointer 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 // Public Classes and Types // 00214 ///////////////////////////////////////////////////////////////////////////// 00215 00216 ///////////////////////////////////////////////////////////////////////////// 00217 /*! 00218 * Class: Expr::iterator 00219 * Author: Sergey Berezin 00220 * Created: Fri Dec 6 15:38:51 2002 00221 * Description: STL-like iterator API to the Expr's children. 00222 * IMPORTANT: the iterator will not be valid after the originating 00223 * expression is destroyed. 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 // Private constructors (used by Expr only) 00233 // 00234 //! Construct an iterator out of the vector's iterator 00235 iterator(std::vector<Expr>::const_iterator it): d_it(it) { } 00236 // Public methods 00237 public: 00238 //! Default constructor 00239 iterator() { } 00240 // Copy constructor and operator= are defined by C++, that's good enough 00241 00242 //! Equality 00243 bool operator==(const iterator& i) const { 00244 return d_it == i.d_it; 00245 } 00246 //! Disequality 00247 bool operator!=(const iterator& i) const { return !(*this == i); } 00248 //! Dereference operator 00249 const Expr& operator*() const { return *d_it; } 00250 //! Dereference and member access 00251 const Expr* operator->() const { return &(operator*()); } 00252 //! Prefix increment 00253 iterator& operator++() { 00254 ++d_it; 00255 return *this; 00256 } 00257 /*! @brief Postfix increment requires a Proxy object to hold the 00258 * intermediate value for dereferencing */ 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 //! Postfix increment 00266 /*! \return Proxy with the old Expr. 00267 * 00268 * Now, an expression like *i++ will return the current *i, and 00269 * then advance the iterator. However, don't try to use Proxy for 00270 * anything else. 00271 */ 00272 Proxy operator++(int) { 00273 Proxy e(*(*this)); 00274 ++(*this); 00275 return e; 00276 } 00277 }; // end of class Expr::iterator 00278 00279 ///////////////////////////////////////////////////////////////////////////// 00280 // Constructors // 00281 ///////////////////////////////////////////////////////////////////////////// 00282 00283 //! Default constructor creates the Null Expr 00284 Expr(): d_expr(NULL) {} 00285 00286 /*! @brief Copy constructor and assignment (copy the pointer and take care 00287 of the refcount) */ 00288 Expr(const Expr& e); 00289 //! Assignment operator: take care of the refcounting and GC 00290 Expr& operator=(const Expr& e); 00291 00292 // These constructors grab the ExprManager from the Op or the first 00293 // child. The operator and all children must belong to the same 00294 // ExprManager. 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 //! Destructor 00305 ~Expr(); 00306 00307 // Compound expression constructors 00308 Expr eqExpr(const Expr& right) const; 00309 Expr notExpr() const; 00310 Expr negate() const; // avoid double-negatives 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 //! Create a Skolem constant for the i'th variable of an existential (*this) 00318 Expr skolemExpr(int i) const; 00319 //! Create a Boolean variable out of the expression 00320 // Expr boolVarExpr() const; 00321 //! Rebuild Expr with a new ExprManager 00322 Expr rebuild(ExprManager* em) const; 00323 // Expr newForall(const Expr& e); 00324 // Expr newExists(const Expr& e); 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 // by yeting, a special subst function for TheoryQuant 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 // Public Static Methods // 00340 ///////////////////////////////////////////////////////////////////////////// 00341 00342 static size_t hash(const Expr& e); 00343 00344 ///////////////////////////////////////////////////////////////////////////// 00345 // Read-only (const) methods // 00346 ///////////////////////////////////////////////////////////////////////////// 00347 00348 size_t hash() const; 00349 00350 // Core expression testers 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 //! Expr represents a type 00370 bool isType() const; 00371 /* 00372 bool isRecord() const; 00373 bool isRecordAccess() const; 00374 bool isTupleAccess() const; 00375 */ 00376 //! Provide access to ExprValue for client subclasses of ExprValue *only* 00377 /*@ Calling getExprValue on an Expr with a built-in ExprValue class will 00378 * cause an error */ 00379 const ExprValue* getExprValue() const; 00380 00381 //! Test if e is a term (as opposed to a predicate/formula) 00382 bool isTerm() const; 00383 //! Test if e is atomic 00384 /*! An atomic expression is TRUE or FALSE or one that does not 00385 * contain a formula (including not being a formula itself). 00386 * \sa isAtomicFormula */ 00387 bool isAtomic() const; 00388 //! Test if e is an atomic formula 00389 /*! An atomic formula is TRUE or FALSE or an application of a predicate 00390 (possibly 0-ary) which does not properly contain any formula. For 00391 instance, the formula "x = IF f THEN y ELSE z ENDIF" is not an atomic 00392 formula, since it contains the condition "f", which is a formula. */ 00393 bool isAtomicFormula() const; 00394 //! An abstract atomic formua is an atomic formula or a quantified formula 00395 bool isAbsAtomicFormula() const 00396 { return isQuantifier() || isAtomicFormula(); } 00397 //! Test if e is a literal 00398 /*! A literal is an atomic formula, or its negation. 00399 \sa isAtomicFormula */ 00400 bool isLiteral() const 00401 { return (isAtomicFormula() || (isNot() && (*this)[0].isAtomicFormula())); } 00402 //! Test if e is an abstract literal 00403 bool isAbsLiteral() const 00404 { return (isAbsAtomicFormula() || (isNot() && (*this)[0].isAbsAtomicFormula())); } 00405 //! A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool) 00406 bool isBoolConnective() const; 00407 //! True iff expr is not a Bool connective 00408 bool isPropAtom() const { return !isTerm() && !isBoolConnective(); } 00409 //! PropAtom or negation of PropAtom 00410 bool isPropLiteral() const 00411 { return (isNot() && (*this)[0].isPropAtom()) || isPropAtom(); } 00412 //! Return whether Expr contains a non-bool type ITE as a sub-term 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 // Leaf accessors - these functions must only be called one expressions of 00432 // the appropriate kind. 00433 00434 // For UCONST and BOUND_VAR Expr's 00435 const std::string& getName() const; 00436 //! For BOUND_VAR, get the UID 00437 const std::string& getUid() const; 00438 00439 // For STRING_EXPR's 00440 const std::string& getString() const; 00441 //! Get bound variables from a closure Expr 00442 const std::vector<Expr>& getVars() const; 00443 //! Get the existential axiom expression for skolem constant 00444 const Expr& getExistential() const; 00445 //! Get the index of the bound var that skolem constant comes from 00446 int getBoundIndex() const; 00447 00448 //! Get the body of the closure Expr 00449 const Expr& getBody() const; 00450 00451 //! Set the triggers for a closure Expr 00452 void setTriggers(const std::vector<std::vector<Expr> >& triggers) const; 00453 void setTriggers(const std::vector<Expr>& triggers) const; 00454 void setTrigger(const Expr& trigger) const; 00455 void setMultiTrigger(const std::vector<Expr>& multiTrigger) const; 00456 00457 //! Get the manual triggers of the closure Expr 00458 const std::vector<std::vector<Expr> >& getTriggers() const; //by yeting 00459 00460 //! Get the Rational value out of RATIONAL_EXPR 00461 const Rational& getRational() const; 00462 //! Get theorem from THEOREM_EXPR 00463 const Theorem& getTheorem() const; 00464 00465 // Get the expression manager. The expression must be non-null. 00466 ExprManager *getEM() const; 00467 00468 // Return a ref to the vector of children. 00469 const std::vector<Expr>& getKids() const; 00470 00471 // Get the kind of this expr. 00472 int getKind() const; 00473 00474 // Get the index field 00475 ExprIndex getIndex() const; 00476 00477 // True if this is the most recently created expression 00478 bool hasLastIndex() const; 00479 00480 //! Make the expr into an operator 00481 Op mkOp() const; 00482 00483 //! Get operator from expression 00484 Op getOp() const; 00485 00486 //! Get expression of operator (for APPLY Exprs only) 00487 Expr getOpExpr() const; 00488 00489 //! Get kind of operator (for APPLY Exprs only) 00490 int getOpKind() const; 00491 00492 // Return the number of children. Note, that an application of a 00493 // user-defined function has the arity of that function (the number 00494 // of arguments), and the function name itself is part of the 00495 // operator. 00496 int arity() const; 00497 00498 // Return the ith child. As with arity, it's also the ith argument 00499 // in function application. 00500 const Expr& operator[](int i) const; 00501 00502 //! Remove leading NOT if any 00503 const Expr& unnegate() const { return isNot() ? (*this)[0] : *this; } 00504 00505 //! Begin iterator 00506 iterator begin() const; 00507 00508 //! End iterator 00509 iterator end() const; 00510 00511 // Check if Expr is Null 00512 bool isNull() const; 00513 00514 // Check if Expr is not Null 00515 bool isInitialized() const { return d_expr != NULL; } 00516 //! Get the memory manager index (it uniquely identifies the subclass) 00517 size_t getMMIndex() const; 00518 00519 // Attributes 00520 00521 // True if the find attribute has been set to something other than NULL. 00522 bool hasFind() const; 00523 00524 // Return the attached find attribute for the expr. Note that this 00525 // must be called repeatedly to get the root of the union-find tree. 00526 // Should only be called if hasFind is true. 00527 const Theorem& getFind() const; 00528 int getFindLevel() const; 00529 const Theorem& getEqNext() const; 00530 00531 // Return the notify list 00532 NotifyList* getNotify() const; 00533 00534 //! Get the type. Recursively compute if necessary 00535 Type getType() const; 00536 //! Look up the current type. Do not recursively compute (i.e. may be NULL) 00537 Type lookupType() const; 00538 //! Return cardinality of type 00539 Cardinality typeCard() const; 00540 //! Return nth (starting with 0) element in a finite type 00541 /*! Returns NULL Expr if unable to compute nth element 00542 */ 00543 Expr typeEnumerateFinite(Unsigned n) const; 00544 //! Return size of a finite type; returns 0 if size cannot be determined 00545 Unsigned typeSizeFinite() const; 00546 00547 /*! @brief Return true if there is a valid cached value for calling 00548 simplify on this Expr. */ 00549 bool validSimpCache() const; 00550 00551 // Get the cached Simplify of this Expr. 00552 const Theorem& getSimpCache() const; 00553 00554 // Return true if valid type flag is set for Expr 00555 bool isValidType() const; 00556 00557 // Return true if there is a valid flag for whether Expr is atomic 00558 bool validIsAtomicFlag() const; 00559 00560 // Return true if there is a valid flag for whether terminals are const 00561 bool validTerminalsConstFlag() const; 00562 00563 // Get the isAtomic flag 00564 bool getIsAtomicFlag() const; 00565 00566 // Get the TerminalsConst flag 00567 bool getTerminalsConstFlag() const; 00568 00569 // Get the RewriteNormal flag 00570 bool isRewriteNormal() const; 00571 00572 // Get the isFinite flag 00573 bool isFinite() const; 00574 00575 // Get the WellFounded flag 00576 bool isWellFounded() const; 00577 00578 // Get the ComputeTransClosure flag 00579 bool computeTransClosure() const; 00580 00581 // Get the ContainsBoundVar flag 00582 bool containsBoundVar() const; 00583 00584 // Get the usesCC flag 00585 bool usesCC() const; 00586 00587 // Get the notArrayNormalized flag 00588 bool notArrayNormalized() const; 00589 00590 // Get the ImpliedLiteral flag 00591 bool isImpliedLiteral() const; 00592 00593 // Get the UserAssumption flag 00594 bool isUserAssumption() const; 00595 00596 // Get the inUserAssumption flag 00597 bool inUserAssumption() const; 00598 00599 // Get the IntAssumption flag 00600 bool isIntAssumption() const; 00601 00602 // Get the Justified flag 00603 bool isJustified() const; 00604 00605 // Get the Translated flag 00606 bool isTranslated() const; 00607 00608 // Get the UserRegisteredAtom flag 00609 bool isUserRegisteredAtom() const; 00610 00611 // Get the RegisteredAtom flag 00612 bool isRegisteredAtom() const; 00613 00614 // Get the Selected flag 00615 bool isSelected() const; 00616 00617 // Get the Stored Predicate flag 00618 bool isStoredPredicate() const; 00619 00620 //! Check if the generic flag is set 00621 bool getFlag() const; 00622 //! Set the generic flag 00623 void setFlag() const; 00624 //! Clear the generic flag in all Exprs 00625 void clearFlags() const; 00626 00627 // Printing functions 00628 00629 //! Print the expression to a string 00630 std::string toString() const; 00631 //! Print the expression to a string using the given output language 00632 std::string toString(InputLanguage lang) const; 00633 //! Print the expression in the specified format 00634 void print(InputLanguage lang, bool dagify = true) const; 00635 00636 //! Print the expression as AST (lisp-like format) 00637 void print() const { print(AST_LANG); } 00638 //! Print the expression as AST without dagifying 00639 void printnodag() const; 00640 00641 //! Pretty-print the expression 00642 void pprint() const; 00643 //! Pretty-print without dagifying 00644 void pprintnodag() const; 00645 00646 //! Print a leaf node 00647 /*@ The top node is pretty-printed if it is a basic leaf type; 00648 * otherwise, just the kind is printed. Should only be called on expressions 00649 * with no children. */ 00650 ExprStream& print(ExprStream& os) const; 00651 //! Print the top node and then recurse through the children */ 00652 /*@ The top node is printed as an AST with all the information, including 00653 * "hidden" Exprs that are part of the ExprValue */ 00654 ExprStream& printAST(ExprStream& os) const; 00655 //! Set initial indentation to n. 00656 /*! The indentation will be reset to default unless the second 00657 argument is true. 00658 \return reference to itself, so one can write `os << e.indent(5)' 00659 */ 00660 Expr& indent(int n, bool permanent = false); 00661 00662 ///////////////////////////////////////////////////////////////////////////// 00663 // Other Public methods // 00664 ///////////////////////////////////////////////////////////////////////////// 00665 00666 // Attributes 00667 00668 //! Set the find attribute to e 00669 void setFind(const Theorem& e) const; 00670 00671 //! Set the eqNext attribute to e 00672 void setEqNext(const Theorem& e) const; 00673 00674 //! Add (e,i) to the notify list of this expression 00675 void addToNotify(Theory* i, const Expr& e) const; 00676 00677 //! Set the cached type 00678 void setType(const Type& t) const; 00679 00680 // Cache the result of a call to Simplify on this Expr 00681 void setSimpCache(const Theorem& e) const; 00682 00683 // Set the valid type flag for this Expr 00684 void setValidType() const; 00685 00686 // Set the isAtomicFlag for this Expr 00687 void setIsAtomicFlag(bool value) const; 00688 00689 // Set the TerminalsConst flag for this Expr 00690 void setTerminalsConstFlag(bool value) const; 00691 00692 // Set or clear the RewriteNormal flag 00693 void setRewriteNormal() const; 00694 void clearRewriteNormal() const; 00695 00696 // Set the isFinite flag 00697 void setFinite() const; 00698 00699 // Set the WellFounded flag 00700 void setWellFounded() const; 00701 00702 // Set the ComputeTransClosure flag 00703 void setComputeTransClosure() const; 00704 00705 // Set the ContainsBoundVar flag 00706 void setContainsBoundVar() const; 00707 00708 // Set the UsesCC flag 00709 void setUsesCC() const; 00710 00711 // Set the notArrayNormalized flag 00712 void setNotArrayNormalized() const; 00713 00714 // Set the impliedLiteral flag for this Expr 00715 void setImpliedLiteral() const; 00716 00717 // Set the user assumption flag for this Expr 00718 void setUserAssumption(int scope = -1) const; 00719 00720 // Set the in user assumption flag for this Expr 00721 void setInUserAssumption(int scope = -1) const; 00722 00723 // Set the internal assumption flag for this Expr 00724 void setIntAssumption() const; 00725 00726 // Set the justified flag for this Expr 00727 void setJustified() const; 00728 00729 //! Set the translated flag for this Expr 00730 void setTranslated(int scope = -1) const; 00731 00732 //! Set the UserRegisteredAtom flag for this Expr 00733 void setUserRegisteredAtom() const; 00734 00735 //! Set the RegisteredAtom flag for this Expr 00736 void setRegisteredAtom() const; 00737 00738 //! Set the Selected flag for this Expr 00739 void setSelected() const; 00740 00741 //! Set the Stored Predicate flag for this Expr 00742 void setStoredPredicate() const; 00743 00744 //! Check if the current Expr (*this) is a subexpression of e 00745 bool subExprOf(const Expr& e) const; 00746 // Returns the maximum number of Boolean expressions on a path from 00747 // this to a leaf, including this. 00748 00749 inline Unsigned getSize() const; 00750 00751 // inline int getHeight() const; 00752 00753 // // Returns the index of the highest kid. 00754 // inline int getHighestKid() const; 00755 00756 // // Gets/sets an expression that this expression was simplified from 00757 // // (see newRWTheorem). This is the equivalent of SVC's Sigx. 00758 // inline bool hasSimpFrom() const; 00759 // inline const Expr& getSimpFrom() const; 00760 // inline void setSimpFrom(const Expr& simpFrom); 00761 00762 // Attributes for uninterpreted function symbols. 00763 bool hasSig() const; 00764 bool hasRep() const; 00765 const Theorem& getSig() const; 00766 const Theorem& getRep() const; 00767 void setSig(const Theorem& e) const; 00768 void setRep(const Theorem& e) const; 00769 00770 ///////////////////////////////////////////////////////////////////////////// 00771 // Friend methods // 00772 ///////////////////////////////////////////////////////////////////////////// 00773 00774 friend CVC_DLL std::ostream& operator<<(std::ostream& os, const Expr& e); 00775 00776 // The master method which defines some fixed total ordering on all 00777 // Exprs. If e1 < e2, e1==e2, and e1 > e2, it returns -1, 0, 1 00778 // respectively. A Null expr is always "smaller" than any other 00779 // expr, but is equal to itself. 00780 friend int compare(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 00785 friend bool operator<(const Expr& e1, const Expr& e2); 00786 friend bool operator<=(const Expr& e1, const Expr& e2); 00787 friend bool operator>(const Expr& e1, const Expr& e2); 00788 friend bool operator>=(const Expr& e1, const Expr& e2); 00789 00790 /*!@}*/ // end of group Expr 00791 00792 }; // end of class Expr 00793 00794 } // end of namespace CVC3 00795 00796 // Include expr_value.h here. We cannot include it earlier, since it 00797 // needs the definition of class Expr. See comments in expr_value.h. 00798 #ifndef DOXYGEN 00799 #include "expr_op.h" 00800 #include "expr_manager.h" 00801 #endif 00802 namespace CVC3 { 00803 00804 inline Expr::Expr(ExprValue* expr) : d_expr(expr) { d_expr->incRefcount(); } 00805 00806 inline Expr::Expr(const Expr& e) : d_expr(e.d_expr) { 00807 if (d_expr != NULL) d_expr->incRefcount(); 00808 } 00809 00810 inline Expr& Expr::operator=(const Expr& e) { 00811 if(&e == this) return *this; // Self-assignment 00812 ExprValue* tmp = e.d_expr; 00813 if(tmp == d_expr) return *this; 00814 if (tmp == NULL) { 00815 d_expr->decRefcount(); 00816 } 00817 else { 00818 tmp->incRefcount(); 00819 if(d_expr != NULL) { 00820 d_expr->decRefcount(); 00821 } 00822 } 00823 d_expr = tmp; 00824 return *this; 00825 } 00826 00827 inline Expr::Expr(const Op& op, const Expr& child) { 00828 ExprManager* em = child.getEM(); 00829 if (op.getKind() != APPLY) { 00830 ExprNode ev(em, op.getKind()); 00831 std::vector<Expr>& kids = ev.getKids1(); 00832 kids.push_back(child); 00833 d_expr = em->newExprValue(&ev); 00834 } else { 00835 ExprApply ev(em, op); 00836 std::vector<Expr>& kids = ev.getKids1(); 00837 kids.push_back(child); 00838 d_expr = em->newExprValue(&ev); 00839 } 00840 d_expr->incRefcount(); 00841 } 00842 00843 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1) { 00844 ExprManager* em = child0.getEM(); 00845 if (op.getKind() != APPLY) { 00846 ExprNode ev(em, op.getKind()); 00847 std::vector<Expr>& kids = ev.getKids1(); 00848 kids.push_back(child0); 00849 kids.push_back(child1); 00850 d_expr = em->newExprValue(&ev); 00851 } else { 00852 ExprApply ev(em, op); 00853 std::vector<Expr>& kids = ev.getKids1(); 00854 kids.push_back(child0); 00855 kids.push_back(child1); 00856 d_expr = em->newExprValue(&ev); 00857 } 00858 d_expr->incRefcount(); 00859 } 00860 00861 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1, 00862 const Expr& child2) { 00863 ExprManager* em = child0.getEM(); 00864 if (op.getKind() != APPLY) { 00865 ExprNode ev(em, op.getKind()); 00866 std::vector<Expr>& kids = ev.getKids1(); 00867 kids.push_back(child0); 00868 kids.push_back(child1); 00869 kids.push_back(child2); 00870 d_expr = em->newExprValue(&ev); 00871 } else { 00872 ExprApply ev(em, op); 00873 std::vector<Expr>& kids = ev.getKids1(); 00874 kids.push_back(child0); 00875 kids.push_back(child1); 00876 kids.push_back(child2); 00877 d_expr = em->newExprValue(&ev); 00878 } 00879 d_expr->incRefcount(); 00880 } 00881 00882 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1, 00883 const Expr& child2, const Expr& child3) { 00884 ExprManager* em = child0.getEM(); 00885 if (op.getKind() != APPLY) { 00886 ExprNode ev(em, op.getKind()); 00887 std::vector<Expr>& kids = ev.getKids1(); 00888 kids.push_back(child0); 00889 kids.push_back(child1); 00890 kids.push_back(child2); 00891 kids.push_back(child3); 00892 d_expr = em->newExprValue(&ev); 00893 } else { 00894 ExprApply ev(em, op); 00895 std::vector<Expr>& kids = ev.getKids1(); 00896 kids.push_back(child0); 00897 kids.push_back(child1); 00898 kids.push_back(child2); 00899 kids.push_back(child3); 00900 d_expr = em->newExprValue(&ev); 00901 } 00902 d_expr->incRefcount(); 00903 } 00904 00905 inline Expr::Expr(const Op& op, const std::vector<Expr>& children, 00906 ExprManager* em) { 00907 if (em == NULL) { 00908 if (op.getKind() == APPLY) em = op.getExpr().getEM(); 00909 else { 00910 DebugAssert(children.size() > 0, 00911 "Expr::Expr(Op, children): op's EM is NULL and " 00912 "no children given"); 00913 em = children[0].getEM(); 00914 } 00915 } 00916 if (op.getKind() != APPLY) { 00917 ExprNodeTmp ev(em, op.getKind(), children); 00918 d_expr = em->newExprValue(&ev); 00919 } else { 00920 ExprApplyTmp ev(em, op, children); 00921 d_expr = em->newExprValue(&ev); 00922 } 00923 d_expr->incRefcount(); 00924 } 00925 00926 inline Expr Expr::eqExpr(const Expr& right) const { 00927 return Expr(EQ, *this, right); 00928 } 00929 00930 inline Expr Expr::notExpr() const { 00931 return Expr(NOT, *this); 00932 } 00933 00934 inline Expr Expr::negate() const { 00935 return isNot() ? (*this)[0] : this->notExpr(); 00936 } 00937 00938 inline Expr Expr::andExpr(const Expr& right) const { 00939 return Expr(AND, *this, right); 00940 } 00941 00942 inline Expr andExpr(const std::vector <Expr>& children) { 00943 DebugAssert(children.size()>0 && !children[0].isNull(), 00944 "Expr::andExpr(kids)"); 00945 return Expr(AND, children); 00946 } 00947 00948 inline Expr Expr::orExpr(const Expr& right) const { 00949 return Expr(OR, *this, right); 00950 } 00951 00952 inline Expr orExpr(const std::vector <Expr>& children) { 00953 DebugAssert(children.size()>0 && !children[0].isNull(), 00954 "Expr::andExpr(kids)"); 00955 return Expr(OR, children); 00956 } 00957 00958 inline Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const { 00959 return Expr(ITE, *this, thenpart, elsepart); 00960 } 00961 00962 inline Expr Expr::iffExpr(const Expr& right) const { 00963 return Expr(IFF, *this, right); 00964 } 00965 00966 inline Expr Expr::impExpr(const Expr& right) const { 00967 return Expr(IMPLIES, *this, right); 00968 } 00969 00970 inline Expr Expr::xorExpr(const Expr& right) const { 00971 return Expr(XOR, *this, right); 00972 } 00973 00974 inline Expr Expr::skolemExpr(int i) const { 00975 return getEM()->newSkolemExpr(*this, i); 00976 } 00977 00978 inline Expr Expr::rebuild(ExprManager* em) const { 00979 return em->rebuild(*this); 00980 } 00981 00982 inline Expr::~Expr() { 00983 if(d_expr != NULL) { 00984 IF_DEBUG(FatalAssert(d_expr->d_refcount > 0, "Mis-handled the ref. counting");) 00985 if (--(d_expr->d_refcount) == 0) d_expr->d_em->gc(d_expr); 00986 } 00987 } 00988 00989 inline size_t Expr::hash(const Expr& e) { return e.getEM()->hash(e); } 00990 00991 ///////////////////////////////////////////////////////////////////////////// 00992 // Read-only (const) methods // 00993 ///////////////////////////////////////////////////////////////////////////// 00994 00995 inline size_t Expr::hash() const { return getEM()->hash(*this); } 00996 00997 inline const ExprValue* Expr::getExprValue() const 00998 { return d_expr->getExprValue(); } 00999 01000 // Core Expression Testers 01001 01002 inline bool Expr::isVar() const { return d_expr->isVar(); } 01003 inline bool Expr::isString() const { return d_expr->isString(); } 01004 inline bool Expr::isClosure() const { return d_expr->isClosure(); } 01005 inline bool Expr::isQuantifier() const { 01006 return (isClosure() && (getKind() == FORALL || getKind() == EXISTS)); 01007 } 01008 inline bool Expr::isLambda() const { 01009 return (isClosure() && getKind() == LAMBDA); 01010 } 01011 inline bool Expr::isApply() const 01012 { DebugAssert((getKind() != APPLY || d_expr->isApply()) && 01013 (!d_expr->isApply() || getKind() == APPLY), "APPLY mismatch"); 01014 return getKind() == APPLY; } 01015 inline bool Expr::isSymbol() const { return d_expr->isSymbol(); } 01016 inline bool Expr::isTheorem() const { return d_expr->isTheorem(); } 01017 inline bool Expr::isType() const { return getEM()->isTypeKind(getOpKind()); } 01018 inline bool Expr::isTerm() const { return !getType().isBool(); } 01019 inline bool Expr::isBoolConnective() const { 01020 if (!getType().isBool()) return false; 01021 switch (getKind()) { 01022 case NOT: case AND: case OR: case IMPLIES: case IFF: case XOR: case ITE: 01023 return true; } 01024 return false; 01025 } 01026 01027 inline Unsigned Expr::getSize() const { 01028 if (d_expr->d_size == 0) { 01029 clearFlags(); 01030 const_cast<ExprValue*>(d_expr)->d_size = d_expr->getSize(); 01031 } 01032 return d_expr->d_size; 01033 } 01034 01035 //inline int Expr::getHeight() const { return d_expr->getHeight(); } 01036 //inline int Expr::getHighestKid() const { return d_expr->getHighestKid(); } 01037 01038 //inline bool Expr::hasSimpFrom() const 01039 // { return !d_expr->getSimpFrom().isNull(); } 01040 // inline const Expr& Expr::getSimpFrom() const 01041 // { return hasSimpFrom() ? d_expr->getSimpFrom() : *this; } 01042 // inline void Expr::setSimpFrom(const Expr& simpFrom) 01043 // { d_expr->setSimpFrom(simpFrom); } 01044 01045 // Leaf accessors 01046 01047 inline const std::string& Expr::getName() const { 01048 DebugAssert(!isNull(), "Expr::getName() on Null expr"); 01049 return d_expr->getName(); 01050 } 01051 01052 inline const std::string& Expr::getString() const { 01053 DebugAssert(isString(), 01054 "CVC3::Expr::getString(): not a string Expr:\n " 01055 + toString(AST_LANG)); 01056 return d_expr->getString(); 01057 } 01058 01059 inline const std::vector<Expr>& Expr::getVars() const { 01060 DebugAssert(isClosure(), 01061 "CVC3::Expr::getVars(): not a closure Expr:\n " 01062 + toString(AST_LANG)); 01063 return d_expr->getVars(); 01064 } 01065 01066 inline const Expr& Expr::getBody() const { 01067 DebugAssert(isClosure(), 01068 "CVC3::Expr::getBody(): not a closure Expr:\n " 01069 + toString(AST_LANG)); 01070 return d_expr->getBody(); 01071 } 01072 01073 inline void Expr::setTriggers(const std::vector< std::vector<Expr> >& triggers) const { 01074 DebugAssert(isClosure(), 01075 "CVC3::Expr::setTriggers(): not a closure Expr:\n " 01076 + toString(AST_LANG)); 01077 d_expr->setTriggers(triggers); 01078 } 01079 01080 inline void Expr::setTriggers(const std::vector<Expr>& triggers) const { 01081 DebugAssert(isClosure(), 01082 "CVC3::Expr::setTriggers(): not a closure Expr:\n " 01083 + toString(AST_LANG)); 01084 std::vector<std::vector<Expr> > patternvv; 01085 for(std::vector<Expr>::const_iterator i = triggers.begin(); i != triggers.end(); ++i ) { 01086 std::vector<Expr> patternv; 01087 patternv.push_back(*i); 01088 patternvv.push_back(patternv); 01089 } 01090 d_expr->setTriggers(patternvv); 01091 } 01092 01093 inline void Expr::setTrigger(const Expr& trigger) const { 01094 DebugAssert(isClosure(), 01095 "CVC3::Expr::setTrigger(): not a closure Expr:\n " 01096 + toString(AST_LANG)); 01097 std::vector<std::vector<Expr> > patternvv; 01098 std::vector<Expr> patternv; 01099 patternv.push_back(trigger); 01100 patternvv.push_back(patternv); 01101 setTriggers(patternvv); 01102 } 01103 01104 inline void Expr::setMultiTrigger(const std::vector<Expr>& multiTrigger) const { 01105 DebugAssert(isClosure(), 01106 "CVC3::Expr::setTrigger(): not a closure Expr:\n " 01107 + toString(AST_LANG)); 01108 std::vector<std::vector<Expr> > patternvv; 01109 patternvv.push_back(multiTrigger); 01110 setTriggers(patternvv); 01111 } 01112 01113 inline const std::vector<std::vector<Expr> >& Expr::getTriggers() const { //by yeting 01114 DebugAssert(isClosure(), 01115 "CVC3::Expr::getTrigs(): not a closure Expr:\n " 01116 + toString(AST_LANG)); 01117 return d_expr->getTriggers(); 01118 } 01119 01120 inline const Expr& Expr::getExistential() const { 01121 DebugAssert(isSkolem(), 01122 "CVC3::Expr::getExistential() not a skolem variable"); 01123 return d_expr->getExistential(); 01124 } 01125 inline int Expr::getBoundIndex() const { 01126 DebugAssert(isSkolem(), 01127 "CVC3::Expr::getBoundIndex() not a skolem variable"); 01128 return d_expr->getBoundIndex(); 01129 } 01130 01131 01132 inline const Rational& Expr::getRational() const { 01133 DebugAssert(isRational(), 01134 "CVC3::Expr::getRational(): not a rational Expr:\n " 01135 + toString(AST_LANG)); 01136 return d_expr->getRational(); 01137 } 01138 01139 inline const Theorem& Expr::getTheorem() const { 01140 DebugAssert(isTheorem(), 01141 "CVC3::Expr::getTheorem(): not a Theorem Expr:\n " 01142 + toString(AST_LANG)); 01143 return d_expr->getTheorem(); 01144 } 01145 01146 inline const std::string& Expr::getUid() const { 01147 DebugAssert(getKind() == BOUND_VAR, 01148 "CVC3::Expr::getUid(): not a BOUND_VAR Expr:\n " 01149 + toString(AST_LANG)); 01150 return d_expr->getUid(); 01151 } 01152 01153 inline ExprManager* Expr::getEM() const { 01154 DebugAssert(d_expr != NULL, 01155 "CVC3::Expr:getEM: on Null Expr (not initialized)"); 01156 return d_expr->d_em; 01157 } 01158 01159 inline const std::vector<Expr>& Expr::getKids() const { 01160 DebugAssert(d_expr != NULL, "Expr::getKids on Null Expr"); 01161 if(isNull()) return getEM()->getEmptyVector(); 01162 else return d_expr->getKids(); 01163 } 01164 01165 inline int Expr::getKind() const { 01166 if(d_expr == NULL) return NULL_KIND; // FIXME: invent a better Null kind 01167 return d_expr->d_kind; 01168 } 01169 01170 inline ExprIndex Expr::getIndex() const { return d_expr->d_index; } 01171 01172 inline bool Expr::hasLastIndex() const 01173 { return d_expr->d_em->lastIndex() == getIndex(); } 01174 01175 inline Op Expr::mkOp() const { 01176 DebugAssert(!isNull(), "Expr::mkOp() on Null expr"); 01177 return Op(*this); 01178 } 01179 01180 inline Op Expr::getOp() const { 01181 DebugAssert(!isNull(), "Expr::getOp() on Null expr"); 01182 if (isApply()) return d_expr->getOp(); 01183 DebugAssert(arity() > 0, 01184 "Expr::getOp() called on non-apply expr with no children"); 01185 return Op(getKind()); 01186 } 01187 01188 inline Expr Expr::getOpExpr() const { 01189 DebugAssert(isApply(), "getOpExpr() called on non-apply"); 01190 return getOp().getExpr(); 01191 } 01192 01193 inline int Expr::getOpKind() const { 01194 if (!isApply()) return getKind(); 01195 return getOp().getExpr().getKind(); 01196 } 01197 01198 inline int Expr::arity() const { 01199 if(isNull()) return 0; 01200 else return d_expr->arity(); 01201 } 01202 01203 inline const Expr& Expr::operator[](int i) const { 01204 DebugAssert(i < arity(), "out of bounds access"); 01205 return (d_expr->getKids())[i]; 01206 } 01207 01208 inline Expr::iterator Expr::begin() const { 01209 if (isNull() || d_expr->arity() == 0) 01210 return Expr::iterator(getEM()->getEmptyVector().begin()); 01211 else return Expr::iterator(d_expr->getKids().begin()); 01212 } 01213 01214 inline Expr::iterator Expr::end() const { 01215 if (isNull() || d_expr->arity() == 0) 01216 return Expr::iterator(getEM()->getEmptyVector().end()); 01217 else return Expr::iterator(d_expr->getKids().end()); 01218 } 01219 01220 inline bool Expr::isNull() const { 01221 return (d_expr == NULL) || (d_expr->d_kind == NULL_KIND); 01222 } 01223 01224 inline size_t Expr::getMMIndex() const { 01225 DebugAssert(!isNull(), "Expr::getMMIndex()"); 01226 return d_expr->getMMIndex(); 01227 } 01228 01229 inline bool Expr::hasFind() const { 01230 DebugAssert(!isNull(), "hasFind called on NULL Expr"); 01231 return (d_expr->d_find && !(d_expr->d_find->get().isNull())); 01232 } 01233 01234 inline const Theorem& Expr::getFind() const { 01235 DebugAssert(hasFind(), "Should only be called if find is valid"); 01236 return d_expr->d_find->get(); 01237 } 01238 01239 inline int Expr::getFindLevel() const { 01240 DebugAssert(hasFind(), "Should only be called if find is valid"); 01241 return d_expr->d_find->level(); 01242 } 01243 01244 inline const Theorem& Expr::getEqNext() const { 01245 DebugAssert(!isNull(), "getEqNext called on NULL Expr"); 01246 DebugAssert(hasFind(), "Should only be called if find is valid"); 01247 DebugAssert(d_expr->d_eqNext, "getEqNext: d_eqNext is NULL"); 01248 return d_expr->d_eqNext->get(); 01249 } 01250 01251 inline NotifyList* Expr::getNotify() const { 01252 if(isNull()) return NULL; 01253 else return d_expr->d_notifyList; 01254 } 01255 01256 inline Type Expr::getType() const { 01257 if (isNull()) return s_null; 01258 if (d_expr->d_type.isNull()) getEM()->computeType(*this); 01259 return d_expr->d_type; 01260 } 01261 01262 inline Type Expr::lookupType() const { 01263 if (isNull()) return s_null; 01264 return d_expr->d_type; 01265 } 01266 01267 inline Cardinality Expr::typeCard() const { 01268 DebugAssert(!isNull(), "typeCard called on NULL Expr"); 01269 Expr e(*this); 01270 Unsigned n; 01271 return getEM()->finiteTypeInfo(e, n, false, false); 01272 } 01273 01274 inline Expr Expr::typeEnumerateFinite(Unsigned n) const { 01275 DebugAssert(!isNull(), "typeEnumerateFinite called on NULL Expr"); 01276 Expr e(*this); 01277 Cardinality card = getEM()->finiteTypeInfo(e, n, true, false); 01278 if (card != CARD_FINITE) e = Expr(); 01279 return e; 01280 } 01281 01282 inline Unsigned Expr::typeSizeFinite() const { 01283 DebugAssert(!isNull(), "typeCard called on NULL Expr"); 01284 Expr e(*this); 01285 Unsigned n; 01286 Cardinality card = getEM()->finiteTypeInfo(e, n, false, true); 01287 if (card != CARD_FINITE) n = 0; 01288 return n; 01289 } 01290 01291 inline bool Expr::validSimpCache() const { 01292 return d_expr->d_simpCacheTag == getEM()->getSimpCacheTag(); 01293 } 01294 01295 inline const Theorem& Expr::getSimpCache() const { 01296 return d_expr->d_simpCache; 01297 } 01298 01299 inline bool Expr::isValidType() const { 01300 return d_expr->d_dynamicFlags.get(VALID_TYPE); 01301 } 01302 01303 inline bool Expr::validIsAtomicFlag() const { 01304 return d_expr->d_dynamicFlags.get(VALID_IS_ATOMIC); 01305 } 01306 01307 inline bool Expr::validTerminalsConstFlag() const { 01308 return d_expr->d_dynamicFlags.get(VALID_TERMINALS_CONST); 01309 } 01310 01311 inline bool Expr::getIsAtomicFlag() const { 01312 return d_expr->d_dynamicFlags.get(IS_ATOMIC); 01313 } 01314 01315 inline bool Expr::getTerminalsConstFlag() const { 01316 return d_expr->d_dynamicFlags.get(TERMINALS_CONST); 01317 } 01318 01319 inline bool Expr::isRewriteNormal() const { 01320 return d_expr->d_dynamicFlags.get(REWRITE_NORMAL); 01321 } 01322 01323 inline bool Expr::isFinite() const { 01324 return d_expr->d_dynamicFlags.get(IS_FINITE); 01325 } 01326 01327 inline bool Expr::isWellFounded() const { 01328 return d_expr->d_dynamicFlags.get(WELL_FOUNDED); 01329 } 01330 01331 inline bool Expr::computeTransClosure() const { 01332 return d_expr->d_dynamicFlags.get(COMPUTE_TRANS_CLOSURE); 01333 } 01334 01335 inline bool Expr::containsBoundVar() const { 01336 return d_expr->d_dynamicFlags.get(CONTAINS_BOUND_VAR); 01337 } 01338 01339 inline bool Expr::usesCC() const { 01340 return d_expr->d_dynamicFlags.get(USES_CC); 01341 } 01342 01343 inline bool Expr::notArrayNormalized() const { 01344 return d_expr->d_dynamicFlags.get(NOT_ARRAY_NORMALIZED); 01345 } 01346 01347 inline bool Expr::isImpliedLiteral() const { 01348 return d_expr->d_dynamicFlags.get(IMPLIED_LITERAL); 01349 } 01350 01351 inline bool Expr::isUserAssumption() const { 01352 return d_expr->d_dynamicFlags.get(IS_USER_ASSUMPTION); 01353 } 01354 01355 inline bool Expr::inUserAssumption() const { 01356 return d_expr->d_dynamicFlags.get(IN_USER_ASSUMPTION); 01357 } 01358 01359 inline bool Expr::isIntAssumption() const { 01360 return d_expr->d_dynamicFlags.get(IS_INT_ASSUMPTION); 01361 } 01362 01363 inline bool Expr::isJustified() const { 01364 return d_expr->d_dynamicFlags.get(IS_JUSTIFIED); 01365 } 01366 01367 inline bool Expr::isTranslated() const { 01368 return d_expr->d_dynamicFlags.get(IS_TRANSLATED); 01369 } 01370 01371 inline bool Expr::isUserRegisteredAtom() const { 01372 return d_expr->d_dynamicFlags.get(IS_USER_REGISTERED_ATOM); 01373 } 01374 01375 inline bool Expr::isRegisteredAtom() const { 01376 return d_expr->d_dynamicFlags.get(IS_REGISTERED_ATOM); 01377 } 01378 01379 inline bool Expr::isSelected() const { 01380 return d_expr->d_dynamicFlags.get(IS_SELECTED); 01381 } 01382 01383 inline bool Expr::isStoredPredicate() const { 01384 return d_expr->d_dynamicFlags.get(IS_STORED_PREDICATE); 01385 } 01386 01387 inline bool Expr::getFlag() const { 01388 DebugAssert(!isNull(), "Expr::getFlag() on Null Expr"); 01389 return (d_expr->d_flag == getEM()->getFlag()); 01390 } 01391 01392 inline void Expr::setFlag() const { 01393 DebugAssert(!isNull(), "Expr::setFlag() on Null Expr"); 01394 d_expr->d_flag = getEM()->getFlag(); 01395 } 01396 01397 inline void Expr::clearFlags() const { 01398 DebugAssert(!isNull(), "Expr::clearFlags() on Null Expr"); 01399 getEM()->clearFlags(); 01400 } 01401 01402 inline void Expr::setFind(const Theorem& e) const { 01403 DebugAssert(!isNull(), "Expr::setFind() on Null expr"); 01404 DebugAssert(e.getLHS() == *this, "bad call to setFind"); 01405 if (d_expr->d_find) d_expr->d_find->set(e); 01406 else { 01407 CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e); 01408 d_expr->d_find = tmp; 01409 IF_DEBUG(tmp->setName("CDO[Expr.find]");) 01410 } 01411 } 01412 01413 inline void Expr::setEqNext(const Theorem& e) const { 01414 DebugAssert(!isNull(), "Expr::setEqNext() on Null expr"); 01415 DebugAssert(e.getLHS() == *this, "bad call to setEqNext"); 01416 if (d_expr->d_eqNext) d_expr->d_eqNext->set(e); 01417 else { 01418 CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e); 01419 d_expr->d_eqNext = tmp; 01420 IF_DEBUG(tmp->setName("CDO[Expr.eqNext]");) 01421 } 01422 } 01423 01424 inline void Expr::setType(const Type& t) const { 01425 DebugAssert(!isNull(), "Expr::setType() on Null expr"); 01426 d_expr->d_type = t; 01427 } 01428 01429 inline void Expr::setSimpCache(const Theorem& e) const { 01430 DebugAssert(!isNull(), "Expr::setSimpCache() on Null expr"); 01431 d_expr->d_simpCache = e; 01432 d_expr->d_simpCacheTag = getEM()->getSimpCacheTag(); 01433 } 01434 01435 inline void Expr::setValidType() const { 01436 DebugAssert(!isNull(), "Expr::setValidType() on Null expr"); 01437 d_expr->d_dynamicFlags.set(VALID_TYPE, 0); 01438 } 01439 01440 inline void Expr::setIsAtomicFlag(bool value) const { 01441 DebugAssert(!isNull(), "Expr::setIsAtomicFlag() on Null expr"); 01442 d_expr->d_dynamicFlags.set(VALID_IS_ATOMIC, 0); 01443 if (value) d_expr->d_dynamicFlags.set(IS_ATOMIC, 0); 01444 else d_expr->d_dynamicFlags.clear(IS_ATOMIC, 0); 01445 } 01446 01447 inline void Expr::setTerminalsConstFlag(bool value) const { 01448 DebugAssert(!isNull(), "Expr::setTerminalsConstFlag() on Null expr"); 01449 d_expr->d_dynamicFlags.set(VALID_TERMINALS_CONST, 0); 01450 if (value) d_expr->d_dynamicFlags.set(TERMINALS_CONST, 0); 01451 else d_expr->d_dynamicFlags.clear(TERMINALS_CONST, 0); 01452 } 01453 01454 inline void Expr::setRewriteNormal() const { 01455 DebugAssert(!isNull(), "Expr::setRewriteNormal() on Null expr"); 01456 TRACE("setRewriteNormal", "setRewriteNormal(", *this, ")"); 01457 d_expr->d_dynamicFlags.set(REWRITE_NORMAL, 0); 01458 } 01459 01460 inline void Expr::setFinite() const { 01461 DebugAssert(!isNull(), "Expr::setFinite() on Null expr"); 01462 d_expr->d_dynamicFlags.set(IS_FINITE, 0); 01463 } 01464 01465 inline void Expr::setWellFounded() const { 01466 DebugAssert(!isNull(), "Expr::setWellFounded() on Null expr"); 01467 d_expr->d_dynamicFlags.set(WELL_FOUNDED, 0); 01468 } 01469 01470 inline void Expr::setComputeTransClosure() const { 01471 DebugAssert(!isNull(), "Expr::setComputeTransClosure() on Null expr"); 01472 d_expr->d_dynamicFlags.set(COMPUTE_TRANS_CLOSURE, 0); 01473 } 01474 01475 inline void Expr::setContainsBoundVar() const { 01476 DebugAssert(!isNull(), "Expr::setContainsBoundVar() on Null expr"); 01477 d_expr->d_dynamicFlags.set(CONTAINS_BOUND_VAR, 0); 01478 } 01479 01480 inline void Expr::setUsesCC() const { 01481 DebugAssert(!isNull(), "Expr::setUsesCC() on Null expr"); 01482 d_expr->d_dynamicFlags.set(USES_CC, 0); 01483 } 01484 01485 inline void Expr::setNotArrayNormalized() const { 01486 DebugAssert(!isNull(), "Expr::setContainsBoundVar() on Null expr"); 01487 d_expr->d_dynamicFlags.set(NOT_ARRAY_NORMALIZED); 01488 } 01489 01490 inline void Expr::setImpliedLiteral() const { 01491 DebugAssert(!isNull(), "Expr::setImpliedLiteral() on Null expr"); 01492 d_expr->d_dynamicFlags.set(IMPLIED_LITERAL); 01493 } 01494 01495 inline void Expr::setUserAssumption(int scope) const { 01496 DebugAssert(!isNull(), "Expr::setUserAssumption() on Null expr"); 01497 d_expr->d_dynamicFlags.set(IS_USER_ASSUMPTION, scope); 01498 } 01499 01500 inline void Expr::setInUserAssumption(int scope) const { 01501 DebugAssert(!isNull(), "Expr::setInUserAssumption() on Null expr"); 01502 d_expr->d_dynamicFlags.set(IN_USER_ASSUMPTION, scope); 01503 } 01504 01505 inline void Expr::setIntAssumption() const { 01506 DebugAssert(!isNull(), "Expr::setIntAssumption() on Null expr"); 01507 d_expr->d_dynamicFlags.set(IS_INT_ASSUMPTION); 01508 } 01509 01510 inline void Expr::setJustified() const { 01511 DebugAssert(!isNull(), "Expr::setJustified() on Null expr"); 01512 d_expr->d_dynamicFlags.set(IS_JUSTIFIED); 01513 } 01514 01515 inline void Expr::setTranslated(int scope) const { 01516 DebugAssert(!isNull(), "Expr::setTranslated() on Null expr"); 01517 d_expr->d_dynamicFlags.set(IS_TRANSLATED, scope); 01518 } 01519 01520 inline void Expr::setUserRegisteredAtom() const { 01521 DebugAssert(!isNull(), "Expr::setUserRegisteredAtom() on Null expr"); 01522 d_expr->d_dynamicFlags.set(IS_USER_REGISTERED_ATOM); 01523 } 01524 01525 inline void Expr::setRegisteredAtom() const { 01526 DebugAssert(!isNull(), "Expr::setUserRegisteredAtom() on Null expr"); 01527 d_expr->d_dynamicFlags.set(IS_REGISTERED_ATOM); 01528 } 01529 01530 inline void Expr::setSelected() const { 01531 DebugAssert(!isNull(), "Expr::setSelected() on Null expr"); 01532 d_expr->d_dynamicFlags.set(IS_SELECTED); 01533 } 01534 01535 inline void Expr::setStoredPredicate() const { 01536 DebugAssert(!isNull(), "Expr::setStoredPredicate() on Null expr"); 01537 d_expr->d_dynamicFlags.set(IS_STORED_PREDICATE); 01538 } 01539 01540 inline void Expr::clearRewriteNormal() const { 01541 DebugAssert(!isNull(), "Expr::clearRewriteNormal() on Null expr"); 01542 d_expr->d_dynamicFlags.clear(REWRITE_NORMAL, 0); 01543 } 01544 01545 inline bool Expr::hasSig() const { 01546 return (!isNull() 01547 && d_expr->getSig() != NULL 01548 && !(d_expr->getSig()->get().isNull())); 01549 } 01550 01551 inline bool Expr::hasRep() const { 01552 return (!isNull() 01553 && d_expr->getRep() != NULL 01554 && !(d_expr->getRep()->get().isNull())); 01555 } 01556 01557 inline const Theorem& Expr::getSig() const { 01558 static Theorem nullThm; 01559 DebugAssert(!isNull(), "Expr::getSig() on Null expr"); 01560 if(d_expr->getSig() != NULL) 01561 return d_expr->getSig()->get(); 01562 else 01563 return nullThm; 01564 } 01565 01566 inline const Theorem& Expr::getRep() const { 01567 static Theorem nullThm; 01568 DebugAssert(!isNull(), "Expr::getRep() on Null expr"); 01569 if(d_expr->getRep() != NULL) 01570 return d_expr->getRep()->get(); 01571 else 01572 return nullThm; 01573 } 01574 01575 inline void Expr::setSig(const Theorem& e) const { 01576 DebugAssert(!isNull(), "Expr::setSig() on Null expr"); 01577 CDO<Theorem>* sig = d_expr->getSig(); 01578 if(sig != NULL) sig->set(e); 01579 else { 01580 CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e); 01581 d_expr->setSig(tmp); 01582 IF_DEBUG(tmp->setName("CDO[Expr.sig] in "+toString());) 01583 } 01584 } 01585 01586 inline void Expr::setRep(const Theorem& e) const { 01587 DebugAssert(!isNull(), "Expr::setRep() on Null expr"); 01588 CDO<Theorem>* rep = d_expr->getRep(); 01589 if(rep != NULL) rep->set(e); 01590 else { 01591 CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e); 01592 d_expr->setRep(tmp); 01593 IF_DEBUG(tmp->setName("CDO[Expr.rep] in "+toString());) 01594 } 01595 } 01596 01597 inline bool operator==(const Expr& e1, const Expr& e2) { 01598 // Comparing pointers (equal expressions are always shared) 01599 return e1.d_expr == e2.d_expr; 01600 } 01601 01602 inline bool operator!=(const Expr& e1, const Expr& e2) 01603 { return !(e1 == e2); } 01604 01605 // compare() is defined in expr.cpp 01606 01607 inline bool operator<(const Expr& e1, const Expr& e2) 01608 { return compare(e1,e2) < 0; } 01609 inline bool operator<=(const Expr& e1, const Expr& e2) 01610 { return compare(e1,e2) <= 0; } 01611 inline bool operator>(const Expr& e1, const Expr& e2) 01612 { return compare(e1,e2) > 0; } 01613 inline bool operator>=(const Expr& e1, const Expr& e2) 01614 { return compare(e1,e2) >= 0; } 01615 01616 } // end of namespace CVC3 01617 01618 #endif