CVC3
2.4.1
|
Data structure of expressions in CVC3. More...
#include <expr.h>
Classes | |
class | iterator |
Public Member Functions | |
Expr () | |
Default constructor creates the Null Expr. More... | |
Expr (const Expr &e) | |
Copy constructor and assignment (copy the pointer and take care of the refcount) More... | |
Expr & | operator= (const Expr &e) |
Assignment operator: take care of the refcounting and GC. More... | |
Expr (const Op &op, const Expr &child) | |
Expr (const Op &op, const Expr &child0, const Expr &child1) | |
Expr (const Op &op, const Expr &child0, const Expr &child1, const Expr &child2) | |
Expr (const Op &op, const Expr &child0, const Expr &child1, const Expr &child2, const Expr &child3) | |
Expr (const Op &op, const std::vector< Expr > &children, ExprManager *em=NULL) | |
~Expr () | |
Destructor. More... | |
Expr | eqExpr (const Expr &right) const |
Expr | notExpr () const |
Expr | negate () const |
Expr | andExpr (const Expr &right) const |
Expr | orExpr (const Expr &right) const |
Expr | iteExpr (const Expr &thenpart, const Expr &elsepart) const |
Expr | iffExpr (const Expr &right) const |
Expr | impExpr (const Expr &right) const |
Expr | xorExpr (const Expr &right) const |
Expr | skolemExpr (int i) const |
Create a Skolem constant for the i'th variable of an existential (*this) More... | |
Expr | rebuild (ExprManager *em) const |
Create a Boolean variable out of the expression. More... | |
Expr | substExpr (const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const |
Expr | substExpr (const ExprHashMap< Expr > &oldToNew) const |
Expr | substExprQuant (const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const |
Expr | substExprQuant (const ExprHashMap< Expr > &oldToNew) const |
Expr | operator! () const |
Expr | operator&& (const Expr &right) const |
Expr | operator|| (const Expr &right) const |
size_t | hash () const |
bool | isFalse () const |
bool | isTrue () const |
bool | isBoolConst () const |
bool | isVar () const |
bool | isBoundVar () const |
bool | isString () const |
bool | isClosure () const |
bool | isQuantifier () const |
bool | isLambda () const |
bool | isApply () const |
bool | isSymbol () const |
bool | isTheorem () const |
bool | isConstant () const |
bool | isRawList () const |
bool | isType () const |
Expr represents a type. More... | |
const ExprValue * | getExprValue () const |
Provide access to ExprValue for client subclasses of ExprValue only More... | |
bool | isTerm () const |
Test if e is a term (as opposed to a predicate/formula) More... | |
bool | isAtomic () const |
Test if e is atomic. More... | |
bool | isAtomicFormula () const |
Test if e is an atomic formula. More... | |
bool | isAbsAtomicFormula () const |
An abstract atomic formua is an atomic formula or a quantified formula. More... | |
bool | isLiteral () const |
Test if e is a literal. More... | |
bool | isAbsLiteral () const |
Test if e is an abstract literal. More... | |
bool | isBoolConnective () const |
A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool) More... | |
bool | isPropAtom () const |
True iff expr is not a Bool connective. More... | |
bool | isPropLiteral () const |
PropAtom or negation of PropAtom. More... | |
bool | containsTermITE () const |
Return whether Expr contains a non-bool type ITE as a sub-term. More... | |
bool | isEq () const |
bool | isNot () const |
bool | isAnd () const |
bool | isOr () const |
bool | isITE () const |
bool | isIff () const |
bool | isImpl () const |
bool | isXor () const |
bool | isForall () const |
bool | isExists () const |
bool | isRational () const |
bool | isSkolem () const |
const std::string & | getName () const |
const std::string & | getUid () const |
For BOUND_VAR, get the UID. More... | |
const std::string & | getString () const |
const std::vector< Expr > & | getVars () const |
Get bound variables from a closure Expr. More... | |
const Expr & | getExistential () const |
Get the existential axiom expression for skolem constant. More... | |
int | getBoundIndex () const |
Get the index of the bound var that skolem constant comes from. More... | |
const Expr & | getBody () const |
Get the body of the closure Expr. More... | |
void | setTriggers (const std::vector< std::vector< Expr > > &triggers) const |
Set the triggers for a closure Expr. More... | |
void | setTriggers (const std::vector< Expr > &triggers) const |
void | setTrigger (const Expr &trigger) const |
void | setMultiTrigger (const std::vector< Expr > &multiTrigger) const |
const std::vector< std::vector < Expr > > & | getTriggers () const |
Get the manual triggers of the closure Expr. More... | |
const Rational & | getRational () const |
Get the Rational value out of RATIONAL_EXPR. More... | |
const Theorem & | getTheorem () const |
Get theorem from THEOREM_EXPR. More... | |
ExprManager * | getEM () const |
const std::vector< Expr > & | getKids () const |
int | getKind () const |
ExprIndex | getIndex () const |
bool | hasLastIndex () const |
Op | mkOp () const |
Make the expr into an operator. More... | |
Op | getOp () const |
Get operator from expression. More... | |
Expr | getOpExpr () const |
Get expression of operator (for APPLY Exprs only) More... | |
int | getOpKind () const |
Get kind of operator (for APPLY Exprs only) More... | |
int | arity () const |
const Expr & | operator[] (int i) const |
const Expr & | unnegate () const |
Remove leading NOT if any. More... | |
iterator | begin () const |
Begin iterator. More... | |
iterator | end () const |
End iterator. More... | |
bool | isNull () const |
bool | isInitialized () const |
size_t | getMMIndex () const |
Get the memory manager index (it uniquely identifies the subclass) More... | |
bool | hasFind () const |
const Theorem & | getFind () const |
int | getFindLevel () const |
const Theorem & | getEqNext () const |
NotifyList * | getNotify () const |
Type | getType () const |
Get the type. Recursively compute if necessary. More... | |
Type | lookupType () const |
Look up the current type. Do not recursively compute (i.e. may be NULL) More... | |
Cardinality | typeCard () const |
Return cardinality of type. More... | |
Expr | typeEnumerateFinite (Unsigned n) const |
Return nth (starting with 0) element in a finite type. More... | |
Unsigned | typeSizeFinite () const |
Return size of a finite type; returns 0 if size cannot be determined. More... | |
bool | validSimpCache () const |
Return true if there is a valid cached value for calling simplify on this Expr. More... | |
const Theorem & | getSimpCache () const |
bool | isValidType () const |
bool | validIsAtomicFlag () const |
bool | validTerminalsConstFlag () const |
bool | getIsAtomicFlag () const |
bool | getTerminalsConstFlag () const |
bool | isRewriteNormal () const |
bool | isFinite () const |
bool | isWellFounded () const |
bool | computeTransClosure () const |
bool | containsBoundVar () const |
bool | usesCC () const |
bool | notArrayNormalized () const |
bool | isImpliedLiteral () const |
bool | isUserAssumption () const |
bool | inUserAssumption () const |
bool | isIntAssumption () const |
bool | isJustified () const |
bool | isTranslated () const |
bool | isUserRegisteredAtom () const |
bool | isRegisteredAtom () const |
bool | isSelected () const |
bool | isStoredPredicate () const |
bool | getFlag () const |
Check if the generic flag is set. More... | |
void | setFlag () const |
Set the generic flag. More... | |
void | clearFlags () const |
Clear the generic flag in all Exprs. More... | |
std::string | toString () const |
Print the expression to a string. More... | |
std::string | toString (InputLanguage lang) const |
Print the expression to a string using the given output language. More... | |
void | print (InputLanguage lang, bool dagify=true) const |
Print the expression in the specified format. More... | |
void | print () const |
Print the expression as AST (lisp-like format) More... | |
void | printnodag () const |
Print the expression as AST without dagifying. More... | |
void | pprint () const |
Pretty-print the expression. More... | |
void | pprintnodag () const |
Pretty-print without dagifying. More... | |
ExprStream & | print (ExprStream &os) const |
Print a leaf node. More... | |
ExprStream & | printAST (ExprStream &os) const |
Print the top node and then recurse through the children */. More... | |
Expr & | indent (int n, bool permanent=false) |
Set initial indentation to n. More... | |
void | setFind (const Theorem &e) const |
Set the find attribute to e. More... | |
void | setEqNext (const Theorem &e) const |
Set the eqNext attribute to e. More... | |
void | addToNotify (Theory *i, const Expr &e) const |
Add (e,i) to the notify list of this expression. More... | |
void | setType (const Type &t) const |
Set the cached type. More... | |
void | setSimpCache (const Theorem &e) const |
void | setValidType () const |
void | setIsAtomicFlag (bool value) const |
void | setTerminalsConstFlag (bool value) const |
void | setRewriteNormal () const |
void | clearRewriteNormal () const |
void | setFinite () const |
void | setWellFounded () const |
void | setComputeTransClosure () const |
void | setContainsBoundVar () const |
void | setUsesCC () const |
void | setNotArrayNormalized () const |
void | setImpliedLiteral () const |
void | setUserAssumption (int scope=-1) const |
void | setInUserAssumption (int scope=-1) const |
void | setIntAssumption () const |
void | setJustified () const |
void | setTranslated (int scope=-1) const |
Set the translated flag for this Expr. More... | |
void | setUserRegisteredAtom () const |
Set the UserRegisteredAtom flag for this Expr. More... | |
void | setRegisteredAtom () const |
Set the RegisteredAtom flag for this Expr. More... | |
void | setSelected () const |
Set the Selected flag for this Expr. More... | |
void | setStoredPredicate () const |
Set the Stored Predicate flag for this Expr. More... | |
bool | subExprOf (const Expr &e) const |
Check if the current Expr (*this) is a subexpression of e. More... | |
Unsigned | getSize () const |
bool | hasSig () const |
bool | hasRep () const |
const Theorem & | getSig () const |
const Theorem & | getRep () const |
void | setSig (const Theorem &e) const |
void | setRep (const Theorem &e) const |
Static Public Member Functions | |
static size_t | hash (const Expr &e) |
Private Types | |
enum | StaticFlagsEnum { VALID_TYPE = 0x1, VALID_IS_ATOMIC = 0x2, IS_ATOMIC = 0x4, REWRITE_NORMAL = 0x8, IS_FINITE = 0x400, WELL_FOUNDED = 0x800, COMPUTE_TRANS_CLOSURE = 0x1000, CONTAINS_BOUND_VAR = 0x00020000, USES_CC = 0x00080000, VALID_TERMINALS_CONST = 0x00100000, TERMINALS_CONST = 0x00200000 } |
bit-masks for static flags More... | |
enum | DynamicFlagsEnum { IMPLIED_LITERAL = 0x10, IS_USER_ASSUMPTION = 0x20, IS_INT_ASSUMPTION = 0x40, IS_JUSTIFIED = 0x80, IS_TRANSLATED = 0x100, IS_USER_REGISTERED_ATOM = 0x200, IS_SELECTED = 0x2000, IS_STORED_PREDICATE = 0x4000, IS_REGISTERED_ATOM = 0x8000, IN_USER_ASSUMPTION = 0x00010000, NOT_ARRAY_NORMALIZED = 0x00040000 } |
bit-masks for dynamic flags More... | |
Private Member Functions | |
Expr (ExprValue *expr) | |
Private constructor, simply wraps around the pointer. More... | |
Expr | recursiveSubst (const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const |
Expr | recursiveQuantSubst (const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const |
std::vector< std::vector< Expr > > | substTriggers (const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const |
Private Attributes | |
ExprValue * | d_expr |
Static Private Attributes | |
static Expr | s_null |
Convenient null expr. More... | |
Friends | |
class | ExprHasher |
class | ExprManager |
class | Op |
class | ExprValue |
class | ExprNode |
class | ExprClosure |
class | ::CInterface |
class | Theorem |
CVC_DLL std::ostream & | operator<< (std::ostream &os, const Expr &e) |
int | compare (const Expr &e1, const Expr &e2) |
bool | operator== (const Expr &e1, const Expr &e2) |
bool | operator!= (const Expr &e1, const Expr &e2) |
bool | operator< (const Expr &e1, const Expr &e2) |
bool | operator<= (const Expr &e1, const Expr &e2) |
bool | operator> (const Expr &e1, const Expr &e2) |
bool | operator>= (const Expr &e1, const Expr &e2) |
Data structure of expressions in CVC3.
Class: Expr
Author: Clark Barrett
Created: Mon Nov 25 15:29:37 2002
This class is the main data structure for expressions that all other components should use. It is actually a smart pointer to the actual data holding class ExprValue and its subclasses.
Expressions are represented as DAGs with maximal sharing of subexpressions. Therefore, testing for equality is a constant time operation (simply compare the pointers).
Unused expressions are automatically garbage-collected. The use is determined by a reference counting mechanism. In particular, this means that if there is a circular dependency among expressions (e.g. an attribute points back to the expression itself), these expressions will not be garbage-collected, even if no one else is using them.
The most frequently used operations are getKind() (determining the kind of the top level node of the expression), arity() (how many children an Expr has), operator[]() for accessing a child, and various testers and methods for constructing new expressions.
In addition, a total ordering operator<() is provided. It is guaranteed to remain the same for the lifetime of the expressions (it may change, however, if the expression is garbage-collected and reborn).
|
friend |
|
friend |