From c59fe5b21c218d3d6048cc5c34a7e27b3643ae78 Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 28 Apr 2010 20:14:17 +0000 Subject: 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. --- src/theory/arith/arith_constants.h | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 src/theory/arith/arith_constants.h (limited to 'src/theory/arith/arith_constants.h') 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 */ -- cgit v1.2.3