22 #ifndef _cvc3__expr_h_
23 #define _cvc3__expr_h_
134 friend class ExprHasher;
140 friend class ::CInterface;
151 VALID_IS_ATOMIC = 0x2,
155 REWRITE_NORMAL = 0x8,
159 WELL_FOUNDED = 0x800,
161 COMPUTE_TRANS_CLOSURE = 0x1000,
163 CONTAINS_BOUND_VAR = 0x00020000,
165 USES_CC = 0x00080000,
167 VALID_TERMINALS_CONST = 0x00100000,
169 TERMINALS_CONST = 0x00200000
176 IMPLIED_LITERAL = 0x10,
177 IS_USER_ASSUMPTION = 0x20,
178 IS_INT_ASSUMPTION = 0x40,
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,
187 NOT_ARRAY_NORMALIZED = 0x00040000
230 :
public std::iterator<std::input_iterator_tag,Expr,ptrdiff_t>
234 std::vector<Expr>::const_iterator
d_it;
238 iterator(std::vector<Expr>::const_iterator it): d_it(it) { }
247 return d_it == i.
d_it;
303 const Expr& child2,
const Expr& child3);
304 Expr(
const Op& op,
const std::vector<Expr>& children,
312 Expr notExpr()
const;
316 Expr iteExpr(
const Expr& thenpart,
const Expr& elsepart)
const;
321 Expr skolemExpr(
int i)
const;
328 Expr substExpr(
const std::vector<Expr>& oldTerms,
329 const std::vector<Expr>& newTerms)
const;
333 Expr substExprQuant(
const std::vector<Expr>& oldTerms,
334 const std::vector<Expr>& newTerms)
const;
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;
390 bool isAtomic()
const;
396 bool isAtomicFormula()
const;
399 {
return isQuantifier() || isAtomicFormula(); }
404 {
return (isAtomicFormula() || (isNot() && (*
this)[0].isAtomicFormula())); }
407 {
return (isAbsAtomicFormula() || (isNot() && (*
this)[0].isAbsAtomicFormula())); }
409 bool isBoolConnective()
const;
411 bool isPropAtom()
const {
return !isTerm() && !isBoolConnective(); }
414 {
return (isNot() && (*
this)[0].isPropAtom()) || isPropAtom(); }
416 bool containsTermITE()
const;
419 bool isEq()
const {
return getKind() ==
EQ; }
422 bool isOr()
const {
return getKind() ==
OR; }
438 const std::string& getName()
const;
440 const std::string& getUid()
const;
443 const std::string& getString()
const;
445 const std::vector<Expr>& getVars()
const;
447 const Expr& getExistential()
const;
449 int getBoundIndex()
const;
452 const Expr& getBody()
const;
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;
461 const std::vector<std::vector<Expr> >& getTriggers()
const;
464 const Rational& getRational()
const;
466 const Theorem& getTheorem()
const;
472 const std::vector<Expr>& getKids()
const;
478 ExprIndex getIndex()
const;
481 bool hasLastIndex()
const;
490 Expr getOpExpr()
const;
493 int getOpKind()
const;
503 const Expr& operator[](
int i)
const;
509 iterator begin()
const;
512 iterator end()
const;
520 size_t getMMIndex()
const;
525 bool hasFind()
const;
530 const Theorem& getFind()
const;
531 int getFindLevel()
const;
532 const Theorem& getEqNext()
const;
538 Type getType()
const;
540 Type lookupType()
const;
552 bool validSimpCache()
const;
555 const Theorem& getSimpCache()
const;
558 bool isValidType()
const;
561 bool validIsAtomicFlag()
const;
564 bool validTerminalsConstFlag()
const;
567 bool getIsAtomicFlag()
const;
570 bool getTerminalsConstFlag()
const;
573 bool isRewriteNormal()
const;
576 bool isFinite()
const;
579 bool isWellFounded()
const;
582 bool computeTransClosure()
const;
585 bool containsBoundVar()
const;
591 bool notArrayNormalized()
const;
594 bool isImpliedLiteral()
const;
597 bool isUserAssumption()
const;
600 bool inUserAssumption()
const;
603 bool isIntAssumption()
const;
606 bool isJustified()
const;
609 bool isTranslated()
const;
612 bool isUserRegisteredAtom()
const;
615 bool isRegisteredAtom()
const;
618 bool isSelected()
const;
621 bool isStoredPredicate()
const;
624 bool getFlag()
const;
626 void setFlag()
const;
628 void clearFlags()
const;
633 std::string toString()
const;
642 void printnodag()
const;
647 void pprintnodag()
const;
663 Expr& indent(
int n,
bool permanent =
false);
672 void setFind(
const Theorem& e)
const;
675 void setEqNext(
const Theorem& e)
const;
678 void addToNotify(
Theory* i,
const Expr& e)
const;
681 void setType(
const Type& t)
const;
684 void setSimpCache(
const Theorem& e)
const;
687 void setValidType()
const;
690 void setIsAtomicFlag(
bool value)
const;
693 void setTerminalsConstFlag(
bool value)
const;
696 void setRewriteNormal()
const;
697 void clearRewriteNormal()
const;
700 void setFinite()
const;
703 void setWellFounded()
const;
706 void setComputeTransClosure()
const;
709 void setContainsBoundVar()
const;
712 void setUsesCC()
const;
715 void setNotArrayNormalized()
const;
718 void setImpliedLiteral()
const;
721 void setUserAssumption(
int scope = -1)
const;
724 void setInUserAssumption(
int scope = -1)
const;
727 void setIntAssumption()
const;
730 void setJustified()
const;
733 void setTranslated(
int scope = -1)
const;
736 void setUserRegisteredAtom()
const;
739 void setRegisteredAtom()
const;
742 void setSelected()
const;
745 void setStoredPredicate()
const;
748 bool subExprOf(
const Expr& e)
const;
770 void setSig(
const Theorem& e)
const;
771 void setRep(
const Theorem& e)
const;
814 if(&e ==
this)
return *
this;
816 if(tmp ==
d_expr)
return *
this;
834 std::vector<Expr>& kids = ev.
getKids1();
835 kids.push_back(child);
839 std::vector<Expr>& kids = ev.
getKids1();
840 kids.push_back(child);
850 std::vector<Expr>& kids = ev.
getKids1();
851 kids.push_back(child0);
852 kids.push_back(child1);
856 std::vector<Expr>& kids = ev.
getKids1();
857 kids.push_back(child0);
858 kids.push_back(child1);
865 const Expr& child2) {
869 std::vector<Expr>& kids = ev.
getKids1();
870 kids.push_back(child0);
871 kids.push_back(child1);
872 kids.push_back(child2);
876 std::vector<Expr>& kids = ev.
getKids1();
877 kids.push_back(child0);
878 kids.push_back(child1);
879 kids.push_back(child2);
886 const Expr& child2,
const Expr& child3) {
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);
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);
914 "Expr::Expr(Op, children): op's EM is NULL and "
915 "no children given");
916 em = children[0].getEM();
930 return Expr(
EQ, *
this, right);
942 return Expr(
AND, *
this, right);
946 DebugAssert(children.size()>0 && !children[0].isNull(),
947 "Expr::andExpr(kids)");
952 return Expr(
OR, *
this, right);
956 DebugAssert(children.size()>0 && !children[0].isNull(),
957 "Expr::andExpr(kids)");
958 return Expr(
OR, children);
962 return Expr(
ITE, *
this, thenpart, elsepart);
966 return Expr(
IFF, *
this, right);
974 return Expr(
XOR, *
this, right);
1023 if (!
getType().isBool())
return false;
1057 "CVC3::Expr::getString(): not a string Expr:\n "
1064 "CVC3::Expr::getVars(): not a closure Expr:\n "
1071 "CVC3::Expr::getBody(): not a closure Expr:\n "
1078 "CVC3::Expr::setTriggers(): not a closure Expr:\n "
1085 "CVC3::Expr::setTriggers(): not a closure Expr:\n "
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);
1098 "CVC3::Expr::setTrigger(): not a closure Expr:\n "
1100 std::vector<std::vector<Expr> > patternvv;
1101 std::vector<Expr> patternv;
1102 patternv.push_back(trigger);
1103 patternvv.push_back(patternv);
1109 "CVC3::Expr::setTrigger(): not a closure Expr:\n "
1111 std::vector<std::vector<Expr> > patternvv;
1112 patternvv.push_back(multiTrigger);
1118 "CVC3::Expr::getTrigs(): not a closure Expr:\n "
1125 "CVC3::Expr::getExistential() not a skolem variable");
1130 "CVC3::Expr::getBoundIndex() not a skolem variable");
1137 "CVC3::Expr::getRational(): not a rational Expr:\n "
1144 "CVC3::Expr::getTheorem(): not a Theorem Expr:\n "
1151 "CVC3::Expr::getUid(): not a BOUND_VAR Expr:\n "
1158 "CVC3::Expr:getEM: on Null Expr (not initialized)");
1187 "Expr::getOp() called on non-apply expr with no children");
1255 if(
isNull())
return NULL;
1412 IF_DEBUG(tmp->setName(
"CDO[Expr.find]");)
1423 IF_DEBUG(tmp->setName(
"CDO[Expr.eqNext]");)
1459 TRACE(
"setRewriteNormal",
"setRewriteNormal(", *
this,
")");
1581 if(sig != NULL) sig->
set(e);
1592 if(rep != NULL) rep->
set(e);
1600 inline bool operator==(
const Expr& e1,
const Expr& e2) {
1606 {
return !(e1 == e2); }
1611 {
return compare(e1,e2) < 0; }
1613 {
return compare(e1,e2) <= 0; }
1615 {
return compare(e1,e2) > 0; }
1617 {
return compare(e1,e2) >= 0; }
Class Op representing the Expr's operator.
unsigned getSimpCacheTag() const
Get the simplifier's cache tag.
CDFlags d_dynamicFlags
context-dependent bit-vector for flags that are context-dependent
Expr operator||(const Expr &right) const
void computeType(const Expr &e)
Compute the type of the Expr.
const Expr & getExpr() const
iterator begin() const
Begin iterator.
CDO< Theorem > * d_eqNext
Equality between this term and next term in ring of all terms in the equivalence class.
size_t getMMIndex() const
Get the memory manager index (it uniquely identifies the subclass)
bool getTerminalsConstFlag() const
Expr newSkolemExpr(const Expr &e, int i)
ExprValue * d_expr
The value. This is the only data member in this class.
std::vector< Expr > & getKids1()
Return reference to children.
void setRewriteNormal() const
void setFlag() const
Set the generic flag.
Data structure of expressions in CVC3.
const Theorem & getFind() const
ExprIndex d_index
Unique expression id.
ExprManager * getEM() const
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
friend bool operator>=(const Expr &e1, const Expr &e2)
virtual Op getOp() const
Get the Op from an Apply Expr.
void set(unsigned mask, int scope=-1)
bool isLiteral() const
Test if e is a literal.
iterator & operator++()
Prefix increment.
Compute transitive closure (for binary uninterpreted predicates)
static Expr s_null
Convenient null expr.
bool notArrayNormalized() const
void setStoredPredicate() const
Set the Stored Predicate flag for this Expr.
ExprValue * newExprValue(ExprValue *ev)
Return either an existing or a new ExprValue matching ev.
bool operator<=(const Expr &e1, const Expr &e2)
const Expr * operator->() const
Dereference and member access.
int compare(const Expr &e1, const Expr &e2)
virtual size_t getMMIndex() const
Get unique memory manager ID.
CDO< Theorem > * d_find
The find attribute (may be NULL)
bool isInitialized() const
ostream & operator<<(ostream &os, const Expr &e)
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
void clearFlags() const
Clear the generic flag in all Exprs.
virtual const Rational & getRational() const
void set(const T &data, int scope=-1)
unsigned d_refcount
Reference counter for garbage collection.
virtual bool isSymbol() const
Special named symbol.
bool isStoredPredicate() const
void setTriggers(const std::vector< std::vector< Expr > > &triggers) const
Set the triggers for a closure Expr.
Cardinality typeCard() const
Return cardinality of type.
InputLanguage
Different input languages.
bool isImpliedLiteral() const
void setFind(const Theorem &e) const
Set the find attribute to e.
void setIsAtomicFlag(bool value) const
bool computeTransClosure() const
long unsigned ExprIndex
Expression index type.
MS C++ specific settings.
Whether expr contains a bounded variable (for quantifier instantiation)
bool isPropAtom() const
True iff expr is not a Bool connective.
Expr()
Default constructor creates the Null Expr.
bool isTranslated() const
Theorem d_simpCache
For caching calls to Simplify.
friend int compare(const Expr &e1, const Expr &e2)
Expr operator&&(const Expr &right) const
Type lookupType() const
Look up the current type. Do not recursively compute (i.e. may be NULL)
Expr eqExpr(const Expr &right) const
virtual const Theorem & getTheorem() const
bool isAbsAtomicFormula() const
An abstract atomic formua is an atomic formula or a quantified formula.
Whether IS_ATOMIC flag is valid (initialized)
void setUserAssumption(int scope=-1) const
#define DebugAssert(cond, str)
NotifyList * d_notifyList
The cached TCC of the expression (may be Null)
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
bool inUserAssumption() const
bool isType() const
Expr represents a type.
bool operator==(const Expr &e1, const Expr &e2)
Definition of input and output languages to CVC3.
void setRep(const Theorem &e) const
void setSig(const Theorem &e) const
bool operator>(const Expr &e1, const Expr &e2)
const Expr & getExistential() const
Get the existential axiom expression for skolem constant.
friend bool operator<=(const Expr &e1, const Expr &e2)
const std::vector< std::vector< Expr > > & getTriggers() const
Get the manual triggers of the closure Expr.
bool get(unsigned mask) const
friend bool operator!=(const Expr &e1, const Expr &e2)
const std::vector< Expr > & getKids() const
Expr andExpr(const Expr &right) const
Whether is valid TYPE expr.
virtual unsigned arity() const
Default arity = 0.
Expr orExpr(const std::vector< Expr > &children)
virtual CDO< Theorem > * getRep() const
bool validIsAtomicFlag() const
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
void setValidType() const
Expr impExpr(const Expr &right) const
void setTrigger(const Expr &trigger) const
Context Dependent Vector of Flags.
bool isWellFounded() const
Op getOp() const
Get operator from expression.
virtual bool isVar() const
Uninterpreted constants.
ExprValueType
Type ID of each ExprValue subclass.
unsigned d_simpCacheTag
For checking whether simplify cache is valid.
virtual const ExprValue * getExprValue() const
Test whether the expression is a generic subclass.
virtual const std::string & getName() const
Returns the string name of UCONST and BOUND_VAR expr's.
virtual const std::vector< std::vector< Expr > > & getTriggers() const
Expr operator*(const Expr &left, const Expr &right)
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Unsigned typeSizeFinite() const
Return size of a finite type; returns 0 if size cannot be determined.
Application of functions and predicates.
bool isBoolConnective() const
A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool)
std::string toString() const
Print the expression to a string.
const std::vector< Expr > & getEmptyVector()
References to empty objects (used in ExprValue)
const Expr & operator*() const
Dereference operator.
Expr rebuild(ExprManager *em) const
Create a Boolean variable out of the expression.
const Theorem & getTheorem() const
Get theorem from THEOREM_EXPR.
virtual const std::vector< Expr > & getKids() const
Get kids: by default, returns a ref to an empty vector.
Expr skolemExpr(int i) const
Create a Skolem constant for the i'th variable of an existential (*this)
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
const Theorem & getSig() const
bool hasLastIndex() const
void setImpliedLiteral() const
bool validSimpCache() const
Return true if there is a valid cached value for calling simplify on this Expr.
bool getIsAtomicFlag() const
Whether TERMINALS_CONST flag is valid (initialized)
Expr typeEnumerateFinite(Unsigned n) const
Return nth (starting with 0) element in a finite type.
Expr iffExpr(const Expr &right) const
const Theorem & getEqNext() const
Abstraction over different operating systems.
const Theorem & getSimpCache() const
const Theorem & getRep() const
virtual bool isClosure() const
A LAMBDA-expression or a quantifier.
Proxy operator++(int)
Postfix increment.
bool isTypeKind(int kind)
Check if a kind represents a type.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
size_t hash(const ExprValue *ev) const
const Expr & unnegate() const
Remove leading NOT if any.
const Expr & getBody() const
Get the body of the closure Expr.
void clearRewriteNormal() const
virtual CDO< Theorem > * getSig() const
Special attributes for uninterpreted functions.
void incRefcount()
Increment reference counter.
virtual bool isApply() const
Application of another expression.
Whether the expression is an atomic term or formula.
void setRegisteredAtom() const
Set the RegisteredAtom flag for this Expr.
bool operator==(const iterator &i) const
Equality.
Expr & operator=(const Expr &e)
Assignment operator: take care of the refcounting and GC.
void clearFlags()
Clears the generic Expr flag in all Exprs.
bool operator<(const Expr &e1, const Expr &e2)
Unsigned getSize() const
Return DAG-size of Expr.
void setSimpCache(const Theorem &e) const
void setInUserAssumption(int scope=-1) const
void setUserRegisteredAtom() const
Set the UserRegisteredAtom flag for this Expr.
NotifyList * getNotify() const
bool getFlag() const
Check if the generic flag is set.
bool isUserRegisteredAtom() const
Expr orExpr(const Expr &right) const
bool isPropLiteral() const
PropAtom or negation of PropAtom.
Expression is the result of a "normal" (idempotent) rewrite.
virtual bool isString() const
String expression tester.
const std::string & getName() const
const ExprValue * getExprValue() const
Provide access to ExprValue for client subclasses of ExprValue only
void setTranslated(int scope=-1) const
Set the translated flag for this Expr.
Context * getCurrentContext() const
Get the current context from our ContextManager.
void decRefcount()
Decrement reference counter.
int getBoundIndex() const
Get the index of the bound var that skolem constant comes from.
Well-founded (used in datatypes)
Whether expr has been added as an implied literal.
unsigned getFlag()
Return the current Expr flag counter.
virtual int getBoundIndex() const
Unsigned d_size
Size of dag rooted at this expression.
virtual const std::string & getString() const
bool operator>=(const Expr &e1, const Expr &e2)
A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers...
ExprManager * d_em
Our expr. manager.
bool isRegisteredAtom() const
virtual const std::vector< Expr > & getVars() const
void setSelected() const
Set the Selected flag for this Expr.
void setType(const Type &t) const
Set the cached type.
void setTerminalsConstFlag(bool value) const
unsigned d_flag
Which child has the largest height.
void print() const
Print the expression as AST (lisp-like format)
iterator(std::vector< Expr >::const_iterator it)
Construct an iterator out of the vector's iterator.
bool isQuantifier() const
Whether expr contains only numerical constants at all possible ite terminals.
bool isUserAssumption() const
bool operator!=(const Expr &e1, const Expr &e2)
bool isAbsLiteral() const
Test if e is an abstract literal.
bool isIntAssumption() const
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Expr xorExpr(const Expr &right) const
bool containsBoundVar() const
void gc(ExprValue *ev)
Garbage collect the ExprValue pointer.
Whether expr uses CC algorithm that relies on not simplifying an expr that has a find.
Expr rebuild(const Expr &e)
Rebuild the Expr with this ExprManager if it belongs to another ExprManager.
virtual const Expr & getExistential() const
virtual void setSig(CDO< Theorem > *sig)
Op mkOp() const
Make the expr into an operator.
const Expr & getLHS() const
void setEqNext(const Theorem &e) const
Set the eqNext attribute to e.
void setMultiTrigger(const std::vector< Expr > &multiTrigger) const
int d_kind
The kind of the expression. In particular, it determines which subclass of ExprValue is used to store...
bool isRewriteNormal() const
Type d_type
The cached type of the expression (may be Null)
void setIntAssumption() const
void setWellFounded() const
The base class for holding the actual data in expressions.
Cardinality
Enum for cardinality of types.
bool validTerminalsConstFlag() const
ExprIndex getIndex() const
const std::string & getString() const
bool operator!=(const iterator &i) const
Disequality.
Postfix increment requires a Proxy object to hold the intermediate value for dereferencing.
Type getType() const
Get the type. Recursively compute if necessary.
virtual const std::string & getUid() const
void setNotArrayNormalized() const
friend bool operator>(const Expr &e1, const Expr &e2)
void setContainsBoundVar() const
const Expr & operator[](int i) const
void setJustified() const
std::vector< Expr >::const_iterator d_it
void setComputeTransClosure() const
Expr andExpr(const std::vector< Expr > &children)
friend bool operator<(const Expr &e1, const Expr &e2)
virtual void setRep(CDO< Theorem > *rep)
virtual void setTriggers(const std::vector< std::vector< Expr > > &triggers)
iterator()
Default constructor.
void clear(unsigned mask, int scope=-1)
Whether expr is normalized (in array theory)
virtual bool isTheorem() const
Special Expr holding a theorem.
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Get information related to finiteness of a type.
virtual const Expr & getBody() const
iterator end() const
End iterator.
const std::string & getUid() const
For BOUND_VAR, get the UID.