From: vijay_ganesh Date: Mon, 30 Nov 2009 19:50:46 +0000 (+0000) Subject: fixed compile/link issues with cryptominisat version 2.0 X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=d6ab2d5be6134e8eccb4ff7fdd7d6b6e52dcf582;p=francis%2Fstp.git fixed compile/link issues with cryptominisat version 2.0 git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@433 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/Makefile b/Makefile index 1f89b09..f19b67a 100644 --- a/Makefile +++ b/Makefile @@ -21,6 +21,9 @@ all: AST STPManager absrefine_counterexample to-sat simplifier printer c_interfa ifdef CRYPTOMINISAT $(MAKE) -C $(SRC)/sat cryptominisat endif +ifdef CRYPTOMINISAT2 + $(MAKE) -C $(SRC)/sat cryptominisat2 +endif ifdef CORE $(MAKE) -C $(SRC)/sat core endif diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 5272713..7dc15ff 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -21,7 +21,7 @@ CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT # OPTION to compile CRYPTOMiniSAT version 2.x #CRYPTOMINISAT2 = true -#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT +#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT2 # OPTION to compile MiniSAT #CORE = true diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 09cb519..d04d5ca 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -24,7 +24,7 @@ namespace BEEV { #ifdef CORE MINISAT::Solver NewSolver; #endif -#ifdef CRYPTOMINISAT +#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 MINISAT::Solver NewSolver; #endif #ifdef SIMP diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index 78d5f35..c74637d 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -715,7 +715,7 @@ namespace BEEV { if (!UserFlags.stats_flag) return; -#ifdef CRYPTOMINISAT +#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 #else double cpu_time = MINISAT::cpuTime(); uint64_t mem_used = MINISAT::memUsed(); diff --git a/src/main/Globals.h b/src/main/Globals.h index 7520196..235f139 100644 --- a/src/main/Globals.h +++ b/src/main/Globals.h @@ -23,7 +23,7 @@ namespace MINISAT { class Solver; -#if defined(CRYPTOMINISAT) +#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 #else typedef int Var; #endif diff --git a/src/sat/Makefile b/src/sat/Makefile index 28d11ff..439fb83 100644 --- a/src/sat/Makefile +++ b/src/sat/Makefile @@ -16,6 +16,11 @@ unsound: cryptominisat: $(MAKE) -C cryptominisat lib all +.PHONY: cryptominisat2 +cryptominisat2: + $(MAKE) -C cryptominisat2 lib all + + .PHONY: clean clean: rm -rf *.o *~ libminisat.a @@ -23,4 +28,5 @@ clean: $(MAKE) -C simp clean $(MAKE) -C unsound clean $(MAKE) -C cryptominisat clean + $(MAKE) -C cryptominisat2 clean diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h index a6768f9..42e1b7e 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 "Vec.h" +#include "mtl/Vec.h" #include "SolverTypes.h" #include "PackedRow.h" diff --git a/src/sat/cryptominisat2/Logger.h b/src/sat/cryptominisat2/Logger.h index 2564303..19bac10 100644 --- a/src/sat/cryptominisat2/Logger.h +++ b/src/sat/cryptominisat2/Logger.h @@ -22,14 +22,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include -#include #include #include #include -#include "Vec.h" -#include "Heap.h" -#include "Alg.h" +#include "mtl/Vec.h" +#include "mtl/Heap.h" +#include "mtl/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 new file mode 100644 index 0000000..964ecc7 --- /dev/null +++ b/src/sat/cryptominisat2/MTRand/MersenneTwister.h @@ -0,0 +1,427 @@ +// 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 795f0c1..2184ae4 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 "Vec.h" +#include "mtl/Vec.h" #include #include #include diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 37686d1..51e71e7 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -25,10 +25,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include -#include "Vec.h" -#include "Heap.h" -#include "Alg.h" -#include "MersenneTwister.h" +#include "mtl/Vec.h" +#include "mtl/Heap.h" +#include "mtl/Alg.h" +#include "MTRand/MersenneTwister.h" #include "SolverTypes.h" #include "Clause.h" #include "VarReplacer.h" @@ -36,6 +36,14 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Logger.h" #include "constants.h" +#ifdef _MSC_VER + #include +#else + #include + #include + #include +#endif + namespace MINISAT { using namespace MINISAT; diff --git a/src/sat/cryptominisat2/SolverTypes.h b/src/sat/cryptominisat2/SolverTypes.h index 7499c56..c95be2e 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 "Alg.h" +#include "mtl/Alg.h" namespace MINISAT { diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h index 3d11ff0..87743b8 100644 --- a/src/sat/cryptominisat2/VarReplacer.h +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -3,7 +3,7 @@ #include "SolverTypes.h" #include "Clause.h" -#include "Vec.h" +#include "mtl/Vec.h" #include #include diff --git a/src/sat/cryptominisat2/mtl/Alg.h b/src/sat/cryptominisat2/mtl/Alg.h new file mode 100644 index 0000000..58fc50a --- /dev/null +++ b/src/sat/cryptominisat2/mtl/Alg.h @@ -0,0 +1,62 @@ +/*******************************************************************************************[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 new file mode 100644 index 0000000..4a34e77 --- /dev/null +++ b/src/sat/cryptominisat2/mtl/BasicHeap.h @@ -0,0 +1,102 @@ +/******************************************************************************************[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 new file mode 100644 index 0000000..3178856 --- /dev/null +++ b/src/sat/cryptominisat2/mtl/BoxedVec.h @@ -0,0 +1,151 @@ +/*******************************************************************************************[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 new file mode 100644 index 0000000..6647a94 --- /dev/null +++ b/src/sat/cryptominisat2/mtl/Heap.h @@ -0,0 +1,173 @@ +/******************************************************************************************[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 new file mode 100644 index 0000000..302069a --- /dev/null +++ b/src/sat/cryptominisat2/mtl/Map.h @@ -0,0 +1,122 @@ +/*******************************************************************************************[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 new file mode 100644 index 0000000..52f8fb2 --- /dev/null +++ b/src/sat/cryptominisat2/mtl/Queue.h @@ -0,0 +1,87 @@ +/*****************************************************************************************[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 new file mode 100644 index 0000000..76f168f --- /dev/null +++ b/src/sat/cryptominisat2/mtl/Sort.h @@ -0,0 +1,94 @@ +/******************************************************************************************[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 new file mode 100644 index 0000000..a3c5fca --- /dev/null +++ b/src/sat/cryptominisat2/mtl/Vec.h @@ -0,0 +1,135 @@ +/*******************************************************************************************[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 diff --git a/src/sat/sat.h b/src/sat/sat.h index 4d3bdd9..e27a544 100644 --- a/src/sat/sat.h +++ b/src/sat/sat.h @@ -6,6 +6,11 @@ #include "cryptominisat/SolverTypes.h" #endif +#ifdef CRYPTOMINISAT2 +#include "cryptominisat2/Solver.h" +#include "cryptominisat2/SolverTypes.h" +#endif + #ifdef CORE #include "core/Solver.h" #include "core/SolverTypes.h" diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index b41d714..bb3c343 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -483,7 +483,7 @@ namespace BEEV x = info[varphi]; } -#ifdef CRYPTOMINISAT +#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 if(isXorChild) { setDoRenamePos(*x); @@ -636,7 +636,7 @@ namespace BEEV convertFormulaToCNFPosCases(varphi, defs); } -#ifdef CRYPTOMINISAT +#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 if ((x->clausespos != NULL && x->clausespos->size() > 1) || (doRenamePos(*x) && !wasVisited(*x))) @@ -1319,7 +1319,7 @@ namespace BEEV void CNFMgr::convertFormulaToCNFPosXOR(const ASTNode& varphi, ClauseList* defs) { -#ifdef CRYPTOMINISAT +#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 ASTVec::const_iterator it = varphi.GetChildren().begin(); ClausePtr xor_clause = new vector(); @@ -1683,7 +1683,7 @@ namespace BEEV ClauseList* defs) { //#ifdef FALSE -#ifdef CRYPTOMINISAT +#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 CNFInfo * xx = info[varphi]; if(NULL != xx && sharesPos(*xx) > 0 diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index aa0d65f..b807f2e 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -109,7 +109,7 @@ namespace BEEV // { // continue; // } -#ifdef CRYPTOMINISAT +#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 if(add_xor_clauses) { //cout << "addXorClause:\n"; @@ -131,7 +131,13 @@ namespace BEEV // << percentage << endl; bm->GetRunTimes()->stop(RunTimes::SendingToSAT); bm->GetRunTimes()->start(RunTimes::Solving); -#ifdef CRYPTOMINISAT + +#if defined CRYPTOMINISAT + if (newS.simplify() == MINISAT::l_Undef) +#endif + +#if defined CRYPTOMINISAT2 + newS.set_gaussian_decision_until(100); if (newS.simplify() == MINISAT::l_Undef) #endif newS.solve(); @@ -158,7 +164,8 @@ namespace BEEV bm->GetRunTimes()->stop(RunTimes::SendingToSAT); bm->GetRunTimes()->start(RunTimes::Solving); -#ifdef CRYPTOMINISAT + +#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 if (newS.simplify() == MINISAT::l_Undef) #endif newS.solve();