expr_value.h File Reference

#include "theorem.h"
#include "type.h"
#include "expr.h"

Include dependency graph for expr_value.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces

• namespace CVC3

Classes

• class CVC3::ExprValue

  The base class for holding the actual data in expressions. More...
  

• class CVC3::ExprNode
• class CVC3::ExprNodeTmp
• class CVC3::ExprApplyTmp
• class CVC3::ExprApply
• class CVC3::ExprString
• class CVC3::ExprSkolem
• class CVC3::ExprRational
• class CVC3::ExprVar
• class CVC3::ExprSymbol
• class CVC3::ExprBoundVar
• class CVC3::ExprClosure

  A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers. More...
  

Defines

• #define PRIME   131

---

Detailed Description

Author: Sergey Berezin

Created: Fri Feb 7 15:07:18 2003

---

License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution.

---

Class ExprValue: the value holding class of Expr. No one should use it directly; use Expr API instead. To enforce that, the constructors are made protected, and only Expr, ExprManager, and subclasses can use them.

Definition in file expr_value.h.

---

Define Documentation

#define PRIME   131

Definition at line 50 of file expr_value.h.

Referenced by CVC3::BVConstExpr::computeHash(), CVC3::ExprBoundVar::computeHash(), CVC3::ExprSymbol::computeHash(), CVC3::ExprSkolem::computeHash(), CVC3::ExprApply::computeHash(), CVC3::ExprApplyTmp::computeHash(), CVC3::ExprClosure::computeHash(), and CVC3::ExprValue::hash().

---