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);