FCSimplex branch merge

1 files changed, 7 insertions, 45 deletions

diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
index e6cecff3f..66b68339d 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.h
@@ -19,15 +19,12 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__ARITHVAR_H
-#define __CVC4__THEORY__ARITH__ARITHVAR_H
-
-#include <ext/hash_map>
-#include "expr/node.h"
-#include "context/cdhashset.h"
+#pragma once
 
+#include <vector>
 #include "util/index.h"
-#include "util/dense_map.h"
+#include "util/rational.h"
+
 
 namespace CVC4 {
 namespace theory {
@@ -36,46 +33,11 @@ namespace arith {
 typedef Index ArithVar;
 extern const ArithVar ARITHVAR_SENTINEL;
 
-//Maps from Nodes -> ArithVars, and vice versa
-typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
-typedef DenseMap<Node> ArithVarToNodeMap;
-
-/**
- * ArithVarCallBack provides a mechanism for agreeing on callbacks while
- * breaking mutual recursion inclusion order problems.
- */
-class ArithVarCallBack {
-public:
-  virtual void operator()(ArithVar x) = 0;
-};
-
-/**
- * Requests arithmetic variables for internal use,
- * and releases arithmetic variables that are no longer being used.
- */
-class ArithVarMalloc {
-public:
-  virtual ArithVar request() = 0;
-  virtual void release(ArithVar v) = 0;
-};
-
-class TNodeCallBack {
-public:
-  virtual void operator()(TNode n) = 0;
-};
-
-class NodeCallBack {
-public:
-  virtual void operator()(Node n) = 0;
-};
-
-class RationalCallBack {
-public:
-  virtual Rational operator()() const = 0;
-};
+typedef std::vector<ArithVar> ArithVarVec;
+typedef std::pair<ArithVar, Rational> ArithRatPair;
+typedef std::vector< ArithRatPair > ArithRatPairVec;
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__ARITHVAR_H */