1 /*****************************************************************************/
2 /*!
3 * \file expr.h
4 * \brief Definition of the API to expression package. See class Expr for details.
5 *
6 * Author: Clark Barrett
7 *
8 * Created: Tue Nov 26 00:27:40 2002
9 *
10 * <hr>
11 *
12 * License to use, copy, modify, sell and/or distribute this software
13 * and its documentation for any purpose is hereby granted without
14 * royalty, subject to the terms and conditions defined in the \ref
15 * LICENSE file provided with this distribution.
16 *
17 * <hr>
18 *
19 */
20 /*****************************************************************************/
21
22 #ifndef _cvc3__expr_h_
23 #define _cvc3__expr_h_
24
25 #include <stdlib.h>
26 #include <sstream>
27 #include <set>
28 #include <functional>
29 #include <iterator>
30 #include <map>
31
32 #include "os.h"
33 #include "compat_hash_map.h"
34 #include "compat_hash_set.h"
35 #include "rational.h"
36 #include "kinds.h"
37 #include "cdo.h"
38 #include "cdflags.h"
39 #include "lang.h"
40 #include "memory_manager.h"
41
42 class CInterface;
43
44 namespace CVC3 {
45
46 class NotifyList;
47 class Theory;
48 class Op;
49 class Type;
50 class Theorem;
51
52 template<class Data>
53 class ExprHashMap;
54
55 class ExprManager;
56 // Internal data-holding classes
57 class ExprValue;
58 class ExprNode;
59 // Printing
60 class ExprStream;
61
62 //! Type ID of each ExprValue subclass.
63 /*! It is defined in expr.h, so that ExprManager can use it before loading
64 expr_value.h */
65 typedef enum {
66 EXPR_VALUE,
67 EXPR_NODE,
68 EXPR_APPLY, //!< Application of functions and predicates
69 EXPR_STRING,
70 EXPR_RATIONAL,
71 EXPR_SKOLEM,
72 EXPR_UCONST,
73 EXPR_SYMBOL,
74 EXPR_BOUND_VAR,
75 EXPR_CLOSURE,
76 EXPR_VALUE_TYPE_LAST // The end of list; don't assign it to any subclass
77 } ExprValueType;
78
79 //! Enum for cardinality of types
80 typedef enum {
81 CARD_FINITE,
82 CARD_INFINITE,
83 CARD_UNKNOWN
84 } Cardinality;
85
86 //! Expression index type
87 typedef long unsigned ExprIndex;
88
89 /**************************************************************************/
90 /*! \defgroup ExprPkg Expression Package
91 * \ingroup BuildingBlocks
92 */
93 /**************************************************************************/
94 /*! \defgroup Expr_SmartPointer Smart Pointer Functionality in Expr
95 * \ingroup ExprPkg
96 */
97 /**************************************************************************/
98
99 /**************************************************************************/
100 //! Data structure of expressions in CVC3
101 /*! \ingroup ExprPkg
102 * Class: Expr <br>
103 * Author: Clark Barrett <br>
104 * Created: Mon Nov 25 15:29:37 2002
105 *
106 * This class is the main data structure for expressions that all
107 * other components should use. It is actually a <em>smart
108 * pointer</em> to the actual data holding class ExprValue and its
109 * subclasses.
110 *
111 * Expressions are represented as DAGs with maximal sharing of
112 * subexpressions. Therefore, testing for equality is a constant time
113 * operation (simply compare the pointers).
114 *
115 * Unused expressions are automatically garbage-collected. The use is
116 * determined by a reference counting mechanism. In particular, this
117 * means that if there is a circular dependency among expressions
118 * (e.g. an attribute points back to the expression itself), these
119 * expressions will not be garbage-collected, even if no one else is
120 * using them.
121 *
122 * The most frequently used operations are getKind() (determining the
123 * kind of the top level node of the expression), arity() (how many
124 * children an Expr has), operator[]() for accessing a child, and
125 * various testers and methods for constructing new expressions.
126 *
127 * In addition, a total ordering operator<() is provided. It is
128 * guaranteed to remain the same for the lifetime of the expressions
129 * (it may change, however, if the expression is garbage-collected and
130 * reborn).
131 */
132 /**************************************************************************/
133 class CVC_DLL Expr {
134 friend class ExprHasher;
135 friend class ExprManager;
136 friend class Op;
137 friend class ExprValue;
138 friend class ExprNode;
139 friend class ExprClosure;
140 friend class ::CInterface;
141 friend class Theorem;
142
143 /*! \addtogroup ExprPkg
144 * @{
145 */
146 //! bit-masks for static flags
147 typedef enum {
148 //! Whether is valid TYPE expr
149 VALID_TYPE = 0x1,
150 //! Whether IS_ATOMIC flag is valid (initialized)
151 VALID_IS_ATOMIC = 0x2,
152 //! Whether the expression is an atomic term or formula
153 IS_ATOMIC = 0x4,
154 //! Expression is the result of a "normal" (idempotent) rewrite
155 REWRITE_NORMAL = 0x8,
156 //! Finite type
157 IS_FINITE = 0x400,
158 //! Well-founded (used in datatypes)
159 WELL_FOUNDED = 0x800,
160 //! Compute transitive closure (for binary uninterpreted predicates)
161 COMPUTE_TRANS_CLOSURE = 0x1000,
162 //! Whether expr contains a bounded variable (for quantifier instantiation)
163 CONTAINS_BOUND_VAR = 0x00020000,
164 //! Whether expr uses CC algorithm that relies on not simplifying an expr that has a find
165 USES_CC = 0x00080000,
166 //! Whether TERMINALS_CONST flag is valid (initialized)
167 VALID_TERMINALS_CONST = 0x00100000,
168 //! Whether expr contains only numerical constants at all possible ite terminals
169 TERMINALS_CONST = 0x00200000
170 } StaticFlagsEnum;
171
172 //! bit-masks for dynamic flags
173 // TODO: Registered flags instead of hard-wired
174 typedef enum {
175 //! Whether expr has been added as an implied literal
176 IMPLIED_LITERAL = 0x10,
177 IS_USER_ASSUMPTION = 0x20,
178 IS_INT_ASSUMPTION = 0x40,
179 IS_JUSTIFIED = 0x80,
180 IS_TRANSLATED = 0x100,
181 IS_USER_REGISTERED_ATOM = 0x200,
182 IS_SELECTED = 0x2000,
183 IS_STORED_PREDICATE = 0x4000,
184 IS_REGISTERED_ATOM = 0x8000,
185 IN_USER_ASSUMPTION = 0x00010000,
186 //! Whether expr is normalized (in array theory)
187 NOT_ARRAY_NORMALIZED = 0x00040000
188 } DynamicFlagsEnum;
189
190 //! Convenient null expr
191 static Expr s_null;
192
193 /////////////////////////////////////////////////////////////////////////////
194 // Private Dynamic Data //
195 /////////////////////////////////////////////////////////////////////////////
196 //! The value. This is the only data member in this class.
197 ExprValue* d_expr;
198
199 /////////////////////////////////////////////////////////////////////////////
200 // Private methods //
201 /////////////////////////////////////////////////////////////////////////////
202
203 //! Private constructor, simply wraps around the pointer
204 Expr(ExprValue* expr);
205
206 Expr recursiveSubst(const ExprHashMap<Expr>& subst,
207 ExprHashMap<Expr>& visited) const;
208
209 Expr recursiveQuantSubst(const ExprHashMap<Expr>& subst,
210 ExprHashMap<Expr>& visited) const;
211
212 std::vector<std::vector<Expr> > substTriggers(const ExprHashMap<Expr> & subst,
213 ExprHashMap<Expr> & visited) const;
214 public:
215 /////////////////////////////////////////////////////////////////////////////
216 // Public Classes and Types //
217 /////////////////////////////////////////////////////////////////////////////
218
219 /////////////////////////////////////////////////////////////////////////////
220 /*!
221 * Class: Expr::iterator
222 * Author: Sergey Berezin
223 * Created: Fri Dec 6 15:38:51 2002
224 * Description: STL-like iterator API to the Expr's children.
225 * IMPORTANT: the iterator will not be valid after the originating
226 * expression is destroyed.
227 */
228 /////////////////////////////////////////////////////////////////////////////
229 class CVC_DLL iterator
230 : public std::iterator<std::input_iterator_tag,Expr,ptrdiff_t>
231 {
232 friend class Expr;
233 private:
234 std::vector<Expr>::const_iterator d_it;
235 // Private constructors (used by Expr only)
236 //
237 //! Construct an iterator out of the vector's iterator
iterator(std::vector<Expr>::const_iterator it)238 iterator(std::vector<Expr>::const_iterator it): d_it(it) { }
239 // Public methods
240 public:
241 //! Default constructor
iterator()242 iterator() { }
243 // Copy constructor and operator= are defined by C++, that's good enough
244
245 //! Equality
246 bool operator==(const iterator& i) const {
247 return d_it == i.d_it;
248 }
249 //! Disequality
250 bool operator!=(const iterator& i) const { return !(*this == i); }
251 //! Dereference operator
252 const Expr& operator*() const { return *d_it; }
253 //! Dereference and member access
254 const Expr* operator->() const { return &(operator*()); }
255 //! Prefix increment
256 iterator& operator++() {
257 ++d_it;
258 return *this;
259 }
260 /*! @brief Postfix increment requires a Proxy object to hold the
261 * intermediate value for dereferencing */
262 class Proxy {
263 const Expr* d_e;
264 public:
Proxy(const Expr & e)265 Proxy(const Expr& e) : d_e(&e) { }
266 Expr operator*() { return *d_e; }
267 };
268 //! Postfix increment
269 /*! \return Proxy with the old Expr.
270 *
271 * Now, an expression like *i++ will return the current *i, and
272 * then advance the iterator. However, don't try to use Proxy for
273 * anything else.
274 */
275 Proxy operator++(int) {
276 Proxy e(*(*this));
277 ++(*this);
278 return e;
279 }
280 }; // end of class Expr::iterator
281
282 /////////////////////////////////////////////////////////////////////////////
283 // Constructors //
284 /////////////////////////////////////////////////////////////////////////////
285
286 //! Default constructor creates the Null Expr
Expr()287 Expr(): d_expr(NULL) {}
288
289 /*! @brief Copy constructor and assignment (copy the pointer and take care
290 of the refcount) */
291 Expr(const Expr& e);
292 //! Assignment operator: take care of the refcounting and GC
293 Expr& operator=(const Expr& e);
294
295 // These constructors grab the ExprManager from the Op or the first
296 // child. The operator and all children must belong to the same
297 // ExprManager.
298 Expr(const Op& op, const Expr& child);
299 Expr(const Op& op, const Expr& child0, const Expr& child1);
300 Expr(const Op& op, const Expr& child0, const Expr& child1,
301 const Expr& child2);
302 Expr(const Op& op, const Expr& child0, const Expr& child1,
303 const Expr& child2, const Expr& child3);
304 Expr(const Op& op, const std::vector<Expr>& children,
305 ExprManager* em = NULL);
306
307 //! Destructor
308 ~Expr();
309
310 // Compound expression constructors
311 Expr eqExpr(const Expr& right) const;
312 Expr notExpr() const;
313 Expr negate() const; // avoid double-negatives
314 Expr andExpr(const Expr& right) const;
315 Expr orExpr(const Expr& right) const;
316 Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
317 Expr iffExpr(const Expr& right) const;
318 Expr impExpr(const Expr& right) const;
319 Expr xorExpr(const Expr& right) const;
320 //! Create a Skolem constant for the i'th variable of an existential (*this)
321 Expr skolemExpr(int i) const;
322 //! Create a Boolean variable out of the expression
323 // Expr boolVarExpr() const;
324 //! Rebuild Expr with a new ExprManager
325 Expr rebuild(ExprManager* em) const;
326 // Expr newForall(const Expr& e);
327 // Expr newExists(const Expr& e);
328 Expr substExpr(const std::vector<Expr>& oldTerms,
329 const std::vector<Expr>& newTerms) const;
330 Expr substExpr(const ExprHashMap<Expr>& oldToNew) const;
331
332 // by yeting, a special subst function for TheoryQuant
333 Expr substExprQuant(const std::vector<Expr>& oldTerms,
334 const std::vector<Expr>& newTerms) const;
335 Expr substExprQuant(const ExprHashMap<Expr>& oldToNew) const;
336
337 Expr operator!() const { return notExpr(); }
338 Expr operator&&(const Expr& right) const { return andExpr(right); }
339 Expr operator||(const Expr& right) const { return orExpr(right); }
340
341 /////////////////////////////////////////////////////////////////////////////
342 // Public Static Methods //
343 /////////////////////////////////////////////////////////////////////////////
344
345 static size_t hash(const Expr& e);
346
347 /////////////////////////////////////////////////////////////////////////////
348 // Read-only (const) methods //
349 /////////////////////////////////////////////////////////////////////////////
350
351 size_t hash() const;
352
353 // Core expression testers
354
isFalse()355 bool isFalse() const { return getKind() == FALSE_EXPR; }
isTrue()356 bool isTrue() const { return getKind() == TRUE_EXPR; }
isBoolConst()357 bool isBoolConst() const { return isFalse() || isTrue(); }
358 bool isVar() const;
isBoundVar()359 bool isBoundVar() const { return getKind() == BOUND_VAR; }
360 bool isString() const;
361 bool isClosure() const;
362 bool isQuantifier() const;
363 bool isLambda() const;
364 bool isApply() const;
365 bool isSymbol() const;
366 bool isTheorem() const;
367
isConstant()368 bool isConstant() const { return getOpKind() <= MAX_CONST; }
369
isRawList()370 bool isRawList() const {return getKind() == RAW_LIST;}
371
372 //! Expr represents a type
373 bool isType() const;
374 /*
375 bool isRecord() const;
376 bool isRecordAccess() const;
377 bool isTupleAccess() const;
378 */
379 //! Provide access to ExprValue for client subclasses of ExprValue *only*
380 /*@ Calling getExprValue on an Expr with a built-in ExprValue class will
381 * cause an error */
382 const ExprValue* getExprValue() const;
383
384 //! Test if e is a term (as opposed to a predicate/formula)
385 bool isTerm() const;
386 //! Test if e is atomic
387 /*! An atomic expression is TRUE or FALSE or one that does not
388 * contain a formula (including not being a formula itself).
389 * \sa isAtomicFormula */
390 bool isAtomic() const;
391 //! Test if e is an atomic formula
392 /*! An atomic formula is TRUE or FALSE or an application of a predicate
393 (possibly 0-ary) which does not properly contain any formula. For
394 instance, the formula "x = IF f THEN y ELSE z ENDIF" is not an atomic
395 formula, since it contains the condition "f", which is a formula. */
396 bool isAtomicFormula() const;
397 //! An abstract atomic formua is an atomic formula or a quantified formula
isAbsAtomicFormula()398 bool isAbsAtomicFormula() const
399 { return isQuantifier() || isAtomicFormula(); }
400 //! Test if e is a literal
401 /*! A literal is an atomic formula, or its negation.
402 \sa isAtomicFormula */
isLiteral()403 bool isLiteral() const
404 { return (isAtomicFormula() || (isNot() && (*this)[0].isAtomicFormula())); }
405 //! Test if e is an abstract literal
isAbsLiteral()406 bool isAbsLiteral() const
407 { return (isAbsAtomicFormula() || (isNot() && (*this)[0].isAbsAtomicFormula())); }
408 //! A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool)
409 bool isBoolConnective() const;
410 //! True iff expr is not a Bool connective
isPropAtom()411 bool isPropAtom() const { return !isTerm() && !isBoolConnective(); }
412 //! PropAtom or negation of PropAtom
isPropLiteral()413 bool isPropLiteral() const
414 { return (isNot() && (*this)[0].isPropAtom()) || isPropAtom(); }
415 //! Return whether Expr contains a non-bool type ITE as a sub-term
416 bool containsTermITE() const;
417
418
isEq()419 bool isEq() const { return getKind() == EQ; }
isNot()420 bool isNot() const { return getKind() == NOT; }
isAnd()421 bool isAnd() const { return getKind() == AND; }
isOr()422 bool isOr() const { return getKind() == OR; }
isITE()423 bool isITE() const { return getKind() == ITE; }
isIff()424 bool isIff() const { return getKind() == IFF; }
isImpl()425 bool isImpl() const { return getKind() == IMPLIES; }
isXor()426 bool isXor() const { return getKind() == XOR;}
427
isForall()428 bool isForall() const { return getKind() == FORALL; }
isExists()429 bool isExists() const { return getKind() == EXISTS; }
430
isRational()431 bool isRational() const { return getKind() == RATIONAL_EXPR; }
isSkolem()432 bool isSkolem() const { return getKind() == SKOLEM_VAR;}
433
434 // Leaf accessors - these functions must only be called one expressions of
435 // the appropriate kind.
436
437 // For UCONST and BOUND_VAR Expr's
438 const std::string& getName() const;
439 //! For BOUND_VAR, get the UID
440 const std::string& getUid() const;
441
442 // For STRING_EXPR's
443 const std::string& getString() const;
444 //! Get bound variables from a closure Expr
445 const std::vector<Expr>& getVars() const;
446 //! Get the existential axiom expression for skolem constant
447 const Expr& getExistential() const;
448 //! Get the index of the bound var that skolem constant comes from
449 int getBoundIndex() const;
450
451 //! Get the body of the closure Expr
452 const Expr& getBody() const;
453
454 //! Set the triggers for a closure Expr
455 void setTriggers(const std::vector<std::vector<Expr> >& triggers) const;
456 void setTriggers(const std::vector<Expr>& triggers) const;
457 void setTrigger(const Expr& trigger) const;
458 void setMultiTrigger(const std::vector<Expr>& multiTrigger) const;
459
460 //! Get the manual triggers of the closure Expr
461 const std::vector<std::vector<Expr> >& getTriggers() const; //by yeting
462
463 //! Get the Rational value out of RATIONAL_EXPR
464 const Rational& getRational() const;
465 //! Get theorem from THEOREM_EXPR
466 const Theorem& getTheorem() const;
467
468 // Get the expression manager. The expression must be non-null.
469 ExprManager *getEM() const;
470
471 // Return a ref to the vector of children.
472 const std::vector<Expr>& getKids() const;
473
474 // Get the kind of this expr.
475 int getKind() const;
476
477 // Get the index field
478 ExprIndex getIndex() const;
479
480 // True if this is the most recently created expression
481 bool hasLastIndex() const;
482
483 //! Make the expr into an operator
484 Op mkOp() const;
485
486 //! Get operator from expression
487 Op getOp() const;
488
489 //! Get expression of operator (for APPLY Exprs only)
490 Expr getOpExpr() const;
491
492 //! Get kind of operator (for APPLY Exprs only)
493 int getOpKind() const;
494
495 // Return the number of children. Note, that an application of a
496 // user-defined function has the arity of that function (the number
497 // of arguments), and the function name itself is part of the
498 // operator.
499 int arity() const;
500
501 // Return the ith child. As with arity, it's also the ith argument
502 // in function application.
503 const Expr& operator[](int i) const;
504
505 //! Remove leading NOT if any
unnegate()506 const Expr& unnegate() const { return isNot() ? (*this)[0] : *this; }
507
508 //! Begin iterator
509 iterator begin() const;
510
511 //! End iterator
512 iterator end() const;
513
514 // Check if Expr is Null
515 bool isNull() const;
516
517 // Check if Expr is not Null
isInitialized()518 bool isInitialized() const { return d_expr != NULL; }
519 //! Get the memory manager index (it uniquely identifies the subclass)
520 size_t getMMIndex() const;
521
522 // Attributes
523
524 // True if the find attribute has been set to something other than NULL.
525 bool hasFind() const;
526
527 // Return the attached find attribute for the expr. Note that this
528 // must be called repeatedly to get the root of the union-find tree.
529 // Should only be called if hasFind is true.
530 const Theorem& getFind() const;
531 int getFindLevel() const;
532 const Theorem& getEqNext() const;
533
534 // Return the notify list
535 NotifyList* getNotify() const;
536
537 //! Get the type. Recursively compute if necessary
538 Type getType() const;
539 //! Look up the current type. Do not recursively compute (i.e. may be NULL)
540 Type lookupType() const;
541 //! Return cardinality of type
542 Cardinality typeCard() const;
543 //! Return nth (starting with 0) element in a finite type
544 /*! Returns NULL Expr if unable to compute nth element
545 */
546 Expr typeEnumerateFinite(Unsigned n) const;
547 //! Return size of a finite type; returns 0 if size cannot be determined
548 Unsigned typeSizeFinite() const;
549
550 /*! @brief Return true if there is a valid cached value for calling
551 simplify on this Expr. */
552 bool validSimpCache() const;
553
554 // Get the cached Simplify of this Expr.
555 const Theorem& getSimpCache() const;
556
557 // Return true if valid type flag is set for Expr
558 bool isValidType() const;
559
560 // Return true if there is a valid flag for whether Expr is atomic
561 bool validIsAtomicFlag() const;
562
563 // Return true if there is a valid flag for whether terminals are const
564 bool validTerminalsConstFlag() const;
565
566 // Get the isAtomic flag
567 bool getIsAtomicFlag() const;
568
569 // Get the TerminalsConst flag
570 bool getTerminalsConstFlag() const;
571
572 // Get the RewriteNormal flag
573 bool isRewriteNormal() const;
574
575 // Get the isFinite flag
576 bool isFinite() const;
577
578 // Get the WellFounded flag
579 bool isWellFounded() const;
580
581 // Get the ComputeTransClosure flag
582 bool computeTransClosure() const;
583
584 // Get the ContainsBoundVar flag
585 bool containsBoundVar() const;
586
587 // Get the usesCC flag
588 bool usesCC() const;
589
590 // Get the notArrayNormalized flag
591 bool notArrayNormalized() const;
592
593 // Get the ImpliedLiteral flag
594 bool isImpliedLiteral() const;
595
596 // Get the UserAssumption flag
597 bool isUserAssumption() const;
598
599 // Get the inUserAssumption flag
600 bool inUserAssumption() const;
601
602 // Get the IntAssumption flag
603 bool isIntAssumption() const;
604
605 // Get the Justified flag
606 bool isJustified() const;
607
608 // Get the Translated flag
609 bool isTranslated() const;
610
611 // Get the UserRegisteredAtom flag
612 bool isUserRegisteredAtom() const;
613
614 // Get the RegisteredAtom flag
615 bool isRegisteredAtom() const;
616
617 // Get the Selected flag
618 bool isSelected() const;
619
620 // Get the Stored Predicate flag
621 bool isStoredPredicate() const;
622
623 //! Check if the generic flag is set
624 bool getFlag() const;
625 //! Set the generic flag
626 void setFlag() const;
627 //! Clear the generic flag in all Exprs
628 void clearFlags() const;
629
630 // Printing functions
631
632 //! Print the expression to a string
633 std::string toString() const;
634 //! Print the expression to a string using the given output language
635 std::string toString(InputLanguage lang) const;
636 //! Print the expression in the specified format
637 void print(InputLanguage lang, bool dagify = true) const;
638
639 //! Print the expression as AST (lisp-like format)
print()640 void print() const { print(AST_LANG); }
641 //! Print the expression as AST without dagifying
642 void printnodag() const;
643
644 //! Pretty-print the expression
645 void pprint() const;
646 //! Pretty-print without dagifying
647 void pprintnodag() const;
648
649 //! Print a leaf node
650 /*@ The top node is pretty-printed if it is a basic leaf type;
651 * otherwise, just the kind is printed. Should only be called on expressions
652 * with no children. */
653 ExprStream& print(ExprStream& os) const;
654 //! Print the top node and then recurse through the children */
655 /*@ The top node is printed as an AST with all the information, including
656 * "hidden" Exprs that are part of the ExprValue */
657 ExprStream& printAST(ExprStream& os) const;
658 //! Set initial indentation to n.
659 /*! The indentation will be reset to default unless the second
660 argument is true.
661 \return reference to itself, so one can write `os << e.indent(5)'
662 */
663 Expr& indent(int n, bool permanent = false);
664
665 /////////////////////////////////////////////////////////////////////////////
666 // Other Public methods //
667 /////////////////////////////////////////////////////////////////////////////
668
669 // Attributes
670
671 //! Set the find attribute to e
672 void setFind(const Theorem& e) const;
673
674 //! Set the eqNext attribute to e
675 void setEqNext(const Theorem& e) const;
676
677 //! Add (e,i) to the notify list of this expression
678 void addToNotify(Theory* i, const Expr& e) const;
679
680 //! Set the cached type
681 void setType(const Type& t) const;
682
683 // Cache the result of a call to Simplify on this Expr
684 void setSimpCache(const Theorem& e) const;
685
686 // Set the valid type flag for this Expr
687 void setValidType() const;
688
689 // Set the isAtomicFlag for this Expr
690 void setIsAtomicFlag(bool value) const;
691
692 // Set the TerminalsConst flag for this Expr
693 void setTerminalsConstFlag(bool value) const;
694
695 // Set or clear the RewriteNormal flag
696 void setRewriteNormal() const;
697 void clearRewriteNormal() const;
698
699 // Set the isFinite flag
700 void setFinite() const;
701
702 // Set the WellFounded flag
703 void setWellFounded() const;
704
705 // Set the ComputeTransClosure flag
706 void setComputeTransClosure() const;
707
708 // Set the ContainsBoundVar flag
709 void setContainsBoundVar() const;
710
711 // Set the UsesCC flag
712 void setUsesCC() const;
713
714 // Set the notArrayNormalized flag
715 void setNotArrayNormalized() const;
716
717 // Set the impliedLiteral flag for this Expr
718 void setImpliedLiteral() const;
719
720 // Set the user assumption flag for this Expr
721 void setUserAssumption(int scope = -1) const;
722
723 // Set the in user assumption flag for this Expr
724 void setInUserAssumption(int scope = -1) const;
725
726 // Set the internal assumption flag for this Expr
727 void setIntAssumption() const;
728
729 // Set the justified flag for this Expr
730 void setJustified() const;
731
732 //! Set the translated flag for this Expr
733 void setTranslated(int scope = -1) const;
734
735 //! Set the UserRegisteredAtom flag for this Expr
736 void setUserRegisteredAtom() const;
737
738 //! Set the RegisteredAtom flag for this Expr
739 void setRegisteredAtom() const;
740
741 //! Set the Selected flag for this Expr
742 void setSelected() const;
743
744 //! Set the Stored Predicate flag for this Expr
745 void setStoredPredicate() const;
746
747 //! Check if the current Expr (*this) is a subexpression of e
748 bool subExprOf(const Expr& e) const;
749 // Returns the maximum number of Boolean expressions on a path from
750 // this to a leaf, including this.
751
752 inline Unsigned getSize() const;
753
754 // inline int getHeight() const;
755
756 // // Returns the index of the highest kid.
757 // inline int getHighestKid() const;
758
759 // // Gets/sets an expression that this expression was simplified from
760 // // (see newRWTheorem). This is the equivalent of SVC's Sigx.
761 // inline bool hasSimpFrom() const;
762 // inline const Expr& getSimpFrom() const;
763 // inline void setSimpFrom(const Expr& simpFrom);
764
765 // Attributes for uninterpreted function symbols.
766 bool hasSig() const;
767 bool hasRep() const;
768 const Theorem& getSig() const;
769 const Theorem& getRep() const;
770 void setSig(const Theorem& e) const;
771 void setRep(const Theorem& e) const;
772
773 /////////////////////////////////////////////////////////////////////////////
774 // Friend methods //
775 /////////////////////////////////////////////////////////////////////////////
776
777 friend CVC_DLL std::ostream& operator<<(std::ostream& os, const Expr& e);
778
779 // The master method which defines some fixed total ordering on all
780 // Exprs. If e1 < e2, e1==e2, and e1 > e2, it returns -1, 0, 1
781 // respectively. A Null expr is always "smaller" than any other
782 // expr, but is equal to itself.
783 friend int compare(const Expr& e1, const Expr& e2);
784
785 friend bool operator==(const Expr& e1, const Expr& e2);
786 friend bool operator!=(const Expr& e1, const Expr& e2);
787
788 friend bool operator<(const Expr& e1, const Expr& e2);
789 friend bool operator<=(const Expr& e1, const Expr& e2);
790 friend bool operator>(const Expr& e1, const Expr& e2);
791 friend bool operator>=(const Expr& e1, const Expr& e2);
792
793 /*!@}*/ // end of group Expr
794
795 }; // end of class Expr
796
797 } // end of namespace CVC3
798
799 // Include expr_value.h here. We cannot include it earlier, since it
800 // needs the definition of class Expr. See comments in expr_value.h.
801 #ifndef DOXYGEN
802 #include "expr_op.h"
803 #include "expr_manager.h"
804 #endif
805 namespace CVC3 {
806
Expr(ExprValue * expr)807 inline Expr::Expr(ExprValue* expr) : d_expr(expr) { d_expr->incRefcount(); }
808
Expr(const Expr & e)809 inline Expr::Expr(const Expr& e) : d_expr(e.d_expr) {
810 if (d_expr != NULL) d_expr->incRefcount();
811 }
812
813 inline Expr& Expr::operator=(const Expr& e) {
814 if(&e == this) return *this; // Self-assignment
815 ExprValue* tmp = e.d_expr;
816 if(tmp == d_expr) return *this;
817 if (tmp == NULL) {
818 d_expr->decRefcount();
819 }
820 else {
821 tmp->incRefcount();
822 if(d_expr != NULL) {
823 d_expr->decRefcount();
824 }
825 }
826 d_expr = tmp;
827 return *this;
828 }
829
Expr(const Op & op,const Expr & child)830 inline Expr::Expr(const Op& op, const Expr& child) {
831 ExprManager* em = child.getEM();
832 if (op.getKind() != APPLY) {
833 ExprNode ev(em, op.getKind());
834 std::vector<Expr>& kids = ev.getKids1();
835 kids.push_back(child);
836 d_expr = em->newExprValue(&ev);
837 } else {
838 ExprApply ev(em, op);
839 std::vector<Expr>& kids = ev.getKids1();
840 kids.push_back(child);
841 d_expr = em->newExprValue(&ev);
842 }
843 d_expr->incRefcount();
844 }
845
Expr(const Op & op,const Expr & child0,const Expr & child1)846 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1) {
847 ExprManager* em = child0.getEM();
848 if (op.getKind() != APPLY) {
849 ExprNode ev(em, op.getKind());
850 std::vector<Expr>& kids = ev.getKids1();
851 kids.push_back(child0);
852 kids.push_back(child1);
853 d_expr = em->newExprValue(&ev);
854 } else {
855 ExprApply ev(em, op);
856 std::vector<Expr>& kids = ev.getKids1();
857 kids.push_back(child0);
858 kids.push_back(child1);
859 d_expr = em->newExprValue(&ev);
860 }
861 d_expr->incRefcount();
862 }
863
Expr(const Op & op,const Expr & child0,const Expr & child1,const Expr & child2)864 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1,
865 const Expr& child2) {
866 ExprManager* em = child0.getEM();
867 if (op.getKind() != APPLY) {
868 ExprNode ev(em, op.getKind());
869 std::vector<Expr>& kids = ev.getKids1();
870 kids.push_back(child0);
871 kids.push_back(child1);
872 kids.push_back(child2);
873 d_expr = em->newExprValue(&ev);
874 } else {
875 ExprApply ev(em, op);
876 std::vector<Expr>& kids = ev.getKids1();
877 kids.push_back(child0);
878 kids.push_back(child1);
879 kids.push_back(child2);
880 d_expr = em->newExprValue(&ev);
881 }
882 d_expr->incRefcount();
883 }
884
Expr(const Op & op,const Expr & child0,const Expr & child1,const Expr & child2,const Expr & child3)885 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1,
886 const Expr& child2, const Expr& child3) {
887 ExprManager* em = child0.getEM();
888 if (op.getKind() != APPLY) {
889 ExprNode ev(em, op.getKind());
890 std::vector<Expr>& kids = ev.getKids1();
891 kids.push_back(child0);
892 kids.push_back(child1);
893 kids.push_back(child2);
894 kids.push_back(child3);
895 d_expr = em->newExprValue(&ev);
896 } else {
897 ExprApply ev(em, op);
898 std::vector<Expr>& kids = ev.getKids1();
899 kids.push_back(child0);
900 kids.push_back(child1);
901 kids.push_back(child2);
902 kids.push_back(child3);
903 d_expr = em->newExprValue(&ev);
904 }
905 d_expr->incRefcount();
906 }
907
Expr(const Op & op,const std::vector<Expr> & children,ExprManager * em)908 inline Expr::Expr(const Op& op, const std::vector<Expr>& children,
909 ExprManager* em) {
910 if (em == NULL) {
911 if (op.getKind() == APPLY) em = op.getExpr().getEM();
912 else {
913 DebugAssert(children.size() > 0,
914 "Expr::Expr(Op, children): op's EM is NULL and "
915 "no children given");
916 em = children[0].getEM();
917 }
918 }
919 if (op.getKind() != APPLY) {
920 ExprNodeTmp ev(em, op.getKind(), children);
921 d_expr = em->newExprValue(&ev);
922 } else {
923 ExprApplyTmp ev(em, op, children);
924 d_expr = em->newExprValue(&ev);
925 }
926 d_expr->incRefcount();
927 }
928
eqExpr(const Expr & right)929 inline Expr Expr::eqExpr(const Expr& right) const {
930 return Expr(EQ, *this, right);
931 }
932
notExpr()933 inline Expr Expr::notExpr() const {
934 return Expr(NOT, *this);
935 }
936
negate()937 inline Expr Expr::negate() const {
938 return isNot() ? (*this)[0] : this->notExpr();
939 }
940
andExpr(const Expr & right)941 inline Expr Expr::andExpr(const Expr& right) const {
942 return Expr(AND, *this, right);
943 }
944
andExpr(const std::vector<Expr> & children)945 inline Expr andExpr(const std::vector <Expr>& children) {
946 DebugAssert(children.size()>0 && !children[0].isNull(),
947 "Expr::andExpr(kids)");
948 return Expr(AND, children);
949 }
950
orExpr(const Expr & right)951 inline Expr Expr::orExpr(const Expr& right) const {
952 return Expr(OR, *this, right);
953 }
954
orExpr(const std::vector<Expr> & children)955 inline Expr orExpr(const std::vector <Expr>& children) {
956 DebugAssert(children.size()>0 && !children[0].isNull(),
957 "Expr::andExpr(kids)");
958 return Expr(OR, children);
959 }
960
iteExpr(const Expr & thenpart,const Expr & elsepart)961 inline Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
962 return Expr(ITE, *this, thenpart, elsepart);
963 }
964
iffExpr(const Expr & right)965 inline Expr Expr::iffExpr(const Expr& right) const {
966 return Expr(IFF, *this, right);
967 }
968
impExpr(const Expr & right)969 inline Expr Expr::impExpr(const Expr& right) const {
970 return Expr(IMPLIES, *this, right);
971 }
972
xorExpr(const Expr & right)973 inline Expr Expr::xorExpr(const Expr& right) const {
974 return Expr(XOR, *this, right);
975 }
976
skolemExpr(int i)977 inline Expr Expr::skolemExpr(int i) const {
978 return getEM()->newSkolemExpr(*this, i);
979 }
980
rebuild(ExprManager * em)981 inline Expr Expr::rebuild(ExprManager* em) const {
982 return em->rebuild(*this);
983 }
984
~Expr()985 inline Expr::~Expr() {
986 if(d_expr != NULL) {
987 IF_DEBUG(FatalAssert(d_expr->d_refcount > 0, "Mis-handled the ref. counting");)
988 if (--(d_expr->d_refcount) == 0) d_expr->d_em->gc(d_expr);
989 }
990 }
991
hash(const Expr & e)992 inline size_t Expr::hash(const Expr& e) { return e.getEM()->hash(e); }
993
994 /////////////////////////////////////////////////////////////////////////////
995 // Read-only (const) methods //
996 /////////////////////////////////////////////////////////////////////////////
997
hash()998 inline size_t Expr::hash() const { return getEM()->hash(*this); }
999
getExprValue()1000 inline const ExprValue* Expr::getExprValue() const
1001 { return d_expr->getExprValue(); }
1002
1003 // Core Expression Testers
1004
isVar()1005 inline bool Expr::isVar() const { return d_expr->isVar(); }
isString()1006 inline bool Expr::isString() const { return d_expr->isString(); }
isClosure()1007 inline bool Expr::isClosure() const { return d_expr->isClosure(); }
isQuantifier()1008 inline bool Expr::isQuantifier() const {
1009 return (isClosure() && (getKind() == FORALL || getKind() == EXISTS));
1010 }
isLambda()1011 inline bool Expr::isLambda() const {
1012 return (isClosure() && getKind() == LAMBDA);
1013 }
isApply()1014 inline bool Expr::isApply() const
1015 { DebugAssert((getKind() != APPLY || d_expr->isApply()) &&
1016 (!d_expr->isApply() || getKind() == APPLY), "APPLY mismatch");
1017 return getKind() == APPLY; }
isSymbol()1018 inline bool Expr::isSymbol() const { return d_expr->isSymbol(); }
isTheorem()1019 inline bool Expr::isTheorem() const { return d_expr->isTheorem(); }
isType()1020 inline bool Expr::isType() const { return getEM()->isTypeKind(getOpKind()); }
isTerm()1021 inline bool Expr::isTerm() const { return !getType().isBool(); }
isBoolConnective()1022 inline bool Expr::isBoolConnective() const {
1023 if (!getType().isBool()) return false;
1024 switch (getKind()) {
1025 case NOT: case AND: case OR: case IMPLIES: case IFF: case XOR: case ITE:
1026 return true; }
1027 return false;
1028 }
1029
getSize()1030 inline Unsigned Expr::getSize() const {
1031 if (d_expr->d_size == 0) {
1032 clearFlags();
1033 const_cast<ExprValue*>(d_expr)->d_size = d_expr->getSize();
1034 }
1035 return d_expr->d_size;
1036 }
1037
1038 //inline int Expr::getHeight() const { return d_expr->getHeight(); }
1039 //inline int Expr::getHighestKid() const { return d_expr->getHighestKid(); }
1040
1041 //inline bool Expr::hasSimpFrom() const
1042 // { return !d_expr->getSimpFrom().isNull(); }
1043 // inline const Expr& Expr::getSimpFrom() const
1044 // { return hasSimpFrom() ? d_expr->getSimpFrom() : *this; }
1045 // inline void Expr::setSimpFrom(const Expr& simpFrom)
1046 // { d_expr->setSimpFrom(simpFrom); }
1047
1048 // Leaf accessors
1049
getName()1050 inline const std::string& Expr::getName() const {
1051 DebugAssert(!isNull(), "Expr::getName() on Null expr");
1052 return d_expr->getName();
1053 }
1054
getString()1055 inline const std::string& Expr::getString() const {
1056 DebugAssert(isString(),
1057 "CVC3::Expr::getString(): not a string Expr:\n "
1058 + toString(AST_LANG));
1059 return d_expr->getString();
1060 }
1061
getVars()1062 inline const std::vector<Expr>& Expr::getVars() const {
1063 DebugAssert(isClosure(),
1064 "CVC3::Expr::getVars(): not a closure Expr:\n "
1065 + toString(AST_LANG));
1066 return d_expr->getVars();
1067 }
1068
getBody()1069 inline const Expr& Expr::getBody() const {
1070 DebugAssert(isClosure(),
1071 "CVC3::Expr::getBody(): not a closure Expr:\n "
1072 + toString(AST_LANG));
1073 return d_expr->getBody();
1074 }
1075
setTriggers(const std::vector<std::vector<Expr>> & triggers)1076 inline void Expr::setTriggers(const std::vector< std::vector<Expr> >& triggers) const {
1077 DebugAssert(isClosure(),
1078 "CVC3::Expr::setTriggers(): not a closure Expr:\n "
1079 + toString(AST_LANG));
1080 d_expr->setTriggers(triggers);
1081 }
1082
setTriggers(const std::vector<Expr> & triggers)1083 inline void Expr::setTriggers(const std::vector<Expr>& triggers) const {
1084 DebugAssert(isClosure(),
1085 "CVC3::Expr::setTriggers(): not a closure Expr:\n "
1086 + toString(AST_LANG));
1087 std::vector<std::vector<Expr> > patternvv;
1088 for(std::vector<Expr>::const_iterator i = triggers.begin(); i != triggers.end(); ++i ) {
1089 std::vector<Expr> patternv;
1090 patternv.push_back(*i);
1091 patternvv.push_back(patternv);
1092 }
1093 d_expr->setTriggers(patternvv);
1094 }
1095
setTrigger(const Expr & trigger)1096 inline void Expr::setTrigger(const Expr& trigger) const {
1097 DebugAssert(isClosure(),
1098 "CVC3::Expr::setTrigger(): not a closure Expr:\n "
1099 + toString(AST_LANG));
1100 std::vector<std::vector<Expr> > patternvv;
1101 std::vector<Expr> patternv;
1102 patternv.push_back(trigger);
1103 patternvv.push_back(patternv);
1104 setTriggers(patternvv);
1105 }
1106
setMultiTrigger(const std::vector<Expr> & multiTrigger)1107 inline void Expr::setMultiTrigger(const std::vector<Expr>& multiTrigger) const {
1108 DebugAssert(isClosure(),
1109 "CVC3::Expr::setTrigger(): not a closure Expr:\n "
1110 + toString(AST_LANG));
1111 std::vector<std::vector<Expr> > patternvv;
1112 patternvv.push_back(multiTrigger);
1113 setTriggers(patternvv);
1114 }
1115
getTriggers()1116 inline const std::vector<std::vector<Expr> >& Expr::getTriggers() const { //by yeting
1117 DebugAssert(isClosure(),
1118 "CVC3::Expr::getTrigs(): not a closure Expr:\n "
1119 + toString(AST_LANG));
1120 return d_expr->getTriggers();
1121 }
1122
getExistential()1123 inline const Expr& Expr::getExistential() const {
1124 DebugAssert(isSkolem(),
1125 "CVC3::Expr::getExistential() not a skolem variable");
1126 return d_expr->getExistential();
1127 }
getBoundIndex()1128 inline int Expr::getBoundIndex() const {
1129 DebugAssert(isSkolem(),
1130 "CVC3::Expr::getBoundIndex() not a skolem variable");
1131 return d_expr->getBoundIndex();
1132 }
1133
1134
getRational()1135 inline const Rational& Expr::getRational() const {
1136 DebugAssert(isRational(),
1137 "CVC3::Expr::getRational(): not a rational Expr:\n "
1138 + toString(AST_LANG));
1139 return d_expr->getRational();
1140 }
1141
getTheorem()1142 inline const Theorem& Expr::getTheorem() const {
1143 DebugAssert(isTheorem(),
1144 "CVC3::Expr::getTheorem(): not a Theorem Expr:\n "
1145 + toString(AST_LANG));
1146 return d_expr->getTheorem();
1147 }
1148
getUid()1149 inline const std::string& Expr::getUid() const {
1150 DebugAssert(getKind() == BOUND_VAR,
1151 "CVC3::Expr::getUid(): not a BOUND_VAR Expr:\n "
1152 + toString(AST_LANG));
1153 return d_expr->getUid();
1154 }
1155
getEM()1156 inline ExprManager* Expr::getEM() const {
1157 DebugAssert(d_expr != NULL,
1158 "CVC3::Expr:getEM: on Null Expr (not initialized)");
1159 return d_expr->d_em;
1160 }
1161
getKids()1162 inline const std::vector<Expr>& Expr::getKids() const {
1163 DebugAssert(d_expr != NULL, "Expr::getKids on Null Expr");
1164 if(isNull()) return getEM()->getEmptyVector();
1165 else return d_expr->getKids();
1166 }
1167
getKind()1168 inline int Expr::getKind() const {
1169 if(d_expr == NULL) return NULL_KIND; // FIXME: invent a better Null kind
1170 return d_expr->d_kind;
1171 }
1172
getIndex()1173 inline ExprIndex Expr::getIndex() const { return d_expr->d_index; }
1174
hasLastIndex()1175 inline bool Expr::hasLastIndex() const
1176 { return d_expr->d_em->lastIndex() == getIndex(); }
1177
mkOp()1178 inline Op Expr::mkOp() const {
1179 DebugAssert(!isNull(), "Expr::mkOp() on Null expr");
1180 return Op(*this);
1181 }
1182
getOp()1183 inline Op Expr::getOp() const {
1184 DebugAssert(!isNull(), "Expr::getOp() on Null expr");
1185 if (isApply()) return d_expr->getOp();
1186 DebugAssert(arity() > 0,
1187 "Expr::getOp() called on non-apply expr with no children");
1188 return Op(getKind());
1189 }
1190
getOpExpr()1191 inline Expr Expr::getOpExpr() const {
1192 DebugAssert(isApply(), "getOpExpr() called on non-apply");
1193 return getOp().getExpr();
1194 }
1195
getOpKind()1196 inline int Expr::getOpKind() const {
1197 if (!isApply()) return getKind();
1198 return getOp().getExpr().getKind();
1199 }
1200
arity()1201 inline int Expr::arity() const {
1202 if(isNull()) return 0;
1203 else return d_expr->arity();
1204 }
1205
1206 inline const Expr& Expr::operator[](int i) const {
1207 DebugAssert(i < arity(), "out of bounds access");
1208 return (d_expr->getKids())[i];
1209 }
1210
begin()1211 inline Expr::iterator Expr::begin() const {
1212 if (isNull() || d_expr->arity() == 0)
1213 return Expr::iterator(getEM()->getEmptyVector().begin());
1214 else return Expr::iterator(d_expr->getKids().begin());
1215 }
1216
end()1217 inline Expr::iterator Expr::end() const {
1218 if (isNull() || d_expr->arity() == 0)
1219 return Expr::iterator(getEM()->getEmptyVector().end());
1220 else return Expr::iterator(d_expr->getKids().end());
1221 }
1222
isNull()1223 inline bool Expr::isNull() const {
1224 return (d_expr == NULL) || (d_expr->d_kind == NULL_KIND);
1225 }
1226
getMMIndex()1227 inline size_t Expr::getMMIndex() const {
1228 DebugAssert(!isNull(), "Expr::getMMIndex()");
1229 return d_expr->getMMIndex();
1230 }
1231
hasFind()1232 inline bool Expr::hasFind() const {
1233 DebugAssert(!isNull(), "hasFind called on NULL Expr");
1234 return (d_expr->d_find && !(d_expr->d_find->get().isNull()));
1235 }
1236
getFind()1237 inline const Theorem& Expr::getFind() const {
1238 DebugAssert(hasFind(), "Should only be called if find is valid");
1239 return d_expr->d_find->get();
1240 }
1241
getFindLevel()1242 inline int Expr::getFindLevel() const {
1243 DebugAssert(hasFind(), "Should only be called if find is valid");
1244 return d_expr->d_find->level();
1245 }
1246
getEqNext()1247 inline const Theorem& Expr::getEqNext() const {
1248 DebugAssert(!isNull(), "getEqNext called on NULL Expr");
1249 DebugAssert(hasFind(), "Should only be called if find is valid");
1250 DebugAssert(d_expr->d_eqNext, "getEqNext: d_eqNext is NULL");
1251 return d_expr->d_eqNext->get();
1252 }
1253
getNotify()1254 inline NotifyList* Expr::getNotify() const {
1255 if(isNull()) return NULL;
1256 else return d_expr->d_notifyList;
1257 }
1258
getType()1259 inline Type Expr::getType() const {
1260 if (isNull()) return s_null;
1261 if (d_expr->d_type.isNull()) getEM()->computeType(*this);
1262 return d_expr->d_type;
1263 }
1264
lookupType()1265 inline Type Expr::lookupType() const {
1266 if (isNull()) return s_null;
1267 return d_expr->d_type;
1268 }
1269
typeCard()1270 inline Cardinality Expr::typeCard() const {
1271 DebugAssert(!isNull(), "typeCard called on NULL Expr");
1272 Expr e(*this);
1273 Unsigned n;
1274 return getEM()->finiteTypeInfo(e, n, false, false);
1275 }
1276
typeEnumerateFinite(Unsigned n)1277 inline Expr Expr::typeEnumerateFinite(Unsigned n) const {
1278 DebugAssert(!isNull(), "typeEnumerateFinite called on NULL Expr");
1279 Expr e(*this);
1280 Cardinality card = getEM()->finiteTypeInfo(e, n, true, false);
1281 if (card != CARD_FINITE) e = Expr();
1282 return e;
1283 }
1284
typeSizeFinite()1285 inline Unsigned Expr::typeSizeFinite() const {
1286 DebugAssert(!isNull(), "typeCard called on NULL Expr");
1287 Expr e(*this);
1288 Unsigned n;
1289 Cardinality card = getEM()->finiteTypeInfo(e, n, false, true);
1290 if (card != CARD_FINITE) n = 0;
1291 return n;
1292 }
1293
validSimpCache()1294 inline bool Expr::validSimpCache() const {
1295 return d_expr->d_simpCacheTag == getEM()->getSimpCacheTag();
1296 }
1297
getSimpCache()1298 inline const Theorem& Expr::getSimpCache() const {
1299 return d_expr->d_simpCache;
1300 }
1301
isValidType()1302 inline bool Expr::isValidType() const {
1303 return d_expr->d_dynamicFlags.get(VALID_TYPE);
1304 }
1305
validIsAtomicFlag()1306 inline bool Expr::validIsAtomicFlag() const {
1307 return d_expr->d_dynamicFlags.get(VALID_IS_ATOMIC);
1308 }
1309
validTerminalsConstFlag()1310 inline bool Expr::validTerminalsConstFlag() const {
1311 return d_expr->d_dynamicFlags.get(VALID_TERMINALS_CONST);
1312 }
1313
getIsAtomicFlag()1314 inline bool Expr::getIsAtomicFlag() const {
1315 return d_expr->d_dynamicFlags.get(IS_ATOMIC);
1316 }
1317
getTerminalsConstFlag()1318 inline bool Expr::getTerminalsConstFlag() const {
1319 return d_expr->d_dynamicFlags.get(TERMINALS_CONST);
1320 }
1321
isRewriteNormal()1322 inline bool Expr::isRewriteNormal() const {
1323 return d_expr->d_dynamicFlags.get(REWRITE_NORMAL);
1324 }
1325
isFinite()1326 inline bool Expr::isFinite() const {
1327 return d_expr->d_dynamicFlags.get(IS_FINITE);
1328 }
1329
isWellFounded()1330 inline bool Expr::isWellFounded() const {
1331 return d_expr->d_dynamicFlags.get(WELL_FOUNDED);
1332 }
1333
computeTransClosure()1334 inline bool Expr::computeTransClosure() const {
1335 return d_expr->d_dynamicFlags.get(COMPUTE_TRANS_CLOSURE);
1336 }
1337
containsBoundVar()1338 inline bool Expr::containsBoundVar() const {
1339 return d_expr->d_dynamicFlags.get(CONTAINS_BOUND_VAR);
1340 }
1341
usesCC()1342 inline bool Expr::usesCC() const {
1343 return d_expr->d_dynamicFlags.get(USES_CC);
1344 }
1345
notArrayNormalized()1346 inline bool Expr::notArrayNormalized() const {
1347 return d_expr->d_dynamicFlags.get(NOT_ARRAY_NORMALIZED);
1348 }
1349
isImpliedLiteral()1350 inline bool Expr::isImpliedLiteral() const {
1351 return d_expr->d_dynamicFlags.get(IMPLIED_LITERAL);
1352 }
1353
isUserAssumption()1354 inline bool Expr::isUserAssumption() const {
1355 return d_expr->d_dynamicFlags.get(IS_USER_ASSUMPTION);
1356 }
1357
inUserAssumption()1358 inline bool Expr::inUserAssumption() const {
1359 return d_expr->d_dynamicFlags.get(IN_USER_ASSUMPTION);
1360 }
1361
isIntAssumption()1362 inline bool Expr::isIntAssumption() const {
1363 return d_expr->d_dynamicFlags.get(IS_INT_ASSUMPTION);
1364 }
1365
isJustified()1366 inline bool Expr::isJustified() const {
1367 return d_expr->d_dynamicFlags.get(IS_JUSTIFIED);
1368 }
1369
isTranslated()1370 inline bool Expr::isTranslated() const {
1371 return d_expr->d_dynamicFlags.get(IS_TRANSLATED);
1372 }
1373
isUserRegisteredAtom()1374 inline bool Expr::isUserRegisteredAtom() const {
1375 return d_expr->d_dynamicFlags.get(IS_USER_REGISTERED_ATOM);
1376 }
1377
isRegisteredAtom()1378 inline bool Expr::isRegisteredAtom() const {
1379 return d_expr->d_dynamicFlags.get(IS_REGISTERED_ATOM);
1380 }
1381
isSelected()1382 inline bool Expr::isSelected() const {
1383 return d_expr->d_dynamicFlags.get(IS_SELECTED);
1384 }
1385
isStoredPredicate()1386 inline bool Expr::isStoredPredicate() const {
1387 return d_expr->d_dynamicFlags.get(IS_STORED_PREDICATE);
1388 }
1389
getFlag()1390 inline bool Expr::getFlag() const {
1391 DebugAssert(!isNull(), "Expr::getFlag() on Null Expr");
1392 return (d_expr->d_flag == getEM()->getFlag());
1393 }
1394
setFlag()1395 inline void Expr::setFlag() const {
1396 DebugAssert(!isNull(), "Expr::setFlag() on Null Expr");
1397 d_expr->d_flag = getEM()->getFlag();
1398 }
1399
clearFlags()1400 inline void Expr::clearFlags() const {
1401 DebugAssert(!isNull(), "Expr::clearFlags() on Null Expr");
1402 getEM()->clearFlags();
1403 }
1404
setFind(const Theorem & e)1405 inline void Expr::setFind(const Theorem& e) const {
1406 DebugAssert(!isNull(), "Expr::setFind() on Null expr");
1407 DebugAssert(e.getLHS() == *this, "bad call to setFind");
1408 if (d_expr->d_find) d_expr->d_find->set(e);
1409 else {
1410 CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
1411 d_expr->d_find = tmp;
1412 IF_DEBUG(tmp->setName("CDO[Expr.find]");)
1413 }
1414 }
1415
setEqNext(const Theorem & e)1416 inline void Expr::setEqNext(const Theorem& e) const {
1417 DebugAssert(!isNull(), "Expr::setEqNext() on Null expr");
1418 DebugAssert(e.getLHS() == *this, "bad call to setEqNext");
1419 if (d_expr->d_eqNext) d_expr->d_eqNext->set(e);
1420 else {
1421 CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
1422 d_expr->d_eqNext = tmp;
1423 IF_DEBUG(tmp->setName("CDO[Expr.eqNext]");)
1424 }
1425 }
1426
setType(const Type & t)1427 inline void Expr::setType(const Type& t) const {
1428 DebugAssert(!isNull(), "Expr::setType() on Null expr");
1429 d_expr->d_type = t;
1430 }
1431
setSimpCache(const Theorem & e)1432 inline void Expr::setSimpCache(const Theorem& e) const {
1433 DebugAssert(!isNull(), "Expr::setSimpCache() on Null expr");
1434 d_expr->d_simpCache = e;
1435 d_expr->d_simpCacheTag = getEM()->getSimpCacheTag();
1436 }
1437
setValidType()1438 inline void Expr::setValidType() const {
1439 DebugAssert(!isNull(), "Expr::setValidType() on Null expr");
1440 d_expr->d_dynamicFlags.set(VALID_TYPE, 0);
1441 }
1442
setIsAtomicFlag(bool value)1443 inline void Expr::setIsAtomicFlag(bool value) const {
1444 DebugAssert(!isNull(), "Expr::setIsAtomicFlag() on Null expr");
1445 d_expr->d_dynamicFlags.set(VALID_IS_ATOMIC, 0);
1446 if (value) d_expr->d_dynamicFlags.set(IS_ATOMIC, 0);
1447 else d_expr->d_dynamicFlags.clear(IS_ATOMIC, 0);
1448 }
1449
setTerminalsConstFlag(bool value)1450 inline void Expr::setTerminalsConstFlag(bool value) const {
1451 DebugAssert(!isNull(), "Expr::setTerminalsConstFlag() on Null expr");
1452 d_expr->d_dynamicFlags.set(VALID_TERMINALS_CONST, 0);
1453 if (value) d_expr->d_dynamicFlags.set(TERMINALS_CONST, 0);
1454 else d_expr->d_dynamicFlags.clear(TERMINALS_CONST, 0);
1455 }
1456
setRewriteNormal()1457 inline void Expr::setRewriteNormal() const {
1458 DebugAssert(!isNull(), "Expr::setRewriteNormal() on Null expr");
1459 TRACE("setRewriteNormal", "setRewriteNormal(", *this, ")");
1460 d_expr->d_dynamicFlags.set(REWRITE_NORMAL, 0);
1461 }
1462
setFinite()1463 inline void Expr::setFinite() const {
1464 DebugAssert(!isNull(), "Expr::setFinite() on Null expr");
1465 d_expr->d_dynamicFlags.set(IS_FINITE, 0);
1466 }
1467
setWellFounded()1468 inline void Expr::setWellFounded() const {
1469 DebugAssert(!isNull(), "Expr::setWellFounded() on Null expr");
1470 d_expr->d_dynamicFlags.set(WELL_FOUNDED, 0);
1471 }
1472
setComputeTransClosure()1473 inline void Expr::setComputeTransClosure() const {
1474 DebugAssert(!isNull(), "Expr::setComputeTransClosure() on Null expr");
1475 d_expr->d_dynamicFlags.set(COMPUTE_TRANS_CLOSURE, 0);
1476 }
1477
setContainsBoundVar()1478 inline void Expr::setContainsBoundVar() const {
1479 DebugAssert(!isNull(), "Expr::setContainsBoundVar() on Null expr");
1480 d_expr->d_dynamicFlags.set(CONTAINS_BOUND_VAR, 0);
1481 }
1482
setUsesCC()1483 inline void Expr::setUsesCC() const {
1484 DebugAssert(!isNull(), "Expr::setUsesCC() on Null expr");
1485 d_expr->d_dynamicFlags.set(USES_CC, 0);
1486 }
1487
setNotArrayNormalized()1488 inline void Expr::setNotArrayNormalized() const {
1489 DebugAssert(!isNull(), "Expr::setContainsBoundVar() on Null expr");
1490 d_expr->d_dynamicFlags.set(NOT_ARRAY_NORMALIZED);
1491 }
1492
setImpliedLiteral()1493 inline void Expr::setImpliedLiteral() const {
1494 DebugAssert(!isNull(), "Expr::setImpliedLiteral() on Null expr");
1495 d_expr->d_dynamicFlags.set(IMPLIED_LITERAL);
1496 }
1497
setUserAssumption(int scope)1498 inline void Expr::setUserAssumption(int scope) const {
1499 DebugAssert(!isNull(), "Expr::setUserAssumption() on Null expr");
1500 d_expr->d_dynamicFlags.set(IS_USER_ASSUMPTION, scope);
1501 }
1502
setInUserAssumption(int scope)1503 inline void Expr::setInUserAssumption(int scope) const {
1504 DebugAssert(!isNull(), "Expr::setInUserAssumption() on Null expr");
1505 d_expr->d_dynamicFlags.set(IN_USER_ASSUMPTION, scope);
1506 }
1507
setIntAssumption()1508 inline void Expr::setIntAssumption() const {
1509 DebugAssert(!isNull(), "Expr::setIntAssumption() on Null expr");
1510 d_expr->d_dynamicFlags.set(IS_INT_ASSUMPTION);
1511 }
1512
setJustified()1513 inline void Expr::setJustified() const {
1514 DebugAssert(!isNull(), "Expr::setJustified() on Null expr");
1515 d_expr->d_dynamicFlags.set(IS_JUSTIFIED);
1516 }
1517
setTranslated(int scope)1518 inline void Expr::setTranslated(int scope) const {
1519 DebugAssert(!isNull(), "Expr::setTranslated() on Null expr");
1520 d_expr->d_dynamicFlags.set(IS_TRANSLATED, scope);
1521 }
1522
setUserRegisteredAtom()1523 inline void Expr::setUserRegisteredAtom() const {
1524 DebugAssert(!isNull(), "Expr::setUserRegisteredAtom() on Null expr");
1525 d_expr->d_dynamicFlags.set(IS_USER_REGISTERED_ATOM);
1526 }
1527
setRegisteredAtom()1528 inline void Expr::setRegisteredAtom() const {
1529 DebugAssert(!isNull(), "Expr::setUserRegisteredAtom() on Null expr");
1530 d_expr->d_dynamicFlags.set(IS_REGISTERED_ATOM);
1531 }
1532
setSelected()1533 inline void Expr::setSelected() const {
1534 DebugAssert(!isNull(), "Expr::setSelected() on Null expr");
1535 d_expr->d_dynamicFlags.set(IS_SELECTED);
1536 }
1537
setStoredPredicate()1538 inline void Expr::setStoredPredicate() const {
1539 DebugAssert(!isNull(), "Expr::setStoredPredicate() on Null expr");
1540 d_expr->d_dynamicFlags.set(IS_STORED_PREDICATE);
1541 }
1542
clearRewriteNormal()1543 inline void Expr::clearRewriteNormal() const {
1544 DebugAssert(!isNull(), "Expr::clearRewriteNormal() on Null expr");
1545 d_expr->d_dynamicFlags.clear(REWRITE_NORMAL, 0);
1546 }
1547
hasSig()1548 inline bool Expr::hasSig() const {
1549 return (!isNull()
1550 && d_expr->getSig() != NULL
1551 && !(d_expr->getSig()->get().isNull()));
1552 }
1553
hasRep()1554 inline bool Expr::hasRep() const {
1555 return (!isNull()
1556 && d_expr->getRep() != NULL
1557 && !(d_expr->getRep()->get().isNull()));
1558 }
1559
getSig()1560 inline const Theorem& Expr::getSig() const {
1561 static Theorem nullThm;
1562 DebugAssert(!isNull(), "Expr::getSig() on Null expr");
1563 if(d_expr->getSig() != NULL)
1564 return d_expr->getSig()->get();
1565 else
1566 return nullThm;
1567 }
1568
getRep()1569 inline const Theorem& Expr::getRep() const {
1570 static Theorem nullThm;
1571 DebugAssert(!isNull(), "Expr::getRep() on Null expr");
1572 if(d_expr->getRep() != NULL)
1573 return d_expr->getRep()->get();
1574 else
1575 return nullThm;
1576 }
1577
setSig(const Theorem & e)1578 inline void Expr::setSig(const Theorem& e) const {
1579 DebugAssert(!isNull(), "Expr::setSig() on Null expr");
1580 CDO<Theorem>* sig = d_expr->getSig();
1581 if(sig != NULL) sig->set(e);
1582 else {
1583 CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
1584 d_expr->setSig(tmp);
1585 IF_DEBUG(tmp->setName("CDO[Expr.sig] in "+toString());)
1586 }
1587 }
1588
setRep(const Theorem & e)1589 inline void Expr::setRep(const Theorem& e) const {
1590 DebugAssert(!isNull(), "Expr::setRep() on Null expr");
1591 CDO<Theorem>* rep = d_expr->getRep();
1592 if(rep != NULL) rep->set(e);
1593 else {
1594 CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
1595 d_expr->setRep(tmp);
1596 IF_DEBUG(tmp->setName("CDO[Expr.rep] in "+toString());)
1597 }
1598 }
1599
1600 inline bool operator==(const Expr& e1, const Expr& e2) {
1601 // Comparing pointers (equal expressions are always shared)
1602 return e1.d_expr == e2.d_expr;
1603 }
1604
1605 inline bool operator!=(const Expr& e1, const Expr& e2)
1606 { return !(e1 == e2); }
1607
1608 // compare() is defined in expr.cpp
1609
1610 inline bool operator<(const Expr& e1, const Expr& e2)
1611 { return compare(e1,e2) < 0; }
1612 inline bool operator<=(const Expr& e1, const Expr& e2)
1613 { return compare(e1,e2) <= 0; }
1614 inline bool operator>(const Expr& e1, const Expr& e2)
1615 { return compare(e1,e2) > 0; }
1616 inline bool operator>=(const Expr& e1, const Expr& e2)
1617 { return compare(e1,e2) >= 0; }
1618
1619 } // end of namespace CVC3
1620
1621 #endif
1622