diff options
author | Tim King <taking@cs.nyu.edu> | 2010-04-28 20:14:17 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-04-28 20:14:17 +0000 |
commit | c59fe5b21c218d3d6048cc5c34a7e27b3643ae78 (patch) | |
tree | bfd3c1d1eb975989b0ef4afa4e88da4eae84ba62 /src/theory/arith/normal.h | |
parent | 2482b19ea90183d5040390b87877b7593021032c (diff) |
Merging the arithmetic theory draft (lra-init) back into the main trunk. This should not affect other parts of the system. This code is untested, and is volatile. It is going to be improved in the future so don't pick on it too much. I am merging this code in its current state back into the main trunk because it was getting unruly to keep merging the updated trunk back into the branch.
Diffstat (limited to 'src/theory/arith/normal.h')
-rw-r--r-- | src/theory/arith/normal.h | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/theory/arith/normal.h b/src/theory/arith/normal.h new file mode 100644 index 000000000..7f8192a7d --- /dev/null +++ b/src/theory/arith/normal.h @@ -0,0 +1,29 @@ + +#ifndef __CVC4__THEORY__ARITH__NORMAL_H +#define __CVC4__THEORY__ARITH__NORMAL_H + +namespace CVC4 { +namespace theory { +namespace arith { + +struct IsNormalAttrID; + +typedef expr::Attribute<IsNormalAttrID, bool> IsNormal; + + +inline bool isNormalized(TNode x){ + return x.hasAttribute(IsNormal()); +} + +struct NormalFormAttrID; + +typedef expr::Attribute<IsNormalAttrID, Node> NormalForm; + + + +}; /* namespace arith */ +}; /* namespace theory */ +}; /* namespace CVC4 */ + + +#endif /* __CVC4__THEORY__ARITH__NORMAL_H */ |