- Removes arith_constants.h

- Adds ArithStaticLearner.  Consolidates and cleans up the code for static learning in arithmetic.  Static learning is now associated with a small amount of state between calls. This is used to track the data for the miplib trick.  The goal is to make this inference work without relying on the fact that all of the miplib problem is asserted under the same AND node.
- This commit contains miscellaneous other arithmetic cleanup.

1 files changed, 0 insertions, 67 deletions

diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h
deleted file mode 100644
index 98a202207..000000000
--- a/src/theory/arith/arith_constants.h
+++ /dev/null
@@ -1,67 +0,0 @@
-/*********************                                                        */
-/*! \file arith_constants.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H
-#define __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H
-
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "util/rational.h"
-#include "theory/arith/delta_rational.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class ArithConstants {
-public:
-  Rational d_ZERO;
-  Rational d_ONE;
-  Rational d_NEGATIVE_ONE;
-
-  DeltaRational d_ZERO_DELTA;
-
-  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_DELTA(d_ZERO),
-    d_ZERO_NODE(nm->mkConst(d_ZERO)),
-    d_ONE_NODE(nm->mkConst(d_ONE)),
-    d_NEGATIVE_ONE_NODE(nm->mkConst(d_NEGATIVE_ONE))
-  {}
-
-  ~ArithConstants() {
-    d_ZERO_NODE = Node::null();
-    d_ONE_NODE = Node::null();
-    d_NEGATIVE_ONE_NODE = Node::null();
-  }
-};/* class ArithConstants */
-
-}/* namespace CVC4::theory::arith */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
-
-#endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */