ifdef CRYPTOMINISAT
$(MAKE) -C $(SRC)/sat cryptominisat
endif
+ifdef CRYPTOMINISAT2
+ $(MAKE) -C $(SRC)/sat cryptominisat2
+endif
ifdef CORE
$(MAKE) -C $(SRC)/sat core
endif
# OPTION to compile CRYPTOMiniSAT version 2.x
#CRYPTOMINISAT2 = true
-#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT
+#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT2
# OPTION to compile MiniSAT
#CORE = true
#ifdef CORE
MINISAT::Solver NewSolver;
#endif
-#ifdef CRYPTOMINISAT
+#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
MINISAT::Solver NewSolver;
#endif
#ifdef SIMP
{
if (!UserFlags.stats_flag)
return;
-#ifdef CRYPTOMINISAT
+#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
#else
double cpu_time = MINISAT::cpuTime();
uint64_t mem_used = MINISAT::memUsed();
namespace MINISAT
{
class Solver;
-#if defined(CRYPTOMINISAT)
+#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
#else
typedef int Var;
#endif
cryptominisat:
$(MAKE) -C cryptominisat lib all
+.PHONY: cryptominisat2
+cryptominisat2:
+ $(MAKE) -C cryptominisat2 lib all
+
+
.PHONY: clean
clean:
rm -rf *.o *~ libminisat.a
$(MAKE) -C simp clean
$(MAKE) -C unsound clean
$(MAKE) -C cryptominisat clean
+ $(MAKE) -C cryptominisat2 clean
#include <cstdio>
#include <vector>
#include <sys/types.h>
-#include "Vec.h"
+#include "mtl/Vec.h"
#include "SolverTypes.h"
#include "PackedRow.h"
#include <stdio.h>
#include <set>
-#include <Vec.h>
#include <vector>
#include <string>
#include <map>
-#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"
--- /dev/null
+// 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 <iostream>
+#include <limits.h>
+#include <stdio.h>
+#include <time.h>
+#include <math.h>
+
+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
#include <vector>
#include <limits.h>
#include "SolverTypes.h"
-#include "Vec.h"
+#include "mtl/Vec.h"
#include <string.h>
#include <iostream>
#include <algorithm>
#include <cstdio>
#include <string.h>
-#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"
#include "Logger.h"
#include "constants.h"
+#ifdef _MSC_VER
+ #include <ctime>
+#else
+ #include <sys/time.h>
+ #include <sys/resource.h>
+ #include <unistd.h>
+#endif
+
namespace MINISAT
{
using namespace MINISAT;
#include <cassert>
#include <stdint.h>
-#include "Alg.h"
+#include "mtl/Alg.h"
namespace MINISAT
{
#include "SolverTypes.h"
#include "Clause.h"
-#include "Vec.h"
+#include "mtl/Vec.h"
#include <sys/types.h>
#include <map>
--- /dev/null
+/*******************************************************************************************[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<class V, class T>
+static inline void remove(V& ts, const T& t)
+{
+ int j = 0;
+ for (; j < ts.size() && ts[j] != t; j++);
+ assert(j < ts.size());
+ for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
+ ts.pop();
+}
+#else
+template<class V, class T>
+static inline void remove(V& ts, const T& t)
+{
+ int j = 0;
+ for (; j < ts.size() && ts[j] != t; j++);
+ assert(j < ts.size());
+ ts[j] = ts.last();
+ ts.pop();
+}
+#endif
+
+template<class V, class T>
+static inline bool find(V& ts, const T& t)
+{
+ int j = 0;
+ for (; j < ts.size() && ts[j] != t; j++);
+ return j < ts.size();
+}
+
+};
+
+#endif
--- /dev/null
+/******************************************************************************************[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 Comp>
+class BasicHeap {
+ Comp lt;
+ vec<int> 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
--- /dev/null
+/*******************************************************************************************[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 <cstdlib>
+#include <cassert>
+#include <new>
+
+namespace MINISAT
+{
+
+//=================================================================================================
+// Automatically resizable arrays
+//
+// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
+
+template<class T>
+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<T>& operator = (altvec<T>& other) { assert(0); }
+ altvec (altvec<T>& 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<T>& copy) const { copy.clear(); for (int i = 0; i < size(); i++) copy.push(ref->data[i]); }
+ void moveTo(altvec<T>& dest) { dest.clear(true); dest.ref = ref; ref = NULL; }
+
+};
+
+};
+
+#endif
--- /dev/null
+/******************************************************************************************[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 Comp>
+class Heap {
+ Comp lt;
+ vec<int> heap; // heap of ints
+ vec<int> 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<int>&)" method ***
+ template <class F>
+ 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
--- /dev/null
+/*******************************************************************************************[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 <stdint.h>
+#include "Vec.h"
+
+namespace MINISAT
+{
+
+//=================================================================================================
+// Default hash/equals functions
+//
+
+template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } };
+template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } };
+
+template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } };
+template<class K> 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 K, class D, class H = Hash<K>, class E = Equal<K> >
+class Map {
+ struct Pair { K key; D data; };
+
+ H hash;
+ E equals;
+
+ vec<Pair>* table;
+ int cap;
+ int size;
+
+ // Don't allow copying (error prone):
+ Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); }
+ Map (Map<K,D,H,E>& 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<Pair>* old = table;
+
+ int newsize = primes[0];
+ for (int i = 1; newsize <= cap && i < nprimes; i++)
+ newsize = primes[i];
+
+ table = new vec<Pair>[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<Pair>& 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<Pair>& 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
--- /dev/null
+/*****************************************************************************************[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 T>
+class Queue {
+ vec<T> 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 T>
+//class Queue {
+// vec<T> 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<T> 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
--- /dev/null
+/******************************************************************************************[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<class T>
+struct LessThan_default {
+ bool operator () (T x, T y) { return x < y; }
+};
+
+
+template <class T, class LessThan>
+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 <class T> static inline void selectionSort(T* array, int size) {
+ selectionSort(array, size, LessThan_default<T>()); }
+
+template <class T, class LessThan>
+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 <class T> static inline void sort(T* array, int size) {
+ sort(array, size, LessThan_default<T>()); }
+
+
+//=================================================================================================
+// For 'vec's:
+
+
+template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) {
+ sort(v.getData(), v.size(), lt); }
+template <class T> void sort(vec<T>& v) {
+ sort(v, LessThan_default<T>()); }
+
+};
+//=================================================================================================
+#endif
--- /dev/null
+/*******************************************************************************************[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 <cstdlib>
+#include <cassert>
+#include <new>
+
+namespace MINISAT
+{
+//=================================================================================================
+// Automatically resizable arrays
+//
+// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
+
+template<class T>
+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<T>& operator = (vec<T>& other) { assert(0); return *this; }
+ vec (vec<T>& 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<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); }
+ void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
+};
+
+template<class T>
+void vec<T>::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<class T>
+void vec<T>::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<class T>
+void vec<T>::growTo(int size) {
+ if (sz >= size) return;
+ grow(size);
+ for (int i = sz; i < size; i++) new (&data[i]) T();
+ sz = size; }
+
+template<class T>
+void vec<T>::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
#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"
x = info[varphi];
}
-#ifdef CRYPTOMINISAT
+#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
if(isXorChild)
{
setDoRenamePos(*x);
convertFormulaToCNFPosCases(varphi, defs);
}
-#ifdef CRYPTOMINISAT
+#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
if ((x->clausespos != NULL
&& x->clausespos->size() > 1)
|| (doRenamePos(*x) && !wasVisited(*x)))
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<const ASTNode*>();
ClauseList* defs)
{
//#ifdef FALSE
-#ifdef CRYPTOMINISAT
+#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
CNFInfo * xx = info[varphi];
if(NULL != xx
&& sharesPos(*xx) > 0
// {
// continue;
// }
-#ifdef CRYPTOMINISAT
+#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
if(add_xor_clauses)
{
//cout << "addXorClause:\n";
// << 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();
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();
projects / francis / stp.git / commitdiff