diff options
author | Tim King <taking@cs.nyu.edu> | 2010-10-23 21:47:47 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-10-23 21:47:47 +0000 |
commit | 237995ce0e7f47b826e26c0afb317cf5e3174879 (patch) | |
tree | ddeec96c8880ff186d350979f2a151179ae2d73f /src/theory/arith/basic.h | |
parent | 0a3ecb598dac9e5e7416f88403dbf73d558c8739 (diff) |
Removed slack.h, and arith_activity.h. Replaced IsBasicManager with the more general ArithVarDenseSet. Renamed NextArithRewriter to ArithRewriter.
Diffstat (limited to 'src/theory/arith/basic.h')
-rw-r--r-- | src/theory/arith/basic.h | 63 |
1 files changed, 0 insertions, 63 deletions
diff --git a/src/theory/arith/basic.h b/src/theory/arith/basic.h deleted file mode 100644 index c52e0881d..000000000 --- a/src/theory/arith/basic.h +++ /dev/null @@ -1,63 +0,0 @@ -/********************* */ -/*! \file basic.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 "expr/node.h" -#include "expr/attribute.h" - - -#ifndef __CVC4__THEORY__ARITH__BASIC_H -#define __CVC4__THEORY__ARITH__BASIC_H - -namespace CVC4 { -namespace theory { -namespace arith { - -class IsBasicManager { -private: - std::vector<bool> d_basic; - -public: - IsBasicManager() : d_basic() {} - - void init(ArithVar var, bool value){ - Assert(var == d_basic.size()); - d_basic.push_back(value); - } - - bool isBasic(ArithVar x) const{ - return d_basic[x]; - } - - void makeBasic(ArithVar x){ - Assert(!isBasic(x)); - d_basic[x] = true; - } - - void makeNonbasic(ArithVar x){ - Assert(isBasic(x)); - d_basic[x] = false; - } -}; - -}; /* namespace arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ - -#endif /* __CVC4__THEORY__ARITH__BASIC_H */ |