diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-12 20:38:10 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-12 20:38:10 +0000 |
commit | 13a6669a35aee32c03f8d29fe386aca95d2fbd8f (patch) | |
tree | b126afb6c384dd45db0249e8096cf733a74daa95 /src/sat/minisat/mtl/Alg.h | |
parent | 5b5474281c4cdc880bff8b9e38b84dc84f88e50c (diff) |
parser, minisat, other things..
Diffstat (limited to 'src/sat/minisat/mtl/Alg.h')
-rw-r--r-- | src/sat/minisat/mtl/Alg.h | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/src/sat/minisat/mtl/Alg.h b/src/sat/minisat/mtl/Alg.h new file mode 100644 index 000000000..a4ca4403b --- /dev/null +++ b/src/sat/minisat/mtl/Alg.h @@ -0,0 +1,63 @@ +/*******************************************************************************************[Alg.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef CVC4_MiniSat_Alg_h +#define CVC4_MiniSat_Alg_h + +namespace CVC4 { +namespace MiniSat { + +//================================================================================================= +// Useful functions on vectors + + +#if 1 +template<class V, class T> +static inline void remove(V& ts, const T& t) +{ + int j = 0; + for (; j < ts.size() && ts[j] != t; j++); + assert(j < ts.size()); + for (; j < ts.size()-1; j++) ts[j] = ts[j+1]; + ts.pop(); +} +#else +template<class V, class T> +static inline void remove(V& ts, const T& t) +{ + int j = 0; + for (; j < ts.size() && ts[j] != t; j++); + assert(j < ts.size()); + ts[j] = ts.last(); + ts.pop(); +} +#endif + +template<class V, class T> +static inline bool find(V& ts, const T& t) +{ + int j = 0; + for (; j < ts.size() && ts[j] != t; j++); + return j < ts.size(); +} + +}/* CVC4::MiniSat namespace */ +}/* CVC4 namespace */ + +#endif /* CVC4_MiniSat_Alg_h */ |