diff options
Diffstat (limited to 'src/theory/arith/arithvar.h')
-rw-r--r-- | src/theory/arith/arithvar.h | 52 |
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 */ |