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 */