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/arith_constants.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/arith_constants.h')
-rw-r--r-- | src/theory/arith/arith_constants.h | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h new file mode 100644 index 000000000..d9419cd6b --- /dev/null +++ b/src/theory/arith/arith_constants.h @@ -0,0 +1,38 @@ + + +#include "expr/node.h" +#include "expr/node_manager.h" +#include "util/rational.h" + +#ifndef __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H +#define __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H + +namespace CVC4 { +namespace theory { +namespace arith { + +class ArithConstants{ +public: + Rational d_ZERO; + Rational d_ONE; + Rational d_NEGATIVE_ONE; + + Node d_ZERO_NODE; + Node d_ONE_NODE; + Node d_NEGATIVE_ONE_NODE; + + ArithConstants(NodeManager* nm) : + d_ZERO(0,1), + d_ONE(1,1), + d_NEGATIVE_ONE(-1,1), + d_ZERO_NODE(nm->mkConst(d_ZERO)), + d_ONE_NODE(nm->mkConst(d_ONE)), + d_NEGATIVE_ONE_NODE(nm->mkConst(d_NEGATIVE_ONE)) + {} +}; + +}; /* namesapce arith */ +}; /* namespace theory */ +}; /* namespace CVC4 */ + +#endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */ |