Adding code of MiniSAT 2.2.

.hgignore

@@ -19,7 +19,6 @@ src/xxx/
 src/aig/au/
 src/aig/ssm/
 src/aig/ddb/
-src/sat/bsat2/
 
 src/base/abc2/
 src/base/abc2d/

Makefile

@@ -109,14 +109,22 @@ DEP := $(OBJ:.o=.d)
 	@echo "$(MSG_PREFIX)\`\` Compiling:" $(LOCAL_PATH)/$<
 	@$(CXX) -c $(CXXFLAGS) $< -o $@
 
+%.o: %.cpp
+	@echo "$(MSG_PREFIX)\`\` Compiling:" $(LOCAL_PATH)/$<
+	@$(CXX) -c $(CXXFLAGS) $< -o $@
+
 %.d: %.c
-	@echo "$(MSG_PREFIX)\`\` Dependency:" $(LOCAL_PATH)/$<
+	@echo "$(MSG_PREFIX)\`\` Generating dependency:" $(LOCAL_PATH)/$<
 	@./depends.sh $(CC) `dirname $*.c` $(CFLAGS) $*.c > $@
 
 %.d: %.cc
 	@echo "$(MSG_PREFIX)\`\` Generating dependency:" $(LOCAL_PATH)/$<
 	@./depends.sh $(CXX) `dirname $*.cc` $(CXXFLAGS) $*.cc > $@
 
+%.d: %.cpp
+	@echo "$(MSG_PREFIX)\`\` Generating dependency:" $(LOCAL_PATH)/$<
+	@./depends.sh $(CXX) `dirname $*.cpp` $(CXXFLAGS) $*.cpp > $@
+
 -include $(DEP)
 
 # Actual targets

src/sat/bsat2/AbcApi.cpp

+/**CFile****************************************************************
+
+  FileName    [AbcApi.cpp]
+
+  PackageName [A C++ version of SAT solver MiniSAT 2.2 developed 
+  by Niklas Sorensson and Niklas Een. http://minisat.se.]
+
+  Synopsis    [Interface to the SAT solver.]
+
+  Author      [Niklas Sorensson and Niklas Een.]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: AbcApi.cpp,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "Solver.h"
+#include "sat/cnf/cnf.h"
+
+ABC_NAMESPACE_IMPL_START
+
+using namespace Minisat;
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CallMiniSat22( Cnf_Dat_t * p )
+{
+    Solver S;
+    int Result = -1;
+    return Result;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END

src/sat/bsat2/Alg.h

+/*******************************************************************************************[Alg.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Alg_h
+#define Minisat_Alg_h
+
+#include "Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Useful functions on vector-like types:
+
+//=================================================================================================
+// Removing and searching for elements:
+//
+
+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();
+}
+
+
+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();
+}
+
+
+//=================================================================================================
+// Copying vectors with support for nested vector types:
+//
+
+// Base case:
+template<class T>
+static inline void copy(const T& from, T& to)
+{
+    to = from;
+}
+
+// Recursive case:
+template<class T>
+static inline void copy(const vec<T>& from, vec<T>& to, bool append = false)
+{
+    if (!append)
+        to.clear();
+    for (int i = 0; i < from.size(); i++){
+        to.push();
+        copy(from[i], to.last());
+    }
+}
+
+template<class T>
+static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); }
+
+//=================================================================================================
+}
+
+#endif

src/sat/bsat2/Alloc.h

+/*****************************************************************************************[Alloc.h]
+Copyright (c) 2008-2010, 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 Minisat_Alloc_h
+#define Minisat_Alloc_h
+
+#include "XAlloc.h"
+#include "Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Simple Region-based memory allocator:
+
+template<class T>
+class RegionAllocator
+{
+    T*        memory;
+    uint32_t  sz;
+    uint32_t  cap;
+    uint32_t  wasted_;
+
+    void capacity(uint32_t min_cap);
+
+ public:
+    // TODO: make this a class for better type-checking?
+    typedef uint32_t Ref;
+    enum { Ref_Undef = UINT32_MAX };
+    enum { Unit_Size = sizeof(uint32_t) };
+
+    explicit RegionAllocator(uint32_t start_cap = 1024*1024) : memory(NULL), sz(0), cap(0), wasted_(0){ capacity(start_cap); }
+    ~RegionAllocator()
+    {
+        if (memory != NULL)
+            ::free(memory);
+    }
+
+
+    uint32_t size      () const      { return sz; }
+    uint32_t wasted    () const      { return wasted_; }
+
+    Ref      alloc     (int size); 
+    void     _free      (int size)    { wasted_ += size; }
+
+    // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
+    T&       operator[](Ref r)       { assert(r >= 0 && r < sz); return memory[r]; }
+    const T& operator[](Ref r) const { assert(r >= 0 && r < sz); return memory[r]; }
+
+    T*       lea       (Ref r)       { assert(r >= 0 && r < sz); return &memory[r]; }
+    const T* lea       (Ref r) const { assert(r >= 0 && r < sz); return &memory[r]; }
+    Ref      ael       (const T* t)  { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);
+        return  (Ref)(t - &memory[0]); }
+
+    void     moveTo(RegionAllocator& to) {
+        if (to.memory != NULL) ::free(to.memory);
+        to.memory = memory;
+        to.sz = sz;
+        to.cap = cap;
+        to.wasted_ = wasted_;
+
+        memory = NULL;
+        sz = cap = wasted_ = 0;
+    }
+
+
+};
+
+template<class T>
+void RegionAllocator<T>::capacity(uint32_t min_cap)
+{
+    if (cap >= min_cap) return;
+
+    uint32_t prev_cap = cap;
+    while (cap < min_cap){
+        // NOTE: Multiply by a factor (13/8) without causing overflow, then add 2 and make the
+        // result even by clearing the least significant bit. The resulting sequence of capacities
+        // is carefully chosen to hit a maximum capacity that is close to the '2^32-1' limit when
+        // using 'uint32_t' as indices so that as much as possible of this space can be used.
+        uint32_t delta = ((cap >> 1) + (cap >> 3) + 2) & ~1;
+        cap += delta;
+
+        if (cap <= prev_cap)
+            throw OutOfMemoryException();
+    }
+    // printf(" .. (%p) cap = %u\n", this, cap);
+
+    assert(cap > 0);
+    memory = (T*)xrealloc(memory, sizeof(T)*cap);
+}
+
+
+template<class T>
+typename RegionAllocator<T>::Ref
+RegionAllocator<T>::alloc(int size)
+{ 
+    // printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout);
+    assert(size > 0);
+    capacity(sz + size);
+
+    uint32_t prev_sz = sz;
+    sz += size;
+    
+    // Handle overflow:
+    if (sz < prev_sz)
+        throw OutOfMemoryException();
+
+    return prev_sz;
+}
+
+
+//=================================================================================================
+}
+
+#endif

src/sat/bsat2/Dimacs.h

+/****************************************************************************************[Dimacs.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Dimacs_h
+#define Minisat_Dimacs_h
+
+#include <stdio.h>
+
+#include "ParseUtils.h"
+#include "SolverTypes.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// DIMACS Parser:
+
+template<class B, class Solver>
+static void readClause(B& in, Solver& S, vec<Lit>& lits) {
+    int     parsed_lit, var;
+    lits.clear();
+    for (;;){
+        parsed_lit = parseInt(in);
+        if (parsed_lit == 0) break;
+        var = abs(parsed_lit)-1;
+        while (var >= S.nVars()) S.newVar();
+        lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
+    }
+}
+
+template<class B, class Solver>
+static void parse_DIMACS_main(B& in, Solver& S) {
+    vec<Lit> lits;
+    int vars    = 0;
+    int clauses = 0;
+    int cnt     = 0;
+    for (;;){
+        skipWhitespace(in);
+        if (*in == EOF) break;
+        else if (*in == 'p'){
+            if (eagerMatch(in, "p cnf")){
+                vars    = parseInt(in);
+                clauses = parseInt(in);
+                // SATRACE'06 hack
+                // if (clauses > 4000000)
+                //     S.eliminate(true);
+            }else{
+                printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
+            }
+        } else if (*in == 'c' || *in == 'p')
+            skipLine(in);
+        else{
+            cnt++;
+            readClause(in, S, lits);
+            S.addClause_(lits); }
+    }
+    if (vars != S.nVars())
+        fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of variables.\n");
+    if (cnt  != clauses)
+        fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of clauses.\n");
+}
+
+// Inserts problem into solver.
+//
+template<class Solver>
+static void parse_DIMACS(gzFile input_stream, Solver& S) {
+    StreamBuffer in(input_stream);
+    parse_DIMACS_main(in, S); }
+
+//=================================================================================================
+}
+
+#endif

src/sat/bsat2/Heap.h

+/******************************************************************************************[Heap.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Heap_h
+#define Minisat_Heap_h
+
+#include "Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// A heap implementation with support for decrease/increase key.
+
+
+template<class Comp>
+class Heap {
+    Comp     lt;       // The heap is a minimum-heap with respect to this comparator
+    vec<int> heap;     // Heap of integers
+    vec<int> indices;  // Each integers position (index) in the 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; }
+
+
+    void percolateUp(int i)
+    {
+        int x  = heap[i];
+        int p  = parent(i);
+        
+        while (i != 0 && lt(x, heap[p])){
+            heap[i]          = heap[p];
+            indices[heap[p]] = i;
+            i                = p;
+            p                = parent(p);
+        }
+        heap   [i] = x;
+        indices[x] = i;
+    }
+
+
+    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;
+    }
+
+
+  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]); }
+    void increase  (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
+
+
+    // Safe variant of insert/decrease/increase:
+    void update(int n)
+    {
+        if (!inHeap(n))
+            insert(n);
+        else {
+            percolateUp(indices[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; 
+    }
+
+
+    // Rebuild the heap from scratch, using the elements in 'ns':
+    void build(vec<int>& ns) {
+        int i;
+        for (i = 0; i < heap.size(); i++)
+            indices[heap[i]] = -1;
+        heap.clear();
+
+        for (i = 0; i < ns.size(); i++){
+            indices[ns[i]] = i;
+            heap.push(ns[i]); }
+
+        for (i = heap.size() / 2 - 1; i >= 0; i--)
+            percolateDown(i);
+    }
+
+    void clear(bool dealloc = false) 
+    { 
+        for (int i = 0; i < heap.size(); i++)
+            indices[heap[i]] = -1;
+        heap.clear(dealloc); 
+    }
+};
+
+
+//=================================================================================================
+}
+
+#endif

src/sat/bsat2/IntTypes.h

+/**************************************************************************************[IntTypes.h]
+Copyright (c) 2009-2010, 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 Minisat_IntTypes_h
+#define Minisat_IntTypes_h
+
+#ifdef __sun
+    // Not sure if there are newer versions that support C99 headers. The
+    // needed features are implemented in the headers below though:
+
+#   include <sys/int_types.h>
+#   include <sys/int_fmtio.h>
+#   include <sys/int_limits.h>
+
+#elif _WIN32
+
+#   include "pstdint.h"
+
+#else
+
+#   include <stdint.h>
+#   include <inttypes.h>
+
+#endif
+
+#include <limits.h>
+
+//=================================================================================================
+
+#endif

src/sat/bsat2/LICENSE

+MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+           Copyright (c) 2007-2010  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.

src/sat/bsat2/MainSat.cpp

+/*****************************************************************************************[Main.cc]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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.
+**************************************************************************************************/
+
+#include <errno.h>
+
+#include <signal.h>
+#include "misc/zlib/zlib.h"
+
+#include "System.h"
+#include "ParseUtils.h"
+#include "Options.h"
+#include "Dimacs.h"
+#include "Solver.h"
+
+using namespace Minisat;
+
+//=================================================================================================
+
+
+void printStats(Solver& solver)
+{
+    double cpu_time = cpuTime();
+    double mem_used = memUsedPeak();
+    printf("restarts              : %-12.0f\n",                                (double)(int64_t)solver.starts);
+    printf("conflicts             : %-12.0f  (%.0f /sec)\n",                   (double)(int64_t)solver.conflicts,    (double)(int64_t)solver.conflicts / cpu_time);
+    printf("decisions             : %-12.0f  (%4.2f %% random) (%.0f /sec)\n", (double)(int64_t)solver.decisions,    (double)(int64_t)solver.rnd_decisions*100 / (double)(int64_t)solver.decisions, (double)(int64_t)solver.decisions / cpu_time);
+    printf("propagations          : %-12.0f  (%.0f /sec)\n",                   (double)(int64_t)solver.propagations, (double)(int64_t)solver.propagations / cpu_time);
+    printf("conflict literals     : %-12.0f  (%4.2f %% deleted)\n",            (double)(int64_t)solver.tot_literals, (double)(int64_t)(solver.max_literals - solver.tot_literals)*100 / (double)(int64_t)solver.max_literals);
+    if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used);
+    printf("CPU time              : %g s\n", cpu_time);
+}
+
+
+static Solver* solver;
+// Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case
+// for this feature of the Solver as it may take longer than an immediate call to '_exit()'.
+static void SIGINT_interrupt(int signum) { solver->interrupt(); }
+
+// Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls
+// destructors and may cause deadlocks if a malloc/free function happens to be running (these
+// functions are guarded by locks for multithreaded use).
+static void SIGINT_exit(int signum) {
+    printf("\n"); printf("*** INTERRUPTED ***\n");
+    if (solver->verbosity > 0){
+        printStats(*solver);
+        printf("\n"); printf("*** INTERRUPTED ***\n"); }
+    _exit(1); }
+
+
+//=================================================================================================
+// Main:
+
+
+extern "C" int MainSat(int argc, char** argv)
+{
+    try {
+        setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
+        // printf("This is MiniSat 2.0 beta\n");
+        
+#if defined(__linux__)
+        fpu_control_t oldcw, newcw;
+        _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+        printf("WARNING: for repeatability, setting FPU to use double precision\n");
+#endif
+        // Extra options:
+        //
+        IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
+        IntOption    cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX));
+        IntOption    mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX));
+        
+        if ( !parseOptions(argc, argv, true) )
+            return 1;
+
+        Solver S;
+        double initial_time = cpuTime();
+
+        S.verbosity = verb;
+        
+        solver = &S;
+/*
+        // Use signal handlers that forcibly quit until the solver will be able to respond to
+        // interrupts:
+        signal(SIGINT, SIGINT_exit);
+        signal(SIGXCPU,SIGINT_exit);
+
+        // Set limit on CPU-time:
+        if (cpu_lim != INT32_MAX){
+            rlimit rl;
+            getrlimit(RLIMIT_CPU, &rl);
+            if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){
+                rl.rlim_cur = cpu_lim;
+                if (setrlimit(RLIMIT_CPU, &rl) == -1)
+                    printf("WARNING! Could not set resource limit: CPU-time.\n");
+            } }
+
+        // Set limit on virtual memory:
+        if (mem_lim != INT32_MAX){
+            rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
+            rlimit rl;
+            getrlimit(RLIMIT_AS, &rl);
+            if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
+                rl.rlim_cur = new_mem_lim;
+                if (setrlimit(RLIMIT_AS, &rl) == -1)
+                    printf("WARNING! Could not set resource limit: Virtual memory.\n");
+            } }
+*/        
+        if (argc == 1)
+        {
+            printf("Reading from standard input... Use '--help' for help.\n");
+            return 1;
+        }
+        
+        gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
+        if (in == NULL)
+            printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
+        
+        if (S.verbosity > 0){
+            printf("============================[ Problem Statistics ]=============================\n");
+            printf("|                                                                             |\n"); }
+        
+        parse_DIMACS(in, S);
+        gzclose(in);
+        FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
+        
+        if (S.verbosity > 0){
+            printf("|  Number of variables:  %12d                                         |\n", S.nVars());
+            printf("|  Number of clauses:    %12d                                         |\n", S.nClauses()); }
+        
+        double parsed_time = cpuTime();
+        if (S.verbosity > 0){
+            printf("|  Parse time:           %12.2f s                                       |\n", parsed_time - initial_time);
+            printf("|                                                                             |\n"); }
+ 
+        // Change to signal-handlers that will only notify the solver and allow it to terminate
+        // voluntarily:
+//        signal(SIGINT, SIGINT_interrupt);
+//        signal(SIGXCPU,SIGINT_interrupt);
+       
+        if (!S.simplify()){
+            if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
+            if (S.verbosity > 0){
+                printf("===============================================================================\n");
+                printf("Solved by unit propagation\n");
+                printStats(S);
+                printf("\n"); }
+            printf("UNSATISFIABLE\n");
+            exit(20);
+        }
+        
+        vec<Lit> dummy;
+        lbool ret = S.solveLimited(dummy);
+        if (S.verbosity > 0){
+            printStats(S);
+            printf("\n"); }
+        printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n");
+        if (res != NULL){
+            if (ret == l_True){
+                fprintf(res, "SAT\n");
+                for (int i = 0; i < S.nVars(); i++)
+                    if (S.model[i] != l_Undef)
+                        fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
+                fprintf(res, " 0\n");
+            }else if (ret == l_False)
+                fprintf(res, "UNSAT\n");
+            else
+                fprintf(res, "INDET\n");
+            fclose(res);
+        }
+        
+//#ifdef NDEBUG
+//        exit(ret == l_True ? 10 : ret == l_False ? 20 : 0);     // (faster than "return", which will invoke the destructor for 'Solver')
+//#else
+        return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
+//#endif
+    } catch (OutOfMemoryException&){
+        printf("===============================================================================\n");
+        printf("INDETERMINATE\n");
+        exit(0);
+    }
+}

src/sat/bsat2/MainSimp.cpp

+/*****************************************************************************************[Main.cc]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007,      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.
+**************************************************************************************************/
+
+#include <errno.h>
+
+#include <signal.h>
+#include "misc/zlib/zlib.h"
+
+#ifndef _WIN32
+#include <sys/resource.h>
+#endif
+
+#include "System.h"
+#include "ParseUtils.h"
+#include "Options.h"
+#include "Dimacs.h"
+#include "SimpSolver.h"
+
+using namespace Minisat;
+
+//=================================================================================================
+
+extern void printStats(Solver& solver);
+
+static Solver* solver;
+// Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case
+// for this feature of the Solver as it may take longer than an immediate call to '_exit()'.
+static void SIGINT_interrupt(int signum) { solver->interrupt(); }
+
+// Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls
+// destructors and may cause deadlocks if a malloc/free function happens to be running (these
+// functions are guarded by locks for multithreaded use).
+static void SIGINT_exit(int signum) {
+    printf("\n"); printf("*** INTERRUPTED ***\n");
+    if (solver->verbosity > 0){
+        printStats(*solver);
+        printf("\n"); printf("*** INTERRUPTED ***\n"); }
+    _exit(1); }
+
+
+//=================================================================================================
+// Main:
+
+extern "C" int MainSimp(int argc, char** argv)
+{
+    try {
+        setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
+        // printf("This is MiniSat 2.0 beta\n");
+        
+#if defined(__linux__)
+        fpu_control_t oldcw, newcw;
+        _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+        printf("WARNING: for repeatability, setting FPU to use double precision\n");
+#endif
+        // Extra options:
+        //
+        IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
+        BoolOption   pre    ("MAIN", "pre",    "Completely turn on/off any preprocessing.", true);
+        StringOption dimacs ("MAIN", "dimacs", "If given, stop after preprocessing and write the result to this file.");
+        IntOption    cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX));
+        IntOption    mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX));
+
+        if ( !parseOptions(argc, argv, true) )
+            return 1;
+        
+        SimpSolver  S;
+        double      initial_time = cpuTime();
+
+        if (!pre) S.eliminate(true);
+
+        S.verbosity = verb;
+        
+        solver = &S;
+/*
+        // Use signal handlers that forcibly quit until the solver will be able to respond to
+        // interrupts:
+        signal(SIGINT, SIGINT_exit);
+        signal(SIGXCPU,SIGINT_exit);
+
+        // Set limit on CPU-time:
+        if (cpu_lim != INT32_MAX){
+            rlimit rl;
+            getrlimit(RLIMIT_CPU, &rl);
+            if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){
+                rl.rlim_cur = cpu_lim;
+                if (setrlimit(RLIMIT_CPU, &rl) == -1)
+                    printf("WARNING! Could not set resource limit: CPU-time.\n");
+            } }
+
+        // Set limit on virtual memory:
+        if (mem_lim != INT32_MAX){
+            rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
+            rlimit rl;
+            getrlimit(RLIMIT_AS, &rl);
+            if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
+                rl.rlim_cur = new_mem_lim;
+                if (setrlimit(RLIMIT_AS, &rl) == -1)
+                    printf("WARNING! Could not set resource limit: Virtual memory.\n");
+            } }
+*/        
+        if (argc == 1)
+        {
+            printf("Reading from standard input... Use '--help' for help.\n");
+            return 1;
+        }
+
+        gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
+        if (in == NULL)
+            printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
+        
+        if (S.verbosity > 0){
+            printf("============================[ Problem Statistics ]=============================\n");
+            printf("|                                                                             |\n"); }
+        
+        parse_DIMACS(in, S);
+        gzclose(in);
+        FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
+
+        if (S.verbosity > 0){
+            printf("|  Number of variables:  %12d                                         |\n", S.nVars());
+            printf("|  Number of clauses:    %12d                                         |\n", S.nClauses()); }
+        
+        double parsed_time = cpuTime();
+        if (S.verbosity > 0)
+            printf("|  Parse time:           %12.2f s                                       |\n", parsed_time - initial_time);
+
+        // Change to signal-handlers that will only notify the solver and allow it to terminate
+        // voluntarily:
+//        signal(SIGINT, SIGINT_interrupt);
+//        signal(SIGXCPU,SIGINT_interrupt);
+
+        S.eliminate(true);
+        double simplified_time = cpuTime();
+        if (S.verbosity > 0){
+            printf("|  Simplification time:  %12.2f s                                       |\n", simplified_time - parsed_time);
+            printf("|                                                                             |\n"); }
+
+        if (!S.okay()){
+            if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
+            if (S.verbosity > 0){
+                printf("===============================================================================\n");
+                printf("Solved by simplification\n");
+                printStats(S);
+                printf("\n"); }
+            printf("UNSATISFIABLE\n");
+            exit(20);
+        }
+
+        if (dimacs){
+            if (S.verbosity > 0)
+                printf("==============================[ Writing DIMACS ]===============================\n");
+            S.toDimacs((const char*)dimacs);
+            if (S.verbosity > 0)
+                printStats(S);
+            exit(0);
+        }
+
+        vec<Lit> dummy;
+        lbool ret = S.solveLimited(dummy);
+        
+        if (S.verbosity > 0){
+            printStats(S);
+            printf("\n"); }
+        printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n");
+        if (res != NULL){
+            if (ret == l_True){
+                fprintf(res, "SAT\n");
+                for (int i = 0; i < S.nVars(); i++)
+                    if (S.model[i] != l_Undef)
+                        fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
+                fprintf(res, " 0\n");
+            }else if (ret == l_False)
+                fprintf(res, "UNSAT\n");
+            else
+                fprintf(res, "INDET\n");
+            fclose(res);
+        }
+
+//#ifdef NDEBUG
+//        exit(ret == l_True ? 10 : ret == l_False ? 20 : 0);     // (faster than "return", which will invoke the destructor for 'Solver')
+//#else
+        return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
+//#endif
+    } catch (OutOfMemoryException&){
+        printf("===============================================================================\n");
+        printf("INDETERMINATE\n");
+        exit(0);
+    }
+}

src/sat/bsat2/Map.h

+/*******************************************************************************************[Map.h]
+Copyright (c) 2006-2010, 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 Minisat_Map_h
+#define Minisat_Map_h
+
+#include "IntTypes.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; } };
+
+static inline uint32_t hash(uint32_t x){ return x; }
+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
+
+
+//=================================================================================================
+// 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 {
+ public:
+    struct Pair { K key; D data; };
+
+ private:
+    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); }
+
+    bool    checkCap(int new_size) const { return new_size > cap; }
+
+    int32_t index  (const K& k) const { return hash(k) % cap; }
+    void   _insert (const K& k, const D& d) { 
+        vec<Pair>& ps = table[index(k)];
+        ps.push(); ps.last().key = k; ps.last().data = d; }
+
+    void    rehash () {
+        const vec<Pair>* old = table;
+
+        int old_cap = cap;
+        int newsize = primes[0];
+        for (int i = 1; newsize <= cap && i < nprimes; i++)
+           newsize = primes[i];
+
+        table = new vec<Pair>[newsize];
+        cap   = newsize;
+
+        for (int i = 0; i < old_cap; i++){
+            for (int j = 0; j < old[i].size(); j++){
+                _insert(old[i][j].key, old[i][j].data); }}
+
+        delete [] old;
+
+        // printf(" --- rehashing, old-cap=%d, new-cap=%d\n", cap, newsize);
+    }
+
+    
+ public:
+
+    Map () : table(NULL), cap(0), size(0) {}
+    Map (const H& h, const E& e) : hash(h), equals(e), table(NULL), cap(0), size(0){}
+    ~Map () { delete [] table; }
+
+    // PRECONDITION: the key must already exist in the map.
+    const D& operator [] (const K& k) const
+    {
+        assert(size != 0);
+        const D*         res = NULL;
+        const vec<Pair>& ps  = table[index(k)];
+        for (int i = 0; i < ps.size(); i++)
+            if (equals(ps[i].key, k))
+                res = &ps[i].data;
+        assert(res != NULL);
+        return *res;
+    }
+
+    // PRECONDITION: the key must already exist in the map.
+    D& operator [] (const K& k)
+    {
+        assert(size != 0);
+        D*         res = NULL;
+        vec<Pair>& ps  = table[index(k)];
+        for (int i = 0; i < ps.size(); i++)
+            if (equals(ps[i].key, k))
+                res = &ps[i].data;
+        assert(res != NULL);
+        return *res;
+    }
+
+    // PRECONDITION: the key must *NOT* exist in the map.
+    void insert (const K& k, const D& d) { if (checkCap(size+1)) rehash(); _insert(k, d); size++; }
+    bool peek   (const K& k, D& d) const {
+        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;
+    }
+
+    bool has   (const K& k) const {
+        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))
+                return true;
+        return false;
+    }
+
+    // PRECONDITION: the key must exist in the map.
+    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();
+        size--;
+    }
+
+    void clear  () {
+        cap = size = 0;
+        delete [] table;
+        table = NULL;
+    }
+
+    int  elems() const { return size; }
+    int  bucket_count() const { return cap; }
+
+    // NOTE: the hash and equality objects are not moved by this method:
+    void moveTo(Map& other){
+        delete [] other.table;
+
+        other.table = table;
+        other.cap   = cap;
+        other.size  = size;
+
+        table = NULL;
+        size = cap = 0;
+    }
+
+    // NOTE: given a bit more time, I could make a more C++-style iterator out of this:
+    const vec<Pair>& bucket(int i) const { return table[i]; }
+};
+
+//=================================================================================================
+}
+
+#endif

src/sat/bsat2/Options.cpp

+/**************************************************************************************[Options.cc]
+Copyright (c) 2008-2010, 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.
+**************************************************************************************************/
+
+#include "Sort.h"
+#include "Options.h"
+#include "ParseUtils.h"
+
+using namespace Minisat;
+
+int Minisat::parseOptions(int& argc, char** argv, bool strict)
+{
+    int i, j;
+    for (i = j = 1; i < argc; i++){
+        const char* str = argv[i];
+        if (match(str, "--") && match(str, Option::getHelpPrefixString()) && match(str, "help")){
+            if (*str == '\0')
+                return printUsageAndExit(argc, argv);
+            else if (match(str, "-verb"))
+                return printUsageAndExit(argc, argv, true);
+        } else {
+            bool parsed_ok = false;
+        
+            for (int k = 0; !parsed_ok && k < Option::getOptionList().size(); k++){
+                parsed_ok = Option::getOptionList()[k]->parse(argv[i]);
+
+                // fprintf(stderr, "checking %d: %s against flag <%s> (%s)\n", i, argv[i], Option::getOptionList()[k]->name, parsed_ok ? "ok" : "skip");
+            }
+
+            if (!parsed_ok)
+                if (strict && match(argv[i], "-"))
+                    { fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()); return 0; } //  exit(0);
+                else
+                    argv[j++] = argv[i];
+        }
+    }
+
+    argc -= (i - j);
+    return 1;
+}
+
+
+void Minisat::setUsageHelp      (const char* str){ Option::getUsageString() = str; }
+void Minisat::setHelpPrefixStr  (const char* str){ Option::getHelpPrefixString() = str; }
+int Minisat::printUsageAndExit (int argc, char** argv, bool verbose)
+{
+    const char* usage = Option::getUsageString();
+    if (usage != NULL)
+        fprintf(stderr, usage, argv[0]);
+
+    sort(Option::getOptionList(), Option::OptionLt());
+
+    const char* prev_cat  = NULL;
+    const char* prev_type = NULL;
+
+    for (int i = 0; i < Option::getOptionList().size(); i++){
+        const char* cat  = Option::getOptionList()[i]->category;
+        const char* type = Option::getOptionList()[i]->type_name;
+
+        if (cat != prev_cat)
+            fprintf(stderr, "\n%s OPTIONS:\n\n", cat);
+        else if (type != prev_type)
+            fprintf(stderr, "\n");
+
+        Option::getOptionList()[i]->help(verbose);
+
+        prev_cat  = Option::getOptionList()[i]->category;
+        prev_type = Option::getOptionList()[i]->type_name;
+    }
+
+    fprintf(stderr, "\nHELP OPTIONS:\n\n");
+    fprintf(stderr, "  --%shelp        Print help message.\n", Option::getHelpPrefixString());
+    fprintf(stderr, "  --%shelp-verb   Print verbose help message.\n", Option::getHelpPrefixString());
+    fprintf(stderr, "\n");
+//    exit(0);
+    return 0;
+}
+

src/sat/bsat2/ParseUtils.h

+/************************************************************************************[ParseUtils.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_ParseUtils_h
+#define Minisat_ParseUtils_h
+
+#include <stdlib.h>
+#include <stdio.h>
+
+#include "misc/zlib/zlib.h"
+
+namespace Minisat {
+
+//-------------------------------------------------------------------------------------------------
+// A simple buffered character stream class:
+
+static const int buffer_size = 1048576;
+
+
+class StreamBuffer {
+    gzFile        in;
+    unsigned char buf[buffer_size];
+    int           pos;
+    int           size;
+
+    void assureLookahead() {
+        if (pos >= size) {
+            pos  = 0;
+            size = gzread(in, buf, sizeof(buf)); } }
+
+public:
+    explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
+
+    int  operator *  () const { return (pos >= size) ? EOF : buf[pos]; }
+    void operator ++ ()       { pos++; assureLookahead(); }
+    int  position    () const { return pos; }
+};
+
+
+//-------------------------------------------------------------------------------------------------
+// End-of-file detection functions for StreamBuffer and char*:
+
+
+static inline bool isEof(StreamBuffer& in) { return *in == EOF;  }
+static inline bool isEof(const char*   in) { return *in == '\0'; }
+
+//-------------------------------------------------------------------------------------------------
+// Generic parse functions parametrized over the input-stream type.
+
+
+template<class B>
+static void skipWhitespace(B& in) {
+    while ((*in >= 9 && *in <= 13) || *in == 32)
+        ++in; }
+
+
+template<class B>
+static void skipLine(B& in) {
+    for (;;){
+        if (isEof(in)) return;
+        if (*in == '\n') { ++in; return; }
+        ++in; } }
+
+
+template<class B>
+static int parseInt(B& in) {
+    int     val = 0;
+    bool    neg = false;
+    skipWhitespace(in);
+    if      (*in == '-') neg = true, ++in;
+    else if (*in == '+') ++in;
+    if (*in < '0' || *in > '9') fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
+    while (*in >= '0' && *in <= '9')
+        val = val*10 + (*in - '0'),
+        ++in;
+    return neg ? -val : val; }
+
+
+// String matching: in case of a match the input iterator will be advanced the corresponding
+// number of characters.
+template<class B>
+static bool match(B& in, const char* str) {
+    int i;
+    for (i = 0; str[i] != '\0'; i++)
+        if (in[i] != str[i])
+            return false;
+
+    in += i;
+
+    return true; 
+}
+
+// String matching: consumes characters eagerly, but does not require random access iterator.
+template<class B>
+static bool eagerMatch(B& in, const char* str) {
+    for (; *str != '\0'; ++str, ++in)
+        if (*str != *in)
+            return false;
+    return true; }
+
+
+//=================================================================================================
+}
+
+#endif

src/sat/bsat2/Queue.h

+/*****************************************************************************************[Queue.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Queue_h
+#define Minisat_Queue_h
+
+#include "Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+
+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 (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; }
+    int  size  () const { return (end >= first) ? end - first : end - first + buf.size(); }
+
+    const T& operator [] (int index) const  { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+    T&       operator [] (int index)        { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+
+    T    peek  () const { 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 j, i = 0;
+            for (j = first; j < buf.size(); j++) tmp[i++] = buf[j];
+            for (j = 0    ; j < end       ; j++) tmp[i++] = buf[j];
+            first = 0;
+            end   = buf.size();
+            tmp.moveTo(buf);
+        }
+    }
+};
+
+
+//=================================================================================================
+}
+
+#endif

src/sat/bsat2/README

+================================================================================
+DIRECTORY OVERVIEW:
+
+mtl/            Mini Template Library
+utils/          Generic helper code (I/O, Parsing, CPU-time, etc)
+core/           A core version of the solver
+simp/           An extended solver with simplification capabilities
+README
+LICENSE
+
+================================================================================
+BUILDING: (release version: without assertions, statically linked, etc)
+
+export MROOT=<minisat-dir>              (or setenv in cshell)
+cd { core | simp }
+gmake rs
+cp minisat_static <install-dir>/minisat
+
+================================================================================
+EXAMPLES:
+
+Run minisat with same heuristics as version 2.0:
+
+> minisat <cnf-file> -no-luby -rinc=1.5 -phase-saving=0 -rnd-freq=0.02

src/sat/bsat2/ReleaseNotes-2.2.0.txt

+Release Notes for MiniSat 2.2.0
+===============================
+
+Changes since version 2.0:
+
+ * Started using a more standard release numbering.
+
+ * Includes some now well-known heuristics: phase-saving and luby
+   restarts. The old heuristics are still present and can be activated
+   if needed.
+
+ * Detection/Handling of out-of-memory and vector capacity
+   overflow. This is fairly new and relatively untested.
+
+ * Simple resource controls: CPU-time, memory, number of
+   conflicts/decisions.
+
+ * CPU-time limiting is implemented by a more general, but simple,
+   asynchronous interruption feature. This means that the solving
+   procedure can be interrupted from another thread or in a signal
+   handler.
+
+ * Improved portability with respect to building on Solaris and with
+   Visual Studio. This is not regularly tested and chances are that
+   this have been broken since, but should be fairly easy to fix if
+   so.
+
+ * Changed C++ file-extention to the less problematic ".cc".
+
+ * Source code is now namespace-protected
+
+ * Introducing a new Clause Memory Allocator that brings reduced
+   memory consumption on 64-bit architechtures and improved
+   performance (to some extent). The allocator uses a region-based
+   approach were all references to clauses are represented as a 32-bit
+   index into a global memory region that contains all clauses. To
+   free up and compact memory it uses a simple copying garbage
+   collector.
+
+ * Improved unit-propagation by Blocking Literals. For each entry in
+   the watcher lists, pair the pointer to a clause with some
+   (arbitrary) literal from the clause. The idea is that if the
+   literal is currently true (i.e. the clause is satisfied) the
+   watchers of the clause does not need to be altered. This can thus
+   be detected without touching the clause's memory at all. As often
+   as can be done cheaply, the blocking literal for entries to the
+   watcher list of a literal 'p' is set to the other literal watched
+   in the corresponding clause.
+
+ * Basic command-line/option handling system. Makes it easy to specify
+   options in the class that they affect, and whenever that class is
+   used in an executable, parsing of options and help messages are
+   brought in automatically.
+
+ * General clean-up and various minor bug-fixes.
+
+ * Changed implementation of variable-elimination/model-extension:
+    
+     - The interface is changed so that arbitrary remembering is no longer
+       possible. If you need to mention some variable again in the future,
+       this variable has to be frozen.
+    
+     - When eliminating a variable, only clauses that contain the variable
+       with one sign is necessary to store. Thereby making the other sign
+       a "default" value when extending models.
+    
+     - The memory consumption for eliminated clauses is further improved
+       by storing all eliminated clauses in a single contiguous vector.
+
+  * Some common utility code (I/O, Parsing, CPU-time, etc) is ripped
+    out and placed in a separate "utils" directory.
+
+  * The DIMACS parse is refactored so that it can be reused in other
+    applications (not very elegant, but at least possible).
+
+  * Some simple improvements to scalability of preprocessing, using
+    more lazy clause removal from data-structures and a couple of
+    ad-hoc limits (the longest clause that can be produced in variable
+    elimination, and the longest clause used in backward subsumption).

src/sat/bsat2/SimpSolver.h

+/************************************************************************************[SimpSolver.h]
+Copyright (c) 2006,      Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_SimpSolver_h
+#define Minisat_SimpSolver_h
+
+#include "Queue.h"
+#include "Solver.h"
+
+
+namespace Minisat {
+
+//=================================================================================================
+
+
+class SimpSolver : public Solver {
+ public:
+    // Constructor/Destructor:
+    //
+    SimpSolver();
+    ~SimpSolver();
+
+    // Problem specification:
+    //
+    Var     newVar    (bool polarity = true, bool dvar = true);
+    bool    addClause (const vec<Lit>& ps);
+    bool    addEmptyClause();                // Add the empty clause to the solver.
+    bool    addClause (Lit p);               // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q);        // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
+    bool    addClause_(      vec<Lit>& ps);
+    bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
+
+    // Variable mode:
+    // 
+    void    setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
+    bool    isEliminated(Var v) const;
+
+    // Solving:
+    //
+    bool    solve       (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+    lbool   solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+    bool    solve       (                     bool do_simp = true, bool turn_off_simp = false);
+    bool    solve       (Lit p       ,        bool do_simp = true, bool turn_off_simp = false);       
+    bool    solve       (Lit p, Lit q,        bool do_simp = true, bool turn_off_simp = false);
+    bool    solve       (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
+    bool    eliminate   (bool turn_off_elim = false);  // Perform variable elimination based simplification. 
+
+    // Memory managment:
+    //
+    virtual void garbageCollect();
+
+
+    // Generate a (possibly simplified) DIMACS file:
+    //
+#if 0
+    void    toDimacs  (const char* file, const vec<Lit>& assumps);
+    void    toDimacs  (const char* file);
+    void    toDimacs  (const char* file, Lit p);
+    void    toDimacs  (const char* file, Lit p, Lit q);
+    void    toDimacs  (const char* file, Lit p, Lit q, Lit r);
+#endif
+
+    // Mode of operation:
+    //
+    int     grow;              // Allow a variable elimination step to grow by a number of clauses (default to zero).
+    int     clause_lim;        // Variables are not eliminated if it produces a resolvent with a length above this limit.
+                               // -1 means no limit.
+    int     subsumption_lim;   // Do not check if subsumption against a clause larger than this. -1 means no limit.
+    double  simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
+
+    bool    use_asymm;         // Shrink clauses by asymmetric branching.
+    bool    use_rcheck;        // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
+    bool    use_elim;          // Perform variable elimination.
+
+    // Statistics:
+    //
+    int     merges;
+    int     asymm_lits;
+    int     eliminated_vars;
+
+ protected:
+
+    // Helper structures:
+    //
+    struct ElimLt {
+        const vec<int>& n_occ;
+        explicit ElimLt(const vec<int>& no) : n_occ(no) {}
+
+        // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
+        // 32-bit implementation instead then, but this will have to do for now.
+        uint64_t cost  (Var x)        const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
+        bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
+        
+        // TODO: investigate this order alternative more.
+        // bool operator()(Var x, Var y) const { 
+        //     int c_x = cost(x);
+        //     int c_y = cost(y);
+        //     return c_x < c_y || c_x == c_y && x < y; }
+    };
+
+    struct ClauseDeleted {
+        const ClauseAllocator& ca;
+        explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
+        bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
+
+    // Solver state:
+    //
+    int                 elimorder;
+    bool                use_simplification;
+    vec<uint32_t>       elimclauses;
+    vec<char>           touched;
+    OccLists<Var, vec<CRef>, ClauseDeleted>
+                        occurs;
+    vec<int>            n_occ;
+    Heap<ElimLt>        elim_heap;
+    Queue<CRef>         subsumption_queue;
+    vec<char>           frozen;
+    vec<char>           eliminated;
+    int                 bwdsub_assigns;
+    int                 n_touched;
+
+    // Temporaries:
+    //
+    CRef                bwdsub_tmpunit;
+
+    // Main internal methods:
+    //
+    lbool         solve_                   (bool do_simp = true, bool turn_off_simp = false);
+    bool          asymm                    (Var v, CRef cr);
+    bool          asymmVar                 (Var v);
+    void          updateElimHeap           (Var v);
+    void          gatherTouchedClauses     ();
+    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
+    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, int& size);
+    bool          backwardSubsumptionCheck (bool verbose = false);
+    bool          eliminateVar             (Var v);
+    void          extendModel              ();
+
+    void          removeClause             (CRef cr);
+    bool          strengthenClause         (CRef cr, Lit l);
+    void          cleanUpClauses           ();
+    bool          implied                  (const vec<Lit>& c);
+    void          relocAll                 (ClauseAllocator& to);
+};
+
+
+//=================================================================================================
+// Implementation of inline methods:
+
+
+inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
+inline void SimpSolver::updateElimHeap(Var v) {
+    assert(use_simplification);
+    // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
+    if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
+        elim_heap.update(v); }
+
+
+inline bool SimpSolver::addClause    (const vec<Lit>& ps)    { ps.copyTo(add_tmp); return addClause_(add_tmp); }
+inline bool SimpSolver::addEmptyClause()                     { add_tmp.clear(); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause    (Lit p)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause    (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
+inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
+
+inline bool SimpSolver::solve        (                     bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (Lit p       ,        bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (Lit p, Lit q,        bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ 
+    budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; }
+
+inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ 
+    assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
+
+//=================================================================================================
+}
+
+#endif

src/sat/bsat2/Sort.h

+/******************************************************************************************[Sort.h]
+Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Sort_h
+#define Minisat_Sort_h
+
+#include "Vec.h"
+
+//=================================================================================================
+// Some sorting algorithms for vec's
+
+
+namespace Minisat {
+
+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((T*)v, v.size(), lt); }
+template <class T> void sort(vec<T>& v) {
+    sort(v, LessThan_default<T>()); }
+
+
+//=================================================================================================
+}
+
+#endif

src/sat/bsat2/System.cpp

+/***************************************************************************************[System.cc]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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.
+**************************************************************************************************/
+
+#include "System.h"
+
+#if defined(__linux__)
+
+#include <stdio.h>
+#include <stdlib.h>
+
+using namespace Minisat;
+
+// TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
+// one for reading the current virtual memory size.
+
+static inline int memReadStat(int field)
+{
+    char  name[256];
+    pid_t pid = getpid();
+    int   value;
+
+    sprintf(name, "/proc/%d/statm", pid);
+    FILE* in = fopen(name, "rb");
+    if (in == NULL) return 0;
+
+    for (; field >= 0; field--)
+        if (fscanf(in, "%d", &value) != 1)
+            printf("ERROR! Failed to parse memory statistics from \"/proc\".\n"), exit(1);
+    fclose(in);
+    return value;
+}
+
+
+static inline int memReadPeak(void)
+{
+    char  name[256];
+    pid_t pid = getpid();
+
+    sprintf(name, "/proc/%d/status", pid);
+    FILE* in = fopen(name, "rb");
+    if (in == NULL) return 0;
+
+    // Find the correct line, beginning with "VmPeak:":
+    int peak_kb = 0;
+    while (!feof(in) && fscanf(in, "VmPeak: %d kB", &peak_kb) != 1)
+        while (!feof(in) && fgetc(in) != '\n')
+            ;
+    fclose(in);
+
+    return peak_kb;
+}
+
+double Minisat::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }
+double Minisat::memUsedPeak() { 
+    double peak = memReadPeak() / 1024;
+    return peak == 0 ? memUsed() : peak; }
+
+#elif defined(__FreeBSD__)
+
+double Minisat::memUsed(void) {
+    struct rusage ru;
+    getrusage(RUSAGE_SELF, &ru);
+    return (double)ru.ru_maxrss / 1024; }
+double MiniSat::memUsedPeak(void) { return memUsed(); }
+
+
+#elif defined(__APPLE__)
+#include <malloc/malloc.h>
+
+double Minisat::memUsed(void) {
+    malloc_statistics_t t;
+    malloc_zone_statistics(NULL, &t);
+    return (double)t.max_size_in_use / (1024*1024); }
+
+#else
+double Minisat::memUsed()     { return 0; }
+double Minisat::memUsedPeak() { return 0; }
+#endif

src/sat/bsat2/System.h

+/****************************************************************************************[System.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_System_h
+#define Minisat_System_h
+
+#if defined(__linux__)
+#include <fpu_control.h>
+#endif
+
+#include "IntTypes.h"
+
+//-------------------------------------------------------------------------------------------------
+
+namespace Minisat {
+
+static inline double cpuTime(void); // CPU-time in seconds.
+extern double memUsed();            // Memory in mega bytes (returns 0 for unsupported architectures).
+extern double memUsedPeak();        // Peak-memory in mega bytes (returns 0 for unsupported architectures).
+
+}
+
+//-------------------------------------------------------------------------------------------------
+// Implementation of inline functions:
+
+#if defined(_MSC_VER) || defined(__MINGW32__)
+#include <time.h>
+
+static inline double Minisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
+
+#else
+#include <sys/time.h>
+#include <sys/resource.h>
+#include <unistd.h>
+
+static inline double Minisat::cpuTime(void) {
+    struct rusage ru;
+    getrusage(RUSAGE_SELF, &ru);
+    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
+
+#endif
+
+#endif

src/sat/bsat2/Vec.h

+/*******************************************************************************************[Vec.h]
+Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Vec_h
+#define Minisat_Vec_h
+
+#include <assert.h>
+#include <new>
+
+#include "IntTypes.h"
+#include "XAlloc.h"
+
+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;
+
+    // Don't allow copying (error prone):
+    vec<T>&  operator = (vec<T>& other) { assert(0); return *this; }
+             vec        (vec<T>& other) { assert(0); }
+             
+    // Helpers for calculating next capacity:
+    static inline int  imax   (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); }
+    //static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
+    static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
+
+public:
+    // Constructors:
+    vec()                       : data(NULL) , sz(0)   , cap(0)    { }
+    explicit 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()                                                          { clear(true); }
+
+    // Pointer to first element:
+    operator T*       (void)           { 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; }
+    int      capacity (void) const     { return cap; }
+    void     capacity (int min_cap);
+    void     growTo   (int size);
+    void     growTo   (int size, const T& pad);
+    void     clear    (bool dealloc = false);
+
+    // Stack interface:
+    void     push  (void)              { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
+    void     push  (const T& elem)     { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
+    void     push_ (const T& elem)     { assert(sz < cap); data[sz++] = elem; }
+    void     pop   (void)              { assert(sz > 0); sz--, data[sz].~T(); }
+    // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
+    // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
+    // happen given the way capacities are calculated (below). Essentially, all capacities are
+    // even, but INT_MAX is odd.
+
+    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++) copy[i] = 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>::capacity(int min_cap) {
+    if (cap >= min_cap) return;
+    int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1);   // NOTE: grow by approximately 3/2
+    if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
+        throw OutOfMemoryException();
+ }
+
+
+template<class T>
+void vec<T>::growTo(int size, const T& pad) {
+    if (sz >= size) return;
+    capacity(size);
+    for (int i = sz; i < size; i++) data[i] = pad;
+    sz = size; }
+
+
+template<class T>
+void vec<T>::growTo(int size) {
+    if (sz >= size) return;
+    capacity(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

src/sat/bsat2/XAlloc.h

+/****************************************************************************************[XAlloc.h]
+Copyright (c) 2009-2010, 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 Minisat_XAlloc_h
+#define Minisat_XAlloc_h
+
+#include <errno.h>
+#include <stdlib.h>
+
+namespace Minisat {
+
+//=================================================================================================
+// Simple layer on top of malloc/realloc to catch out-of-memory situtaions and provide some typing:
+
+class OutOfMemoryException{};
+static inline void* xrealloc(void *ptr, size_t size)
+{
+    void* mem = realloc(ptr, size);
+    if (mem == NULL && errno == ENOMEM){
+        throw OutOfMemoryException();
+    }else
+        return mem;
+}
+
+//=================================================================================================
+}
+
+#endif

src/sat/bsat2/module.make

+SRC +=  src/sat/bsat2/AbcApi.cpp \
+    src/sat/bsat2/MainSat.cpp \
+    src/sat/bsat2/MainSimp.cpp \
+    src/sat/bsat2/Options.cpp \
+    src/sat/bsat2/SimpSolver.cpp \
+    src/sat/bsat2/Solver.cpp \
+    src/sat/bsat2/System.cpp