From 82e8079f6f83369c99a1535e6c16c0db33f0db85 Mon Sep 17 00:00:00 2001 From: msoos Date: Tue, 1 Dec 2009 22:35:14 +0000 Subject: [PATCH] CryptoMiniSat2 is using the same MTL and MTRand directory as that of CryptoMiniSat1. This is made explicit by the Makefile's -I directives. Therefore, there is no need to have it twice in the source tree. Also, some files in CryptoMiniSat2 have been changed to have 'mtl/' in front of their #include directives. This was superflous, as the Makefile already -I includes the ../cryptominisat/mtl and ../cryptominisat/MTRand directories in the search path.Effectively, with 'mtl' directory in, and the #include 'mtl/X.h', it was compiler-implementation specific which file was included (either cryptominisat/mtl/X.h or cryptominisat2/mtl/X.h), therefore potentially making debugging next to impossible and the build fragile in the future (if ever the two mtl directories will be different) git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@439 e59a4935-1847-0410-ae03-e826735625c1 --- src/sat/cryptominisat2/Clause.h | 2 +- src/sat/cryptominisat2/Logger.h | 6 +- .../cryptominisat2/MTRand/MersenneTwister.h | 427 ------------------ src/sat/cryptominisat2/PackedRow.h | 2 +- src/sat/cryptominisat2/Solver.h | 6 +- src/sat/cryptominisat2/SolverTypes.h | 2 +- src/sat/cryptominisat2/VarReplacer.h | 2 +- src/sat/cryptominisat2/mtl/Alg.h | 62 --- src/sat/cryptominisat2/mtl/BasicHeap.h | 102 ----- src/sat/cryptominisat2/mtl/BoxedVec.h | 151 ------- src/sat/cryptominisat2/mtl/Heap.h | 173 ------- src/sat/cryptominisat2/mtl/Map.h | 122 ----- src/sat/cryptominisat2/mtl/Queue.h | 87 ---- src/sat/cryptominisat2/mtl/Sort.h | 94 ---- src/sat/cryptominisat2/mtl/Vec.h | 135 ------ 15 files changed, 10 insertions(+), 1363 deletions(-) delete mode 100644 src/sat/cryptominisat2/MTRand/MersenneTwister.h delete mode 100644 src/sat/cryptominisat2/mtl/Alg.h delete mode 100644 src/sat/cryptominisat2/mtl/BasicHeap.h delete mode 100644 src/sat/cryptominisat2/mtl/BoxedVec.h delete mode 100644 src/sat/cryptominisat2/mtl/Heap.h delete mode 100644 src/sat/cryptominisat2/mtl/Map.h delete mode 100644 src/sat/cryptominisat2/mtl/Queue.h delete mode 100644 src/sat/cryptominisat2/mtl/Sort.h delete mode 100644 src/sat/cryptominisat2/mtl/Vec.h diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h index 42e1b7e..a6768f9 100644 --- a/src/sat/cryptominisat2/Clause.h +++ b/src/sat/cryptominisat2/Clause.h @@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include #include -#include "mtl/Vec.h" +#include "Vec.h" #include "SolverTypes.h" #include "PackedRow.h" diff --git a/src/sat/cryptominisat2/Logger.h b/src/sat/cryptominisat2/Logger.h index 19bac10..f4caffa 100644 --- a/src/sat/cryptominisat2/Logger.h +++ b/src/sat/cryptominisat2/Logger.h @@ -26,9 +26,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include -#include "mtl/Vec.h" -#include "mtl/Heap.h" -#include "mtl/Alg.h" +#include "Vec.h" +#include "Heap.h" +#include "Alg.h" #include "SolverTypes.h" #include "stdint.h" #include "limits.h" diff --git a/src/sat/cryptominisat2/MTRand/MersenneTwister.h b/src/sat/cryptominisat2/MTRand/MersenneTwister.h deleted file mode 100644 index 964ecc7..0000000 --- a/src/sat/cryptominisat2/MTRand/MersenneTwister.h +++ /dev/null @@ -1,427 +0,0 @@ -// MersenneTwister.h -// Mersenne Twister random number generator -- a C++ class MTRand -// Based on code by Makoto Matsumoto, Takuji Nishimura, and Shawn Cokus -// Richard J. Wagner v1.0 15 May 2003 rjwagner@writeme.com - -// The Mersenne Twister is an algorithm for generating random numbers. It -// was designed with consideration of the flaws in various other generators. -// The period, 2^19937-1, and the order of equidistribution, 623 dimensions, -// are far greater. The generator is also fast; it avoids multiplication and -// division, and it benefits from caches and pipelines. For more information -// see the inventors' web page at http://www.math.keio.ac.jp/~matumoto/emt.html - -// Reference -// M. Matsumoto and T. Nishimura, "Mersenne Twister: A 623-Dimensionally -// Equidistributed Uniform Pseudo-Random Number Generator", ACM Transactions on -// Modeling and Computer Simulation, Vol. 8, No. 1, January 1998, pp 3-30. - -// Copyright (C) 1997 - 2002, Makoto Matsumoto and Takuji Nishimura, -// Copyright (C) 2000 - 2003, Richard J. Wagner -// All rights reserved. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions -// are met: -// -// 1. Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// -// 2. Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// -// 3. The names of its contributors may not be used to endorse or promote -// products derived from this software without specific prior written -// permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR -// CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - -// The original code included the following notice: -// -// When you use this, send an email to: matumoto@math.keio.ac.jp -// with an appropriate reference to your work. -// -// It would be nice to CC: rjwagner@writeme.com and Cokus@math.washington.edu -// when you write. - -#ifndef MERSENNETWISTER_H -#define MERSENNETWISTER_H - -#include -#include -#include -#include -#include - -namespace MINISAT -{ - -// Not thread safe (unless auto-initialization is avoided and each thread has -// its own MTRand object) - -class MTRand { -// Data -public: - typedef unsigned long uint32; // unsigned integer type, at least 32 bits - - enum { N = 624 }; // length of state vector - enum { SAVE = N + 1 }; // length of array for save() - -protected: - enum { M = 397 }; // period parameter - - uint32 state[N]; // internal state - uint32 *pNext; // next value to get from state - int left; // number of values left before reload needed - - -//Methods -public: - MTRand( const uint32& oneSeed ); // initialize with a simple uint32 - MTRand( uint32 *const bigSeed, uint32 const seedLength = N ); // or an array - MTRand(); // auto-initialize with /dev/urandom or time() and clock() - - // Do NOT use for CRYPTOGRAPHY without securely hashing several returned - // values together, otherwise the generator state can be learned after - // reading 624 consecutive values. - - // Access to 32-bit random numbers - double rand(); // real number in [0,1] - double rand( const double& n ); // real number in [0,n] - double randExc(); // real number in [0,1) - double randExc( const double& n ); // real number in [0,n) - double randDblExc(); // real number in (0,1) - double randDblExc( const double& n ); // real number in (0,n) - uint32 randInt(); // integer in [0,2^32-1] - uint32 randInt( const uint32& n ); // integer in [0,n] for n < 2^32 - double operator()() { return rand(); } // same as rand() - - // Access to 53-bit random numbers (capacity of IEEE double precision) - double rand53(); // real number in [0,1) - - // Access to nonuniform random number distributions - double randNorm( const double& mean = 0.0, const double& variance = 0.0 ); - - // Re-seeding functions with same behavior as initializers - void seed( const uint32 oneSeed ); - void seed( uint32 *const bigSeed, const uint32 seedLength = N ); - void seed(); - - // Saving and loading generator state - void save( uint32* saveArray ) const; // to array of size SAVE - void load( uint32 *const loadArray ); // from such array - friend std::ostream& operator<<( std::ostream& os, const MTRand& mtrand ); - friend std::istream& operator>>( std::istream& is, MTRand& mtrand ); - -protected: - void initialize( const uint32 oneSeed ); - void reload(); - uint32 hiBit( const uint32& u ) const { return u & 0x80000000UL; } - uint32 loBit( const uint32& u ) const { return u & 0x00000001UL; } - uint32 loBits( const uint32& u ) const { return u & 0x7fffffffUL; } - uint32 mixBits( const uint32& u, const uint32& v ) const - { return hiBit(u) | loBits(v); } - uint32 twist( const uint32& m, const uint32& s0, const uint32& s1 ) const - { return m ^ (mixBits(s0,s1)>>1) ^ (-loBit(s1) & 0x9908b0dfUL); } - static uint32 hash( time_t t, clock_t c ); -}; - - -inline MTRand::MTRand( const uint32& oneSeed ) - { seed(oneSeed); } - -inline MTRand::MTRand( uint32 *const bigSeed, const uint32 seedLength ) - { seed(bigSeed,seedLength); } - -inline MTRand::MTRand() - { seed(); } - -inline double MTRand::rand() - { return double(randInt()) * (1.0/4294967295.0); } - -inline double MTRand::rand( const double& n ) - { return rand() * n; } - -inline double MTRand::randExc() - { return double(randInt()) * (1.0/4294967296.0); } - -inline double MTRand::randExc( const double& n ) - { return randExc() * n; } - -inline double MTRand::randDblExc() - { return ( double(randInt()) + 0.5 ) * (1.0/4294967296.0); } - -inline double MTRand::randDblExc( const double& n ) - { return randDblExc() * n; } - -inline double MTRand::rand53() -{ - uint32 a = randInt() >> 5, b = randInt() >> 6; - return ( a * 67108864.0 + b ) * (1.0/9007199254740992.0); // by Isaku Wada -} - -inline double MTRand::randNorm( const double& mean, const double& variance ) -{ - // Return a real number from a normal (Gaussian) distribution with given - // mean and variance by Box-Muller method - double r = sqrt( -2.0 * log( 1.0-randDblExc()) ) * variance; - double phi = 2.0 * 3.14159265358979323846264338328 * randExc(); - return mean + r * cos(phi); -} - -inline MTRand::uint32 MTRand::randInt() -{ - // Pull a 32-bit integer from the generator state - // Every other access function simply transforms the numbers extracted here - - if( left == 0 ) reload(); - --left; - - register uint32 s1; - s1 = *pNext++; - s1 ^= (s1 >> 11); - s1 ^= (s1 << 7) & 0x9d2c5680UL; - s1 ^= (s1 << 15) & 0xefc60000UL; - return ( s1 ^ (s1 >> 18) ); -} - -inline MTRand::uint32 MTRand::randInt( const uint32& n ) -{ - // Find which bits are used in n - // Optimized by Magnus Jonsson (magnus@smartelectronix.com) - uint32 used = n; - used |= used >> 1; - used |= used >> 2; - used |= used >> 4; - used |= used >> 8; - used |= used >> 16; - - // Draw numbers until one is found in [0,n] - uint32 i; - do - i = randInt() & used; // toss unused bits to shorten search - while( i > n ); - return i; -} - - -inline void MTRand::seed( const uint32 oneSeed ) -{ - // Seed the generator with a simple uint32 - initialize(oneSeed); - reload(); -} - - -inline void MTRand::seed( uint32 *const bigSeed, const uint32 seedLength ) -{ - // Seed the generator with an array of uint32's - // There are 2^19937-1 possible initial states. This function allows - // all of those to be accessed by providing at least 19937 bits (with a - // default seed length of N = 624 uint32's). Any bits above the lower 32 - // in each element are discarded. - // Just call seed() if you want to get array from /dev/urandom - initialize(19650218UL); - register int i = 1; - register uint32 j = 0; - register int k = ( N > seedLength ? N : seedLength ); - for( ; k; --k ) - { - state[i] = - state[i] ^ ( (state[i-1] ^ (state[i-1] >> 30)) * 1664525UL ); - state[i] += ( bigSeed[j] & 0xffffffffUL ) + j; - state[i] &= 0xffffffffUL; - ++i; ++j; - if( i >= N ) { state[0] = state[N-1]; i = 1; } - if( j >= seedLength ) j = 0; - } - for( k = N - 1; k; --k ) - { - state[i] = - state[i] ^ ( (state[i-1] ^ (state[i-1] >> 30)) * 1566083941UL ); - state[i] -= i; - state[i] &= 0xffffffffUL; - ++i; - if( i >= N ) { state[0] = state[N-1]; i = 1; } - } - state[0] = 0x80000000UL; // MSB is 1, assuring non-zero initial array - reload(); -} - - -inline void MTRand::seed() -{ - // Seed the generator with an array from /dev/urandom if available - // Otherwise use a hash of time() and clock() values - - // First try getting an array from /dev/urandom - FILE* urandom = fopen( "/dev/urandom", "rb" ); - if( urandom ) - { - uint32 bigSeed[N]; - register uint32 *s = bigSeed; - register int i = N; - register bool success = true; - while( success && i-- ) - success = fread( s++, sizeof(uint32), 1, urandom ); - fclose(urandom); - if( success ) { seed( bigSeed, N ); return; } - } - - // Was not successful, so use time() and clock() instead - seed( hash( time(NULL), clock() ) ); -} - - -inline void MTRand::initialize( const uint32 seed ) -{ - // Initialize generator state with seed - // See Knuth TAOCP Vol 2, 3rd Ed, p.106 for multiplier. - // In previous versions, most significant bits (MSBs) of the seed affect - // only MSBs of the state array. Modified 9 Jan 2002 by Makoto Matsumoto. - register uint32 *s = state; - register uint32 *r = state; - register int i = 1; - *s++ = seed & 0xffffffffUL; - for( ; i < N; ++i ) - { - *s++ = ( 1812433253UL * ( *r ^ (*r >> 30) ) + i ) & 0xffffffffUL; - r++; - } -} - - -inline void MTRand::reload() -{ - // Generate N new values in state - // Made clearer and faster by Matthew Bellew (matthew.bellew@home.com) - register uint32 *p = state; - register int i; - for( i = N - M; i--; ++p ) - *p = twist( p[M], p[0], p[1] ); - for( i = M; --i; ++p ) - *p = twist( p[M-N], p[0], p[1] ); - *p = twist( p[M-N], p[0], state[0] ); - - left = N, pNext = state; -} - - -inline MTRand::uint32 MTRand::hash( time_t t, clock_t c ) -{ - // Get a uint32 from t and c - // Better than uint32(x) in case x is floating point in [0,1] - // Based on code by Lawrence Kirby (fred@genesis.demon.co.uk) - - static uint32 differ = 0; // guarantee time-based seeds will change - - uint32 h1 = 0; - unsigned char *p = (unsigned char *) &t; - for( size_t i = 0; i < sizeof(t); ++i ) - { - h1 *= UCHAR_MAX + 2U; - h1 += p[i]; - } - uint32 h2 = 0; - p = (unsigned char *) &c; - for( size_t j = 0; j < sizeof(c); ++j ) - { - h2 *= UCHAR_MAX + 2U; - h2 += p[j]; - } - return ( h1 + differ++ ) ^ h2; -} - - -inline void MTRand::save( uint32* saveArray ) const -{ - register uint32 *sa = saveArray; - register const uint32 *s = state; - register int i = N; - for( ; i--; *sa++ = *s++ ) {} - *sa = left; -} - - -inline void MTRand::load( uint32 *const loadArray ) -{ - register uint32 *s = state; - register uint32 *la = loadArray; - register int i = N; - for( ; i--; *s++ = *la++ ) {} - left = *la; - pNext = &state[N-left]; -} - - -inline std::ostream& operator<<( std::ostream& os, const MTRand& mtrand ) -{ - register const MTRand::uint32 *s = mtrand.state; - register int i = mtrand.N; - for( ; i--; os << *s++ << "\t" ) {} - return os << mtrand.left; -} - - -inline std::istream& operator>>( std::istream& is, MTRand& mtrand ) -{ - register MTRand::uint32 *s = mtrand.state; - register int i = mtrand.N; - for( ; i--; is >> *s++ ) {} - is >> mtrand.left; - mtrand.pNext = &mtrand.state[mtrand.N-mtrand.left]; - return is; -} -}; - -#endif // MERSENNETWISTER_H - -// Change log: -// -// v0.1 - First release on 15 May 2000 -// - Based on code by Makoto Matsumoto, Takuji Nishimura, and Shawn Cokus -// - Translated from C to C++ -// - Made completely ANSI compliant -// - Designed convenient interface for initialization, seeding, and -// obtaining numbers in default or user-defined ranges -// - Added automatic seeding from /dev/urandom or time() and clock() -// - Provided functions for saving and loading generator state -// -// v0.2 - Fixed bug which reloaded generator one step too late -// -// v0.3 - Switched to clearer, faster reload() code from Matthew Bellew -// -// v0.4 - Removed trailing newline in saved generator format to be consistent -// with output format of built-in types -// -// v0.5 - Improved portability by replacing static const int's with enum's and -// clarifying return values in seed(); suggested by Eric Heimburg -// - Removed MAXINT constant; use 0xffffffffUL instead -// -// v0.6 - Eliminated seed overflow when uint32 is larger than 32 bits -// - Changed integer [0,n] generator to give better uniformity -// -// v0.7 - Fixed operator precedence ambiguity in reload() -// - Added access for real numbers in (0,1) and (0,n) -// -// v0.8 - Included time.h header to properly support time_t and clock_t -// -// v1.0 - Revised seeding to match 26 Jan 2002 update of Nishimura and Matsumoto -// - Allowed for seeding with arrays of any length -// - Added access for real numbers in [0,1) with 53-bit resolution -// - Added access for real numbers from normal (Gaussian) distributions -// - Increased overall speed by optimizing twist() -// - Doubled speed of integer [0,n] generation -// - Fixed out-of-range number generation on 64-bit machines -// - Improved portability by substituting literal constants for long enum's -// - Changed license from GNU LGPL to BSD diff --git a/src/sat/cryptominisat2/PackedRow.h b/src/sat/cryptominisat2/PackedRow.h index 2184ae4..795f0c1 100644 --- a/src/sat/cryptominisat2/PackedRow.h +++ b/src/sat/cryptominisat2/PackedRow.h @@ -23,7 +23,7 @@ along with this program. If not, see . #include #include #include "SolverTypes.h" -#include "mtl/Vec.h" +#include "Vec.h" #include #include #include diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 51e71e7..95564c2 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -25,9 +25,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include -#include "mtl/Vec.h" -#include "mtl/Heap.h" -#include "mtl/Alg.h" +#include "Vec.h" +#include "Heap.h" +#include "Alg.h" #include "MTRand/MersenneTwister.h" #include "SolverTypes.h" #include "Clause.h" diff --git a/src/sat/cryptominisat2/SolverTypes.h b/src/sat/cryptominisat2/SolverTypes.h index c95be2e..7499c56 100644 --- a/src/sat/cryptominisat2/SolverTypes.h +++ b/src/sat/cryptominisat2/SolverTypes.h @@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include -#include "mtl/Alg.h" +#include "Alg.h" namespace MINISAT { diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h index 87743b8..3d11ff0 100644 --- a/src/sat/cryptominisat2/VarReplacer.h +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -3,7 +3,7 @@ #include "SolverTypes.h" #include "Clause.h" -#include "mtl/Vec.h" +#include "Vec.h" #include #include diff --git a/src/sat/cryptominisat2/mtl/Alg.h b/src/sat/cryptominisat2/mtl/Alg.h deleted file mode 100644 index 58fc50a..0000000 --- a/src/sat/cryptominisat2/mtl/Alg.h +++ /dev/null @@ -1,62 +0,0 @@ -/*******************************************************************************************[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 Alg_h -#define Alg_h - -namespace MINISAT -{ - -//================================================================================================= -// Useful functions on vectors - - -#if 1 -template -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 -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 -static inline bool find(V& ts, const T& t) -{ - int j = 0; - for (; j < ts.size() && ts[j] != t; j++); - return j < ts.size(); -} - -}; - -#endif diff --git a/src/sat/cryptominisat2/mtl/BasicHeap.h b/src/sat/cryptominisat2/mtl/BasicHeap.h deleted file mode 100644 index 4a34e77..0000000 --- a/src/sat/cryptominisat2/mtl/BasicHeap.h +++ /dev/null @@ -1,102 +0,0 @@ -/******************************************************************************************[Heap.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 BasicHeap_h -#define BasicHeap_h -#include "Vec.h" - - -namespace MINISAT -{ - -//================================================================================================= -// A heap implementation with support for decrease/increase key. - - -template -class BasicHeap { - Comp lt; - vec heap; // heap of ints - - // Index "traversal" functions - static inline int left (int i) { return i*2+1; } - static inline int right (int i) { return (i+1)*2; } - static inline int parent(int i) { return (i-1) >> 1; } - - inline void percolateUp(int i) - { - int x = heap[i]; - while (i != 0 && lt(x, heap[parent(i)])){ - heap[i] = heap[parent(i)]; - i = parent(i); - } - heap [i] = x; - } - - - inline void percolateDown(int i) - { - int x = heap[i]; - while (left(i) < heap.size()){ - int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i); - if (!lt(heap[child], x)) break; - heap[i] = heap[child]; - i = child; - } - heap[i] = x; - } - - - bool heapProperty(int i) { - return i >= heap.size() - || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); } - - - public: - BasicHeap(const C& c) : comp(c) { } - - int size () const { return heap.size(); } - bool empty () const { return heap.size() == 0; } - int operator[](int index) const { return heap[index+1]; } - void clear (bool dealloc = false) { heap.clear(dealloc); } - void insert (int n) { heap.push(n); percolateUp(heap.size()-1); } - - - int removeMin() { - int r = heap[0]; - heap[0] = heap.last(); - heap.pop(); - if (heap.size() > 1) percolateDown(0); - return r; - } - - - // DEBUG: consistency checking - bool heapProperty() { - return heapProperty(1); } - - - // COMPAT: should be removed - int getmin () { return removeMin(); } -}; - -}; - -//================================================================================================= -#endif diff --git a/src/sat/cryptominisat2/mtl/BoxedVec.h b/src/sat/cryptominisat2/mtl/BoxedVec.h deleted file mode 100644 index 3178856..0000000 --- a/src/sat/cryptominisat2/mtl/BoxedVec.h +++ /dev/null @@ -1,151 +0,0 @@ -/*******************************************************************************************[Vec.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 BoxedVec_h -#define BoxedVec_h - -#include -#include -#include - -namespace MINISAT -{ - -//================================================================================================= -// Automatically resizable arrays -// -// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) - -template -class bvec { - - static inline int imin(int x, int y) { - int mask = (x-y) >> (sizeof(int)*8-1); - return (x&mask) + (y&(~mask)); } - - static inline int imax(int x, int y) { - int mask = (y-x) >> (sizeof(int)*8-1); - return (x&mask) + (y&(~mask)); } - - struct Vec_t { - int sz; - int cap; - T data[0]; - - static Vec_t* alloc(Vec_t* x, int size){ - x = (Vec_t*)realloc((void*)x, sizeof(Vec_t) + sizeof(T)*size); - x->cap = size; - return x; - } - - }; - - Vec_t* ref; - - static const int init_size = 2; - static int nextSize (int current) { return (current * 3 + 1) >> 1; } - static int fitSize (int needed) { int x; for (x = init_size; needed > x; x = nextSize(x)); return x; } - - void fill (int size) { - assert(ref != NULL); - for (T* i = ref->data; i < ref->data + size; i++) - new (i) T(); - } - - void fill (int size, const T& pad) { - assert(ref != NULL); - for (T* i = ref->data; i < ref->data + size; i++) - new (i) T(pad); - } - - // Don't allow copying (error prone): - altvec& operator = (altvec& other) { assert(0); } - altvec (altvec& other) { assert(0); } - -public: - void clear (bool dealloc = false) { - if (ref != NULL){ - for (int i = 0; i < ref->sz; i++) - (*ref).data[i].~T(); - - if (dealloc) { - free(ref); ref = NULL; - }else - ref->sz = 0; - } - } - - // Constructors: - altvec(void) : ref (NULL) { } - altvec(int size) : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size); ref->sz = size; } - altvec(int size, const T& pad) : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size, pad); ref->sz = size; } - ~altvec(void) { clear(true); } - - // Ownership of underlying array: - operator T* (void) { return ref->data; } // (unsafe but convenient) - operator const T* (void) const { return ref->data; } - - // Size operations: - int size (void) const { return ref != NULL ? ref->sz : 0; } - - void pop (void) { assert(ref != NULL && ref->sz > 0); int last = --ref->sz; ref->data[last].~T(); } - void push (const T& elem) { - int size = ref != NULL ? ref->sz : 0; - int cap = ref != NULL ? ref->cap : 0; - if (size == cap){ - cap = cap != 0 ? nextSize(cap) : init_size; - ref = Vec_t::alloc(ref, cap); - } - //new (&ref->data[size]) T(elem); - ref->data[size] = elem; - ref->sz = size+1; - } - - void push () { - int size = ref != NULL ? ref->sz : 0; - int cap = ref != NULL ? ref->cap : 0; - if (size == cap){ - cap = cap != 0 ? nextSize(cap) : init_size; - ref = Vec_t::alloc(ref, cap); - } - new (&ref->data[size]) T(); - ref->sz = size+1; - } - - void shrink (int nelems) { for (int i = 0; i < nelems; i++) pop(); } - void shrink_(int nelems) { for (int i = 0; i < nelems; i++) pop(); } - void growTo (int size) { while (this->size() < size) push(); } - void growTo (int size, const T& pad) { while (this->size() < size) push(pad); } - void capacity (int size) { growTo(size); } - - const T& last (void) const { return ref->data[ref->sz-1]; } - T& last (void) { return ref->data[ref->sz-1]; } - - // Vector interface: - const T& operator [] (int index) const { return ref->data[index]; } - T& operator [] (int index) { return ref->data[index]; } - - void copyTo(altvec& copy) const { copy.clear(); for (int i = 0; i < size(); i++) copy.push(ref->data[i]); } - void moveTo(altvec& dest) { dest.clear(true); dest.ref = ref; ref = NULL; } - -}; - -}; - -#endif diff --git a/src/sat/cryptominisat2/mtl/Heap.h b/src/sat/cryptominisat2/mtl/Heap.h deleted file mode 100644 index 6647a94..0000000 --- a/src/sat/cryptominisat2/mtl/Heap.h +++ /dev/null @@ -1,173 +0,0 @@ -/******************************************************************************************[Heap.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 Heap_h -#define Heap_h - -#include "Vec.h" - -namespace MINISAT -{ - -//================================================================================================= -// A heap implementation with support for decrease/increase key. - - -template -class Heap { - Comp lt; - vec heap; // heap of ints - vec indices; // int -> index in heap - - // Index "traversal" functions - static inline int left (int i) { return i*2+1; } - static inline int right (int i) { return (i+1)*2; } - static inline int parent(int i) { return (i-1) >> 1; } - - - inline void percolateUp(int i) - { - int x = heap[i]; - while (i != 0 && lt(x, heap[parent(i)])){ - heap[i] = heap[parent(i)]; - indices[heap[i]] = i; - i = parent(i); - } - heap [i] = x; - indices[x] = i; - } - - - inline void percolateDown(int i) - { - int x = heap[i]; - while (left(i) < heap.size()){ - int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i); - if (!lt(heap[child], x)) break; - heap[i] = heap[child]; - indices[heap[i]] = i; - i = child; - } - heap [i] = x; - indices[x] = i; - } - - - bool heapProperty (int i) const { - return i >= heap.size() - || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); } - - - public: - Heap(const Comp& c) : lt(c) { } - - int size () const { return heap.size(); } - bool empty () const { return heap.size() == 0; } - bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; } - int operator[](int index) const { assert(index < heap.size()); return heap[index]; } - - void decrease (int n) { assert(inHeap(n)); percolateUp(indices[n]); } - - // RENAME WHEN THE DEPRECATED INCREASE IS REMOVED. - void increase_ (int n) { assert(inHeap(n)); percolateDown(indices[n]); } - - - void insert(int n) - { - indices.growTo(n+1, -1); - assert(!inHeap(n)); - - indices[n] = heap.size(); - heap.push(n); - percolateUp(indices[n]); - } - - - int removeMin() - { - int x = heap[0]; - heap[0] = heap.last(); - indices[heap[0]] = 0; - indices[x] = -1; - heap.pop(); - if (heap.size() > 1) percolateDown(0); - return x; - } - - - void clear(bool dealloc = false) - { - for (int i = 0; i < heap.size(); i++) - indices[heap[i]] = -1; -#ifdef NDEBUG - for (int i = 0; i < indices.size(); i++) - assert(indices[i] == -1); -#endif - heap.clear(dealloc); - } - - - // Fool proof variant of insert/decrease/increase - void update (int n) - { - if (!inHeap(n)) - insert(n); - else { - percolateUp(indices[n]); - percolateDown(indices[n]); - } - } - - - // Delete elements from the heap using a given filter function (-object). - // *** this could probaly be replaced with a more general "buildHeap(vec&)" method *** - template - void filter(const F& filt) { - int i,j; - for (i = j = 0; i < heap.size(); i++) - if (filt(heap[i])){ - heap[j] = heap[i]; - indices[heap[i]] = j++; - }else - indices[heap[i]] = -1; - - heap.shrink(i - j); - for (int i = heap.size() / 2 - 1; i >= 0; i--) - percolateDown(i); - - assert(heapProperty()); - } - - - // DEBUG: consistency checking - bool heapProperty() const { - return heapProperty(1); } - - - // COMPAT: should be removed - void setBounds (int n) { } - void increase (int n) { decrease(n); } - int getmin () { return removeMin(); } - -}; - -}; - -//================================================================================================= -#endif diff --git a/src/sat/cryptominisat2/mtl/Map.h b/src/sat/cryptominisat2/mtl/Map.h deleted file mode 100644 index 302069a..0000000 --- a/src/sat/cryptominisat2/mtl/Map.h +++ /dev/null @@ -1,122 +0,0 @@ -/*******************************************************************************************[Map.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 Map_h -#define Map_h - -#include -#include "Vec.h" - -namespace MINISAT -{ - -//================================================================================================= -// Default hash/equals functions -// - -template struct Hash { uint32_t operator()(const K& k) const { return hash(k); } }; -template struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } }; - -template struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } }; -template struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } }; - -//================================================================================================= -// Some primes -// - -static const int nprimes = 25; -static const int primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 }; - -//================================================================================================= -// Hash table implementation of Maps -// - -template, class E = Equal > -class Map { - struct Pair { K key; D data; }; - - H hash; - E equals; - - vec* table; - int cap; - int size; - - // Don't allow copying (error prone): - Map& operator = (Map& other) { assert(0); } - Map (Map& other) { assert(0); } - - int32_t index (const K& k) const { return hash(k) % cap; } - void _insert (const K& k, const D& d) { table[index(k)].push(); table[index(k)].last().key = k; table[index(k)].last().data = d; } - void rehash () { - const vec* old = table; - - int newsize = primes[0]; - for (int i = 1; newsize <= cap && i < nprimes; i++) - newsize = primes[i]; - - table = new vec[newsize]; - - for (int i = 0; i < cap; i++){ - for (int j = 0; j < old[i].size(); j++){ - _insert(old[i][j].key, old[i][j].data); }} - - delete [] old; - - cap = newsize; - } - - - public: - - Map () : table(NULL), cap(0), size(0) {} - Map (const H& h, const E& e) : Map(), hash(h), equals(e) {} - ~Map () { delete [] table; } - - void insert (const K& k, const D& d) { if (size+1 > cap / 2) rehash(); _insert(k, d); size++; } - bool peek (const K& k, D& d) { - if (size == 0) return false; - const vec& ps = table[index(k)]; - for (int i = 0; i < ps.size(); i++) - if (equals(ps[i].key, k)){ - d = ps[i].data; - return true; } - return false; - } - - void remove (const K& k) { - assert(table != NULL); - vec& ps = table[index(k)]; - int j = 0; - for (; j < ps.size() && !equals(ps[j].key, k); j++); - assert(j < ps.size()); - ps[j] = ps.last(); - ps.pop(); - } - - void clear () { - cap = size = 0; - delete [] table; - table = NULL; - } -}; - -}; - -#endif diff --git a/src/sat/cryptominisat2/mtl/Queue.h b/src/sat/cryptominisat2/mtl/Queue.h deleted file mode 100644 index 52f8fb2..0000000 --- a/src/sat/cryptominisat2/mtl/Queue.h +++ /dev/null @@ -1,87 +0,0 @@ -/*****************************************************************************************[Queue.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 Queue_h -#define Queue_h - -#include "Vec.h" - -namespace MINISAT -{ - -//================================================================================================= - - -template -class Queue { - vec elems; - int first; - -public: - Queue(void) : first(0) { } - - void insert(T x) { elems.push(x); } - T peek () const { return elems[first]; } - void pop () { first++; } - - void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; } - int size(void) { return elems.size() - first; } - - //bool has(T x) { for (int i = first; i < elems.size(); i++) if (elems[i] == x) return true; return false; } - - const T& operator [] (int index) const { return elems[first + index]; } - -}; - -//template -//class Queue { -// vec buf; -// int first; -// int end; -// -//public: -// typedef T Key; -// -// Queue() : buf(1), first(0), end(0) {} -// -// void clear () { buf.shrinkTo(1); first = end = 0; } -// int size () { return (end >= first) ? end - first : end - first + buf.size(); } -// -// T peek () { assert(first != end); return buf[first]; } -// void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; } -// void insert(T elem) { // INVARIANT: buf[end] is always unused -// buf[end++] = elem; -// if (end == buf.size()) end = 0; -// if (first == end){ // Resize: -// vec tmp((buf.size()*3 + 1) >> 1); -// //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0); -// int i = 0; -// for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j]; -// for (int j = 0 ; j < end ; j++) tmp[i++] = buf[j]; -// first = 0; -// end = buf.size(); -// tmp.moveTo(buf); -// } -// } -//}; - -}; - -//================================================================================================= -#endif diff --git a/src/sat/cryptominisat2/mtl/Sort.h b/src/sat/cryptominisat2/mtl/Sort.h deleted file mode 100644 index 76f168f..0000000 --- a/src/sat/cryptominisat2/mtl/Sort.h +++ /dev/null @@ -1,94 +0,0 @@ -/******************************************************************************************[Sort.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 Sort_h -#define Sort_h -#include "Vec.h" - -namespace MINISAT -{ -//================================================================================================= -// Some sorting algorithms for vec's - - -template -struct LessThan_default { - bool operator () (T x, T y) { return x < y; } -}; - - -template -void selectionSort(T* array, int size, LessThan lt) -{ - int i, j, best_i; - T tmp; - - for (i = 0; i < size-1; i++){ - best_i = i; - for (j = i+1; j < size; j++){ - if (lt(array[j], array[best_i])) - best_i = j; - } - tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; - } -} -template static inline void selectionSort(T* array, int size) { - selectionSort(array, size, LessThan_default()); } - -template -void sort(T* array, int size, LessThan lt) -{ - if (size <= 15) - selectionSort(array, size, lt); - - else{ - T pivot = array[size / 2]; - T tmp; - int i = -1; - int j = size; - - for(;;){ - do i++; while(lt(array[i], pivot)); - do j--; while(lt(pivot, array[j])); - - if (i >= j) break; - - tmp = array[i]; array[i] = array[j]; array[j] = tmp; - } - - sort(array , i , lt); - sort(&array[i], size-i, lt); - } -} -template static inline void sort(T* array, int size) { - sort(array, size, LessThan_default()); } - - -//================================================================================================= -// For 'vec's: - - -template void sort(vec& v, LessThan lt) { - sort(v.getData(), v.size(), lt); } -template void sort(vec& v) { - sort(v, LessThan_default()); } - -}; -//================================================================================================= -#endif diff --git a/src/sat/cryptominisat2/mtl/Vec.h b/src/sat/cryptominisat2/mtl/Vec.h deleted file mode 100644 index a3c5fca..0000000 --- a/src/sat/cryptominisat2/mtl/Vec.h +++ /dev/null @@ -1,135 +0,0 @@ -/*******************************************************************************************[Vec.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 Vec_h -#define Vec_h -#include -#include -#include - -namespace MINISAT -{ -//================================================================================================= -// Automatically resizable arrays -// -// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) - -template -class vec { - T* data; - int sz; - int cap; - - void init(int size, const T& pad); - void grow(int min_cap); - - // Don't allow copying (error prone): - vec& operator = (vec& other) { assert(0); return *this; } - vec (vec& other) { assert(0); } - - static inline int imin(int x, int y) { - int mask = (x-y) >> (sizeof(int)*8-1); - return (x&mask) + (y&(~mask)); } - - static inline int imax(int x, int y) { - int mask = (y-x) >> (sizeof(int)*8-1); - return (x&mask) + (y&(~mask)); } - -public: - // Types: - typedef int Key; - typedef T Datum; - - // Constructors: - vec(void) : data(NULL) , sz(0) , cap(0) { } - vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); } - vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); } - vec(T* array, int size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'free()') - ~vec(void) { clear(true); } - - // Ownership of underlying array: - T* release (void) { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; } - const T* getData() const {return data; } - T* getData() {return data; } - - // Size operations: - int size (void) const { return sz; } - void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); } - void shrink_(int nelems) { assert(nelems <= sz); sz -= nelems; } - void pop (void) { sz--, data[sz].~T(); } - void growTo (int size); - void growTo (int size, const T& pad); - void clear (bool dealloc = false); - void capacity (int size) { grow(size); } - - // Stack interface: -#if 1 - void push (void) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; } - //void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(elem); sz++; } - void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } data[sz++] = elem; } - void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; } -#else - void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; } - void push (const T& elem) { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; } -#endif - - const T& last (void) const { return data[sz-1]; } - T& last (void) { return data[sz-1]; } - - // Vector interface: - const T& operator [] (int index) const { return data[index]; } - T& operator [] (int index) { return data[index]; } - - - // Duplicatation (preferred instead): - void copyTo(vec& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); } - void moveTo(vec& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } -}; - -template -void vec::grow(int min_cap) { - if (min_cap <= cap) return; - if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2; - else do cap = (cap*3+1) >> 1; while (cap < min_cap); - data = (T*)realloc(data, cap * sizeof(T)); } - -template -void vec::growTo(int size, const T& pad) { - if (sz >= size) return; - grow(size); - for (int i = sz; i < size; i++) new (&data[i]) T(pad); - sz = size; } - -template -void vec::growTo(int size) { - if (sz >= size) return; - grow(size); - for (int i = sz; i < size; i++) new (&data[i]) T(); - sz = size; } - -template -void vec::clear(bool dealloc) { - if (data != NULL){ - for (int i = 0; i < sz; i++) data[i].~T(); - sz = 0; - if (dealloc) free(data), data = NULL, cap = 0; } } - -}; - -#endif -- 2.47.3