diff options
author | Tim King <taking@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
commit | 9098391fe334d829ec4101f190b8f1fa21c30752 (patch) | |
tree | b134fc1fe1c767a50013e1449330ca6a7ee18a3d /src/theory/arith/arithvar.h | |
parent | a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16 (diff) |
FCSimplex branch merge
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 */ |