24 #ifndef _cvc3__expr_h_
28 #ifndef _cvc3__include__expr_manager_h_
29 #define _cvc3__include__expr_manager_h_
40 class ExprManagerNotifyObj;
80 return h(const_cast<char*>(s.c_str()));
133 std::vector<MemoryManager*>
d_mm;
188 virtual void computeType(
const Expr& e) = 0;
190 virtual void checkType(
const Expr& e) = 0;
193 bool enumerate,
bool computeSize) = 0;
216 {
FatalAssert(++d_flagCounter,
"flag overflow");
return d_flagCounter; }
219 void computeType(
const Expr& e);
221 void checkType(
const Expr& e);
231 bool enumerate,
bool computeSize);
291 Expr newLeafExpr(
const Op& op);
292 Expr newStringExpr(
const std::string &s);
294 Expr newSkolemExpr(
const Expr& e,
int i);
295 Expr newVarExpr(
const std::string &s);
296 Expr newSymbolExpr(
const std::string &s,
int kind);
297 Expr newBoundVarExpr(
const std::string &name,
const std::string& uid);
298 Expr newBoundVarExpr(
const std::string &name,
const std::string& uid,
300 Expr newBoundVarExpr(
const Type& type);
301 Expr newClosureExpr(
int kind,
const Expr& var,
const Expr& body);
302 Expr newClosureExpr(
int kind,
const std::vector<Expr>& vars,
304 Expr newClosureExpr(
int kind,
const std::vector<Expr>& vars,
305 const Expr& body,
const Expr& trigger);
306 Expr newClosureExpr(
int kind,
const std::vector<Expr>& vars,
307 const Expr& body,
const std::vector<Expr>& triggers);
308 Expr newClosureExpr(
int kind,
const std::vector<Expr>& vars,
309 const Expr& body,
const std::vector<std::vector<Expr> >& triggers);
313 {
return Expr(
AND, children,
this); }
315 {
return Expr(
OR, children,
this); }
335 DebugAssert(MMIndex < d_mm.size(),
"ExprManager::getMM()");
336 return d_mm[MMIndex];
345 { d_typeComputer = typeComputer; }
354 int indent()
const {
return d_indentTransient; }
356 int indent(
int n,
bool permanent =
false);
360 int incIndent(
int n,
bool permanent =
false);
383 void newKind(
int kind,
const std::string &name,
bool isType =
false);
389 void unregisterPrettyPrinter();
394 bool isTypeKind(
int kind) {
return d_typeKinds.count(kind) > 0; }
398 const std::string& getKindName(
int kind);
400 int getKind(
const std::string& name);
407 size_t registerSubclass(
size_t sizeOfSubclass);
410 unsigned long getMemory(
int verbosity);
450 DebugAssert(ev!=NULL,
"ExprManager::hash() called on a NULL ExprValue");
462 std::vector<Expr> kids;
485 const std::string& uid)
489 const std::string& uid,
494 "newBoundVarExpr: redefining a variable " + name);
500 static int nextNum = 0;
501 std::string name(
"_cvc3_");
512 const std::vector<Expr>& vars,
517 const std::vector<Expr>& vars,
519 const std::vector<Expr>& triggers)
524 const std::vector<Expr>& vars,
526 const std::vector<std::vector<Expr> >& triggers)
531 const std::vector<Expr>& vars,
539 return (*ev1) == (*ev2);
unsigned getSimpCacheTag() const
Get the simplifier's cache tag.
const Expr & getExpr() const
std::vector< Expr > d_emptyVec
Empty vector of Expr to return by reference as empty vector of children.
Expr newSkolemExpr(const Expr &e, int i)
ExprValue * d_expr
The value. This is the only data member in this class.
std::deque< ExprValue * > d_pending
Queue of pending exprs to GC.
Data structure of expressions in CVC3.
int d_indent
Permanent indentation.
TypeComputer * d_typeComputer
Instance of TypeComputer: must be registered.
ExprManager * getEM() const
PrettyPrinter * d_prettyPrinter
The registered pretty-printer, a connector to theory-specific pretty-printers.
Expr d_nullExpr
Null Expr to return by reference, for efficiency.
const Expr & getNullExpr()
References to empty objects (used in ExprValue)
void postponeGC()
Postpone deletion of garbage-collected expressions.
size_t operator()(const std::string &s) const
unsigned d_simpCacheTagCurrent
Current value of the simplifier cache tag.
std::vector< ExprValue * > d_postponed
Vector of postponed garbage-collected expressions.
Expr newSymbolExpr(const std::string &s, int kind)
const Expr & boolExpr()
BOOLEAN Expr.
int scopelevel()
Get current scope level.
void setTriggers(const std::vector< std::vector< Expr > > &triggers) const
Set the triggers for a closure Expr.
Private class for d_exprSet.
InputLanguage
Different input languages.
void setTM(TheoremManager *tm)
Set the TheoremManager.
ContextManager * getCM() const
Fetch our ContextManager.
long unsigned ExprIndex
Expression index type.
bool dagPrinting() const
Whether to print Expr's as DAGs.
MS C++ specific settings.
std::hash_set< ExprValue *, HashEV, EqEV > ExprValueSet
Hash set type for uniquifying expressions.
Expr orExpr(const std::vector< Expr > &children)
const std::string * d_inputLang
Input language (printing)
Type lookupType() const
Look up the current type. Do not recursively compute (i.e. may be NULL)
Notifies ExprManager before and after each pop()
bool d_postponeGC
Postpone deleting garbage-collected expressions.
const std::string * d_outputLang
Output language (printing)
size_t hash() const
Caching hash function.
#define DebugAssert(cond, str)
ExprHashMap< Expr > d_rebuildCache
Rebuild cache.
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
ExprIndex d_index
Index counter for Expr compare()
void registerTypeComputer(TypeComputer *typeComputer)
Register type computer.
const int * d_lineWidth
Suggested line width for printing with indentation.
const bool * d_dagPrinting
Whether to print Expr's as DAGs.
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
void setTrigger(const Expr &trigger) const
ContextManager * d_cm
For backtracking attributes.
const Expr & getExpr() const
std::hash_map< std::string, int, HashString > d_kindMapByName
The reverse map of names to kinds.
Expr newExpr(ExprValue *ev)
Return either an existing or a new Expr matching ev.
MemoryManager * getMM(size_t MMIndex)
Return a MemoryManager for the given ExprValue type.
Expr newStringExpr(const std::string &s)
unsigned long getMemory(int verbosity)
std::hash_set< int > d_typeKinds
The set of kinds representing a type.
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
TheoremManager * getTM() const
Fetch the TheoremManager.
Abstract class for computing expr type.
const int * d_printDepth
Print upto the given depth, replace the rest with "...". -1==unlimited depth.
const std::vector< Expr > & getEmptyVector()
References to empty objects (used in ExprValue)
bool withIndentation() const
Whether to print with indentation.
Abstraction over different operating systems.
const Expr & falseExpr()
FALSE Expr.
bool isTypeKind(int kind)
Check if a kind represents a type.
Expr newLeafExpr(const Op &op)
size_t hash(const ExprValue *ev) const
PrettyPrinter * getPrinter() const
Return the pretty-printer if there is one; otherwise return NULL.
std::string int2string(int n)
bool d_inGC
Flag for whether GC is already running.
const Expr & trueExpr()
TRUE Expr.
unsigned d_flagCounter
Counter for a generic Expr flag.
TheoremManager * d_tm
Needed for Refl Theorems.
void clearFlags()
Clears the generic Expr flag in all Exprs.
std::hash< void * > d_pointerHash
A hash function for hashing pointers.
size_t operator()(ExprValue *ev) const
Expr newRatExpr(const Rational &r)
void restoreIndent()
Set transient indentation to permanent.
Private class for d_exprSet.
Context * getCurrentContext() const
Get the current context from our ContextManager.
int indent() const
Get initial indentation.
std::hash_map< int, std::string > d_kindMap
The database of registered kinds.
unsigned getFlag()
Return the current Expr flag counter.
A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers...
void setType(const Type &t) const
Set the cached type.
int printDepth() const
Get printing depth.
Expr andExpr(const std::vector< Expr > &children)
bool isKindRegistered(int kind)
Returns true if kind is built into CVC or has been registered via newKind.
Expr d_bool
Expr constants cached for fast access.
ExprManagerNotifyObj * d_notifyObj
Notification on pop()
const std::string d_mmFlag
Which memory manager to use (copy the flag value and keep it the same)
bool d_disableGC
Disable garbage collection.
Definition of the API to expression package. See class Expr for details.
Private class for hashing strings.
ExprIndex nextIndex()
Return the next Expr index.
Expr newVarExpr(const std::string &s)
const bool * d_withIndentation
Whether to print with indentation.
ExprManagerNotifyObj(ExprManager *em, Context *cxt)
Constructor.
void invalidateSimpCache()
Invalidate the simplifier's cache tag.
The base class for holding the actual data in expressions.
Cardinality
Enum for cardinality of types.
int lineWidth() const
Suggested line width for printing with indentation.
Manager for multiple contexts. Also holds current context.
int d_indentTransient
Transient indentation.
ExprValueSet d_exprSet
Hash set for uniquifying expressions.
std::vector< MemoryManager * > d_mm
Array of memory managers for subclasses of ExprValue.
Abstract API to a pretty-printer for Expr.
unsigned nextFlag()
Increment and return the Expr flag counter (this clears all the flags)
bool operator()(const ExprValue *ev1, const ExprValue *ev2) const