39 #ifndef _cvc3__expr_h_
43 #ifndef _cvc3__expr_value_h_
44 #define _cvc3__expr_value_h_
73 friend class ::CInterface;
149 if((--d_refcount) == 0) d_em->
gc(
this);
157 const_cast<ExprValue*
>(
this)->d_hash = computeHash();
163 if (d_flag == d_em->
getFlag())
return 0;
165 return computeSize();
185 static size_t pointerHash(
void* p) {
return s_intHash((
long int)p); }
187 static size_t hash(
const int kind,
const std::vector<Expr>& kids);
189 static size_t hash(
const int n) {
return s_intHash((
long int)n); }
192 static Unsigned sizeWithChildren(
const std::vector<Expr>& kids);
197 return d_em->
getMM(MMIndex);
202 {
return copy(em, 0); }
224 : d_index(idx), d_refcount(0),
225 d_hash(0), d_find(NULL), d_eqNext(NULL), d_notifyList(NULL),
227 d_dynamicFlags(em->getCurrentContext()),
230 d_flag(0), d_kind(kind), d_em(em)
232 DebugAssert(em != NULL,
"NULL ExprManager is given to ExprValue()");
235 +
")): kind is not registered").c_str());
254 {
return mm->newData(size); }
256 mm->deleteData(pMem);
260 void operator delete(
void*) { }
276 {
throw Exception(
"Illegal call to getExprValue()"); }
282 virtual bool isVar()
const {
return false; }
284 virtual bool isApply()
const {
return false; }
293 virtual const std::vector<Expr>&
getKids()
const
299 virtual unsigned arity()
const {
return 0; }
303 DebugAssert(
false,
"getSig() is called on ExprValue");
308 DebugAssert(
false,
"getRep() is called on ExprValue");
313 DebugAssert(
false,
"setSig() is called on ExprValue");
317 DebugAssert(
false,
"setRep() is called on ExprValue");
320 virtual const std::string&
getUid()
const {
321 static std::string null;
322 DebugAssert(
false,
"ExprValue::getUid() called in base class");
327 DebugAssert(
false,
"getString() is called on ExprValue");
328 static std::string s(
"");
333 DebugAssert(
false,
"getRational() is called on ExprValue");
340 static std::string ret =
"";
341 DebugAssert(
false,
"getName() is called on ExprValue");
347 DebugAssert(
false,
"getVar() is called on ExprValue");
354 DebugAssert(
false,
"getOp() is called on ExprValue");
358 virtual const std::vector<Expr>&
getVars()
const {
359 DebugAssert(
false,
"getVars() is called on ExprValue");
360 static std::vector<Expr> null;
365 DebugAssert(
false,
"getBody() is called on ExprValue");
370 virtual void setTriggers(
const std::vector<std::vector<Expr> >& triggers) {
371 DebugAssert(
false,
"setTriggers() is called on ExprValue");
374 virtual const std::vector<std::vector<Expr> >&
getTriggers()
const {
375 DebugAssert(
false,
"getTrigs() is called on ExprValue");
376 static std::vector<std::vector<Expr> > null;
382 DebugAssert(
false,
"getExistential() is called on ExprValue");
387 DebugAssert(
false,
"getIndex() is called on ExprValue");
391 virtual const std::vector<std::string>&
getFields()
const {
392 DebugAssert(
false,
"getFields() is called on ExprValue");
393 static std::vector<std::string> null;
397 DebugAssert(
false,
"getField() is called on ExprValue");
398 static std::string null;
402 DebugAssert(
false,
"getTupleIndex() is called on ExprValue");
407 DebugAssert(
false,
"getTheorem() is called on ExprValue");
433 unsigned arity()
const {
return d_children.size(); }
436 std::vector<Expr>&
getKids1() {
return d_children; }
439 const std::vector<Expr>&
getKids()
const {
return d_children; }
457 :
ExprValue(em, kind, idx), d_sig(NULL), d_rep(NULL) { }
461 :
ExprValue(em, kind, idx), d_children(kids), d_sig(NULL), d_rep(NULL) { }
467 {
return mm->newData(size); }
469 mm->deleteData(pMem);
473 void operator delete(
void*) { }
502 unsigned arity()
const {
return d_children.size(); }
523 :
ExprValue(em, kind, 0), d_children(kids) { }
551 const std::vector<Expr>& kids)
581 const std::vector<Expr>& kids,
ExprIndex idx = 0)
590 return mm->newData(size);
593 mm->deleteData(pMem);
595 void operator delete(
void*) { }
666 static size_t hash(
const std::string& str) {
692 return mm->newData(size);
695 mm->deleteData(pMem);
697 void operator delete(
void*) { }
733 return mm->newData(size);
736 mm->deleteData(pMem);
738 void operator delete(
void*) { }
773 return mm->newData(size);
776 mm->deleteData(pMem);
778 void operator delete(
void*) { }
797 virtual bool isVar()
const {
return true; }
812 return mm->newData(size);
815 mm->deleteData(pMem);
817 void operator delete(
void*) { }
844 :
ExprValue(em, kind, idx), d_name(name) { }
851 return mm->newData(size);
854 mm->deleteData(pMem);
856 void operator delete(
void*) { }
876 virtual bool isVar()
const {
return true; }
883 const std::string& uid,
ExprIndex idx = 0)
891 return mm->newData(size);
894 mm->deleteData(pMem);
896 void operator delete(
void*) { }
917 virtual void setTriggers(
const std::vector<std::vector<Expr> >& triggers) { d_manual_triggers = triggers; }
931 :
ExprValue(em, kind, idx), d_body(body) { d_vars.push_back(var); }
935 :
ExprValue(em, kind, idx), d_vars(vars), d_body(body) { }
938 const Expr& body,
const std::vector<std::vector<Expr> >& trigs,
ExprIndex idx = 0)
939 :
ExprValue(em, kind, idx), d_vars(vars), d_body(body), d_manual_triggers(trigs) { }
947 return mm->newData(size);
950 mm->deleteData(pMem);
952 void operator delete(
void*) { }
Unsigned computeSize() const
Non-caching size function which actually computes the size.
Expr d_body
The body of the quantifier/lambda.
CDFlags d_dynamicFlags
context-dependent bit-vector for flags that are context-dependent
const Expr & getExpr() const
CDO< Theorem > * d_eqNext
Equality between this term and next term in ring of all terms in the equivalence class.
unsigned arity() const
Return number of children.
size_t computeHash() const
Use our static hash() for the member method.
Expr rebuildRec(const Expr &e)
Cached recursive descent. Must be called only during rebuild()
ExprValue * d_expr
The value. This is the only data member in this class.
virtual const std::string & getUid() const
bool isSymbol() const
Special named symbol.
std::vector< Expr > & getKids1()
Return reference to children.
ExprNodeTmp(ExprManager *em, int kind, const std::vector< Expr > &kids)
Constructor.
ExprValue * rebuild(ExprManager *em) const
Make a clean copy of itself using the given ExprManager.
Data structure of expressions in CVC3.
ExprIndex d_index
Unique expression id.
virtual size_t computeHash() const
Non-caching hash function which actually computes the hash.
virtual bool isRational() const
Rational number expression tester.
std::vector< Expr > d_children
Vector of children.
virtual const std::string & getName() const
Returns the string name of UCONST and BOUND_VAR expr's.
virtual void setSig(CDO< Theorem > *sig)
Op getOp() const
Get the Op from an Apply Expr.
bool isVar() const
Uninterpreted constants.
virtual bool operator==(const ExprValue &ev2) const
Compare with another ExprValue.
static size_t pointerHash(void *p)
virtual Op getOp() const
Get the Op from an Apply Expr.
virtual size_t computeHash() const
Non-caching hash function which actually computes the hash.
size_t computeHash() const
Non-caching hash function which actually computes the hash.
ExprApply(ExprManager *em, const Op &op, const std::vector< Expr > &kids, ExprIndex idx=0)
virtual size_t getMMIndex() const
Get unique memory manager ID.
Expr rebuild(Expr e, ExprManager *em) const
Make a clean copy of the expr using the given ExprManager.
CDO< Theorem > * d_find
The find attribute (may be NULL)
virtual ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
virtual const Rational & getRational() const
Op getOp() const
Get the Op from an Apply Expr.
ExprClosure(ExprManager *em, int kind, const Expr &var, const Expr &body, ExprIndex idx=0)
unsigned d_refcount
Reference counter for garbage collection.
virtual bool isSymbol() const
Special named symbol.
virtual void setRep(CDO< Theorem > *rep)
virtual bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
long unsigned ExprIndex
Expression index type.
MS C++ specific settings.
virtual bool isString() const
String expression tester.
static Unsigned sizeWithChildren(const std::vector< Expr > &kids)
Theorem d_simpCache
For caching calls to Simplify.
size_t d_hash
Cached hash value (initially 0)
ExprClosure(ExprManager *em, int kind, const std::vector< Expr > &vars, const Expr &body, ExprIndex idx=0)
bool isApply() const
Application of another expression.
virtual ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
virtual bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
Expr d_quant
The quantified expression to skolemize.
std::string toString(int base=10) const
virtual const Theorem & getTheorem() const
virtual bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
int getKind() const
Get the kind of the expression.
virtual size_t computeHash() const
Non-caching hash function which actually computes the hash.
virtual const std::string & getName() const
Returns the string name of UCONST and BOUND_VAR expr's.
size_t getMMIndex() const
Get unique memory manager ID.
size_t hash() const
Caching hash function.
virtual const Expr & getVar() const
Returns the original Boolean variable (for BoolVarExprValue)
virtual bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
#define DebugAssert(cond, str)
NotifyList * d_notifyList
The cached TCC of the expression (may be Null)
bool operator==(const Expr &e1, const Expr &e2)
virtual bool isRational() const
Rational number expression tester.
virtual ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
const std::vector< Expr > & d_children
Vector of children.
bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
ExprNode(ExprManager *em, int kind, ExprIndex idx=0)
Constructor.
virtual const std::vector< std::string > & getFields() const
ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
virtual unsigned arity() const
Default arity = 0.
virtual size_t getMMIndex() const
Get unique memory manager ID.
virtual bool isVar() const
Uninterpreted constants.
virtual CDO< Theorem > * getRep() const
virtual size_t computeHash() const
Non-caching hash function which actually computes the hash.
ExprRational(ExprManager *em, const Rational &r, ExprIndex idx=0)
virtual size_t getMMIndex() const
Get unique memory manager ID.
Unsigned computeSize() const
Use our static sizeWithChildren() for the member method.
MemoryManager * getMM(size_t MMIndex)
Return a MemoryManager for the given ExprValue type.
std::vector< std::vector< Expr > > d_manual_triggers
Manual triggers. // added by yeting.
virtual bool isVar() const
Uninterpreted constants.
virtual CDO< Theorem > * getRep() const
unsigned d_simpCacheTag
For checking whether simplify cache is valid.
virtual const ExprValue * getExprValue() const
Test whether the expression is a generic subclass.
std::vector< Expr > d_vars
Bound variables.
virtual const std::string & getName() const
Returns the string name of UCONST and BOUND_VAR expr's.
ExprSkolem(ExprManager *em, int index, const Expr &exist, ExprIndex idx=0)
virtual const std::vector< std::vector< Expr > > & getTriggers() const
virtual int getTupleIndex() const
virtual ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
ExprString(ExprManager *em, const std::string &s, ExprIndex idx=0)
ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
Application of functions and predicates.
const std::vector< Expr > & getEmptyVector()
References to empty objects (used in ExprValue)
virtual ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
static size_t hash(const Rational &r)
virtual const std::vector< Expr > & getKids() const
Get kids: by default, returns a ref to an empty vector.
static std::hash< char * > s_charHash
Return child with greatest height.
virtual bool isClosure() const
A LAMBDA-expression or a quantifier.
int getBoundIndex() const
virtual const std::string & getField() const
const Expr & getBody() const
Get the body of the closure Expr.
std::string int2string(int n)
virtual CDO< Theorem > * getSig() const
Special attributes for uninterpreted functions.
virtual size_t computeHash() const
Non-caching hash function which actually computes the hash.
size_t computeHash() const
Use our static hash() for the member method.
const std::vector< Expr > & getKids() const
Return reference to children.
ExprSymbol(ExprManager *em, int kind, const std::string &name, ExprIndex idx=0)
void incRefcount()
Increment reference counter.
virtual bool isApply() const
Application of another expression.
virtual size_t getMMIndex() const
Tell ExprManager who we are.
ExprApplyTmp(ExprManager *em, const Op &op, const std::vector< Expr > &kids)
unsigned arity() const
Return number of children.
MemoryManager * getMM(size_t MMIndex)
Return the memory manager (for the benefit of subclasses)
virtual void setTriggers(const std::vector< std::vector< Expr > > &triggers)
ExprVar(ExprManager *em, const std::string &name, ExprIndex idx=0)
Unsigned getSize() const
Return DAG-size of Expr.
bool operator==(const ExprValue &ev2) const
Compare with another ExprValue.
virtual Unsigned computeSize() const
Non-caching size function which actually computes the size.
size_t computeHash() const
Non-caching hash function which actually computes the hash.
virtual bool isString() const
String expression tester.
void decRefcount()
Decrement reference counter.
unsigned getFlag()
Return the current Expr flag counter.
virtual ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
static size_t hash(const Expr &e)
ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
virtual int getBoundIndex() const
ExprApply(ExprManager *em, const Op &op, ExprIndex idx=0)
ExprValue(ExprManager *em, int kind, ExprIndex idx=0)
Constructor.
Unsigned d_size
Size of dag rooted at this expression.
virtual const std::string & getString() const
A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers...
ExprManager * d_em
Our expr. manager.
virtual const std::vector< Expr > & getVars() const
virtual const Rational & getRational() const
size_t getMMIndex() const
Tell ExprManager who we are.
unsigned d_flag
Which child has the largest height.
size_t getMMIndex() const
Tell ExprManager who we are.
bool isApply() const
Application of another expression.
Unsigned computeSize() const
Use our static sizeWithChildren() for the member method.
virtual ~ExprNodeTmp()
Destructor.
static std::hash< long int > s_intHash
const std::vector< Expr > & getKids() const
Return reference to children.
size_t getMMIndex() const
Tell ExprManager who we are.
bool isKindRegistered(int kind)
Returns true if kind is built into CVC or has been registered via newKind.
static size_t hash(const std::string &str)
virtual bool isVar() const
Uninterpreted constants.
Definition of the API to expression package. See class Expr for details.
void gc(ExprValue *ev)
Garbage collect the ExprValue pointer.
virtual const Expr & getBody() const
ExprBoundVar(ExprManager *em, const std::string &name, const std::string &uid, ExprIndex idx=0)
virtual const Expr & getExistential() const
virtual void setSig(CDO< Theorem > *sig)
const Expr & getExistential() const
virtual const std::vector< Expr > & getVars() const
size_t getMMIndex() const
Tell ExprManager who we are.
int d_kind
The kind of the expression. In particular, it determines which subclass of ExprValue is used to store...
virtual const std::vector< std::vector< Expr > > & getTriggers() const
int d_idx
Variable index in the quantified expression.
Type d_type
The cached type of the expression (may be Null)
virtual size_t getMMIndex() const
Get unique memory manager ID.
static size_t hash(const int n)
ExprClosure(ExprManager *em, int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &trigs, ExprIndex idx=0)
The base class for holding the actual data in expressions.
virtual size_t computeHash() const
Non-caching hash function which actually computes the hash.
ExprNode(ExprManager *em, int kind, const std::vector< Expr > &kids, ExprIndex idx=0)
Constructor.
virtual const std::string & getUid() const
virtual const std::string & getName() const
Returns the string name of UCONST and BOUND_VAR expr's.
virtual size_t getMMIndex() const
Get unique memory manager ID.
virtual void setRep(CDO< Theorem > *rep)
virtual void setTriggers(const std::vector< std::vector< Expr > > &triggers)
virtual bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
virtual CDO< Theorem > * getSig() const
Special attributes for uninterpreted functions.
virtual bool isClosure() const
A LAMBDA-expression or a quantifier.
virtual const std::string & getString() const
void setIndex(ExprIndex idx)
Set the ExprIndex.
virtual bool isTheorem() const
Special Expr holding a theorem.
bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
virtual const Expr & getBody() const
size_t computeHash() const
Use our static hash() for the member method.
size_t computeHash() const
Use our static hash() for the member method.
virtual size_t getMMIndex() const
Get unique memory manager ID.