Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

10 files changed, 2560 insertions, 0 deletions

diff --git a/stp/sat/Global.h b/stp/sat/Global.h
new file mode 100644
index 00000000..a428975c
--- /dev/null
+++ b/stp/sat/Global.h
@@ -0,0 +1,255 @@
+/****************************************************************************************[Global.h]
+MiniSat -- Copyright (c) 2003-2005, 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 Global_h
+#define Global_h
+
+#include <cassert>
+#include <cstdio>
+#include <cstdlib>
+#include <cstring>
+#include <new>
+
+// PKT: needs to be outside namespace MINISAT or mac os x compilation breaks
+#ifdef _MSC_VER
+#else
+#include <unistd.h>
+#endif
+
+namespace MINISAT {
+//=================================================================================================
+// Basic Types & Minor Things:
+
+// DWD: This is needed on darwin.
+typedef unsigned int uint;
+
+#ifdef _MSC_VER
+
+typedef INT64              int64;
+typedef UINT64             uint64;
+typedef INT_PTR            intp;
+typedef UINT_PTR           uintp;
+#define I64_fmt "I64d"
+#else
+
+typedef long long          int64;
+typedef unsigned long long uint64;
+typedef __PTRDIFF_TYPE__   intp;
+typedef unsigned __PTRDIFF_TYPE__ uintp;
+#define I64_fmt "lld"
+#endif
+
+template<class T> static inline T min(T x, T y) { return (x < y) ? x : y; }
+template<class T> static inline T max(T x, T y) { return (x > y) ? x : y; }
+
+template <bool> struct STATIC_ASSERTION_FAILURE;
+template <> struct STATIC_ASSERTION_FAILURE<true>{};
+#define TEMPLATE_FAIL STATIC_ASSERTION_FAILURE<false>()
+
+
+//=================================================================================================
+// 'malloc()'-style memory allocation -- never returns NULL; aborts instead:
+
+
+template<class T> static inline T* xmalloc(size_t size) {
+    T*   tmp = (T*)malloc(size * sizeof(T));
+    assert(size == 0 || tmp != NULL);
+    return tmp; }
+
+template<class T> static inline T* xrealloc(T* ptr, size_t size) {
+    T*   tmp = (T*)realloc((void*)ptr, size * sizeof(T));
+    assert(size == 0 || tmp != NULL);
+    return tmp; }
+
+template<class T> static inline void xfree(T *ptr) {
+    if (ptr != NULL) free((void*)ptr); }
+
+
+//=================================================================================================
+// Random numbers:
+
+
+// Returns a random float 0 <= x < 1. Seed must never be 0.
+static inline double drand(double& seed) {
+    seed *= 1389796;
+    int q = (int)(seed / 2147483647);
+    seed -= (double)q * 2147483647;
+    return seed / 2147483647; }
+
+// Returns a random integer 0 <= x < size. Seed must never be 0.
+static inline int irand(double& seed, int size) {
+    return (int)(drand(seed) * size); }
+
+
+//=================================================================================================
+// 'vec' -- automatically resizable arrays (via 'push()' method):
+
+
+// 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);
+
+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 'xfree()')
+   ~vec(void)                                                      { clear(true); }
+
+    // Ownership of underlying array:
+    T*       release  (void)           { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; }
+    operator T*       (void)           { return data; }     // (unsafe but convenient)
+    operator const T* (void) const     { 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     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:
+    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++; }
+    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]; }
+
+    // Don't allow copying (error prone):
+    vec<T>&  operator = (vec<T>& other) { TEMPLATE_FAIL; }
+             vec        (vec<T>& other) { TEMPLATE_FAIL; }
+
+    // Duplicatation (preferred instead):
+    void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (&copy[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 = xrealloc(data, cap); }
+
+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) xfree(data), data = NULL, cap = 0; } }
+
+
+//=================================================================================================
+// Useful functions on vectors
+
+
+template<class V, class T>
+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>
+bool find(V& ts, const T& t)
+{
+    int j = 0;
+    for (; j < ts.size() && ts[j] != t; j++);
+    return j < ts.size();
+}
+
+//=================================================================================================
+// Lifted booleans:
+
+
+class lbool {
+    int     value;
+    explicit lbool(int v) : value(v) { }
+
+public:
+    lbool()       : value(0) { }
+    lbool(bool x) : value((int)x*2-1) { }
+    int toInt(void) const { return value; }
+
+    bool  operator == (const lbool& other) const { return value == other.value; }
+    bool  operator != (const lbool& other) const { return value != other.value; }
+    lbool operator ~  (void)               const { return lbool(-value); }
+
+    friend int   toInt  (lbool l);
+    friend lbool toLbool(int   v);
+};
+inline int   toInt  (lbool l) { return l.toInt(); }
+inline lbool toLbool(int   v) { return lbool(v);  }
+
+const lbool l_True  = toLbool( 1);
+const lbool l_False = toLbool(-1);
+const lbool l_Undef = toLbool( 0);
+
+
+//=================================================================================================
+// Relation operators -- extend definitions from '==' and '<'
+
+
+#ifndef __SGI_STL_INTERNAL_RELOPS   // (be aware of SGI's STL implementation...)
+#define __SGI_STL_INTERNAL_RELOPS
+template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
+template <class T> static inline bool operator >  (const T& x, const T& y) { return y < x;     }
+template <class T> static inline bool operator <= (const T& x, const T& y) { return !(y < x);  }
+template <class T> static inline bool operator >= (const T& x, const T& y) { return !(x < y);  }
+#endif
+
+
+//=================================================================================================
+};
+#endif
diff --git a/stp/sat/Heap.h b/stp/sat/Heap.h
new file mode 100644
index 00000000..acfa1c1e
--- /dev/null
+++ b/stp/sat/Heap.h
@@ -0,0 +1,151 @@
+/******************************************************************************************[Heap.h]
+MiniSat -- Copyright (c) 2003-2005, 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 "../AST/ASTUtil.h"
+namespace MINISAT {
+
+//=================================================================================================
+
+
+static inline int left  (int i) { return i+i; }
+static inline int right (int i) { return i+i + 1; }
+static inline int parent(int i) { return i >> 1; }
+
+template<class C>
+class Heap {
+  public:
+    C        comp;
+    vec<int> heap;     // heap of ints
+    vec<int> indices;  // int -> index in heap
+
+    inline void percolateUp(int i)
+    {
+        int x = heap[i];
+        while (parent(i) != 0 && comp(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() && comp(heap[right(i)],heap[left(i)]) ? right(i) : left(i);
+            if (!comp(heap[child],x)) break;
+            heap[i]          = heap[child];
+            indices[heap[i]] = i;
+            i                = child;
+        }
+        heap   [i] = x;
+        indices[x] = i;
+    }
+
+    bool ok(int n) const { 
+        return n >= 0 && n < (int)indices.size(); }
+
+  public:
+    Heap(C c) : comp(c) { heap.push(-1); }
+
+    void setBounds (int size)    { assert(size >= 0); indices.growTo(size,0); }
+    void increase  (int n)       { assert(ok(n)); assert(inHeap(n)); percolateUp(indices[n]); }
+    bool inHeap    (int n) const { assert(ok(n)); return indices[n] != 0; }
+    int  size      ()      const { return heap.size()-1; }
+    bool empty     ()      const { return size() == 0; }
+
+
+    void insert(int n) {
+        assert(!inHeap(n));
+        assert(ok(n));
+        indices[n] = heap.size();
+        heap.push(n);
+        percolateUp(indices[n]); 
+    }
+
+
+  int  getmin() {
+    //printing heap
+    if(BEEV::print_sat_varorder) {
+      // fprintf(stderr, "Vijay: heap before getmin: ");
+      //       for (uint i = 1; i < (uint)heap.size(); i++)
+      // 	fprintf(stderr, "%d ", heap[i]);
+      //       fprintf(stderr, "\n");
+    }
+    
+    int r            = heap[1];
+    heap[1]          = heap.last();
+    indices[heap[1]] = 1;
+    indices[r]       = 0;
+    heap.pop();
+    if (heap.size() > 1)
+      percolateDown(1);
+    return r; 
+  }
+
+    // fool proof variant of insert/increase
+    void update    (int n)    {
+        //fprintf(stderr, "update heap: ");
+        //for (uint i = 1; i < (uint)heap.size(); i++)
+        //    fprintf(stderr, "%d ", heap[i]);
+        //fprintf(stderr, "\n");
+        setBounds(n+1);
+        if (!inHeap(n))
+            insert(n);
+        else {
+            percolateUp(indices[n]);
+            percolateDown(indices[n]);
+        }
+    }
+
+
+    bool heapProperty() {
+        return heapProperty(1); }
+
+
+    bool heapProperty(int i) {
+        return i >= heap.size()
+            || ((parent(i) == 0 || !comp(heap[i],heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); }
+
+    template <class F> void filter(const F& filt) {
+        int i,j;
+        for (i = j = 1; i < heap.size(); i++)
+            if (filt(heap[i])){
+                heap[j]          = heap[i];
+                indices[heap[i]] = j++;
+            }else
+                indices[heap[i]] = 0;
+
+        heap.shrink(i - j);
+        for (int i = heap.size() / 2; i >= 1; i--)
+            percolateDown(i);
+
+        assert(heapProperty());
+    }
+
+};
+
+//=================================================================================================
+};
+#endif
diff --git a/stp/sat/LICENSE b/stp/sat/LICENSE
new file mode 100644
index 00000000..590930bc
--- /dev/null
+++ b/stp/sat/LICENSE
@@ -0,0 +1,20 @@
+MiniSat -- Copyright (c) 2003-2005, 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.
diff --git a/stp/sat/Makefile b/stp/sat/Makefile
new file mode 100644
index 00000000..8298e05a
--- /dev/null
+++ b/stp/sat/Makefile
@@ -0,0 +1,16 @@
+include ../Makefile.common
+
+SRCS = Solver.C Simplifier.C
+OBJS = $(SRCS:.C=.o)
+
+libsatsolver.a: $(OBJS)
+	$(AR) rc $@ $^
+	$(RANLIB) $@
+
+Solver.o: Solver.C Solver.h Sort.h SolverTypes.h VarOrder.h Global.h Heap.h
+Simplifier.o: Simplifier.C Solver.h Sort.h SolverTypes.h VarOrder.h Global.h Heap.h
+
+clean:
+	rm -rf *.o *~  *.a  depend.mak .#*
+depend:
+	makedepend -- $(CFLAGS) -- $(SRCS)
diff --git a/stp/sat/Simplifier.C b/stp/sat/Simplifier.C
new file mode 100644
index 00000000..1c192e20
--- /dev/null
+++ b/stp/sat/Simplifier.C
@@ -0,0 +1,542 @@
+/************************************************************************************[Simplifier.C]
+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.
+**************************************************************************************************/
+
+#include "Solver.h"
+
+namespace MINISAT {
+
+static const int grow = 0;
+
+//#define WEAKEN
+//#define MATING
+//#define ASSYMM
+
+bool Solver::assymmetricBranching(Clause& c)
+{
+    assert(decisionLevel() == 0);
+
+    //fprintf(stderr, "assymmetric branching on clause: "); printClause(c); fprintf(stderr, "\n");
+    if (satisfied(c)){
+        //fprintf(stderr, "subsumed.\n");
+        return true; }
+
+    int      old;
+    vec<Lit> copy; for (int i = 0; i < c.size(); i++) copy.push(c[i]);
+
+    do {
+        assert(copy.size() == c.size());
+
+        old = copy.size();
+
+        //fprintf(stderr, "checking that clause is normalized\n");
+        //for (int i = 0; i < copy.size(); i++)
+        //    assert(value(copy[i]) == l_Undef);
+
+        for (int i = 0; i < copy.size(); i++){
+            trail_lim.push(trail.size());
+            //fprintf(stderr, " -- trying to delete literal "); printLit(copy[i]); 
+            for (int j = 0; j < copy.size(); j++)
+                if (j != i)
+                    check(enqueue(~copy[j]));
+
+            if (propagate() != NULL){
+                //fprintf(stderr, " succeeded\n");
+                cancelUntil(0);
+                Lit l = copy[i];
+                assert(find(copy, l));
+                remove(copy, l);
+                if (!strengthen(c, l))
+                    return false;
+                i--;
+
+                if (c.size() == 1)
+                    return propagate() == NULL;
+                else
+                    assert(qhead == trail.size());
+            }
+            else
+                //fprintf(stderr, " failed\n");
+
+            cancelUntil(0);
+        }
+
+        //} while (false);
+    } while (copy.size() < old);
+
+    return true;
+}
+
+// Returns FALSE if clause is always satisfied ('out_clause' should not be used). 
+//bool Solver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
+bool Solver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
+{  
+    stats.merges++;
+
+    bool  ps_smallest = _ps.size() < _qs.size();
+    const Clause& ps =  ps_smallest ? _qs : _ps;
+    const Clause& qs =  ps_smallest ? _ps : _qs;
+
+    for (int i = 0; i < qs.size(); i++){
+        if (var(qs[i]) != v){
+            for (int j = 0; j < ps.size(); j++)
+                if (var(ps[j]) == var(qs[i])) {
+                    if (ps[j] == ~qs[i])
+                        return false;
+                    else
+                        goto next;
+                }
+            out_clause.push(qs[i]);
+        }
+        next:;
+    }
+
+    for (int i = 0; i < ps.size(); i++)
+        if (var(ps[i]) != v)
+            out_clause.push(ps[i]);
+
+    return true;
+}
+
+
+void Solver::gather(vec<Clause*>& clauses)
+{
+    //fprintf(stderr, "Gathering clauses for backwards subsumption\n");
+    int ntouched = 0;
+    assert(touched.size() == occurs.size());
+    clauses.clear();
+    for (int i = 0; i < touched.size(); i++)
+        if (touched[i]){
+            const vec<Clause*>& cs = getOccurs(i);
+            ntouched++;
+            for (int j = 0; j < cs.size(); j++)
+                if (cs[j]->mark() == 0){
+                    clauses.push(cs[j]);
+                    cs[j]->mark(2);
+                }
+            touched[i] = 0;
+        }
+
+    //fprintf(stderr, "Touched variables %d of %d yields %d clauses to check\n", ntouched, touched.size(), clauses.size());
+    for (int i = 0; i < clauses.size(); i++)
+        clauses[i]->mark(0);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  subsumes : (_c : ClauseId) (c : Clause&) (_d : ClauseId) (d : Clause&)  ->  bool
+|
+|  Description:
+|     Checks if c subsumes d, and at the same time, if c can be used to simplify d by subsumption
+|     resolution.
+|    
+|  Input:
+|     Indices into the 'clauses' vector _c, _d, and references to the corresponding clauses c, d.
+|
+|  Result:
+|     lit_Error  - No subsumption or simplification
+|     lit_Undef  - Clause c subsumes d
+|     l          - The literal l can be deleted from d
+|________________________________________________________________________________________________@*/
+inline Lit Solver::subsumes(const Clause& c, const Clause& d)
+{
+    stats.subsumption_checks++;
+    if (d.size() < c.size() || (c.abstraction() & ~d.abstraction()) != 0)
+        return lit_Error;
+
+    Lit ret = lit_Undef;
+
+    for (int i = 0; i < c.size(); i++) {
+        // search for c[i] or ~c[i]
+        for (int j = 0; j < d.size(); j++)
+            if (c[i] == d[j])
+                goto ok;
+            else if (ret == lit_Undef && c[i] == ~d[j]){
+                ret = c[i];
+                goto ok;
+            }
+
+        // did not find it
+        stats.subsumption_misses++;
+        return lit_Error;
+    ok:;
+    }
+
+    return ret;
+}
+
+
+// Backward subsumption + backward subsumption resolution
+bool Solver::backwardSubsumptionCheck()
+{
+    while (subsumption_queue.size() > 0 || qhead < trail.size()){
+
+        // if propagation queue is non empty, take the first literal and
+        // create a dummy unit clause
+        if (qhead < trail.size()){
+            Lit l = trail[qhead++];
+            (*bwdsub_tmpunit)[0] = l;
+            assert(bwdsub_tmpunit->mark() == 0);
+            subsumption_queue.push(bwdsub_tmpunit);
+        }
+        Clause&  c = *subsumption_queue.last(); subsumption_queue.pop();
+
+        if (c.mark())
+            continue;
+
+        if (c.size() == 1 && !enqueue(c[0]))
+            return false; 
+
+        // (1) find best variable to scan
+        Var best = var(c[0]);
+        for (int i = 1; i < c.size(); i++)
+            if (occurs[var(c[i])].size() < occurs[best].size())
+                best = var(c[i]);
+
+        // (2) search all candidates
+        const vec<Clause*>& cs = getOccurs(best);
+
+        for (int j = 0; j < cs.size(); j++)
+            if (cs[j] != &c){
+                if (cs[j]->mark())
+                    continue;
+                if (c.mark())
+                    break;
+
+                //fprintf(stderr, "backward candidate "); printClause(*cs[j]); fprintf(stderr, "\n"); 
+                Lit l = subsumes(c, *cs[j]);
+                if (l == lit_Undef){
+                    //fprintf(stderr, "clause backwards subsumed\n");
+                    //fprintf(stderr, " >> clause %d: ", cs[j]->mark()); printClause(*cs[j]); fprintf(stderr, "\n");
+                    //fprintf(stderr, " >> clause %d: ", c.mark()); printClause(c); fprintf(stderr, "\n");
+                    removeClause(*cs[j], false);
+                }else if (l != lit_Error){
+                    //fprintf(stderr, "backwards subsumption resolution\n");
+                    //fprintf(stderr, " >> clause %d: ", cs[j]->mark()); printClause(*cs[j]); fprintf(stderr, "\n");
+                    //fprintf(stderr, " >> clause %d: ", c.mark()); printClause(c); fprintf(stderr, "\n");
+
+                    assert(cs[j]->size() > 1);
+                    assert(find(*cs[j], ~l));
+
+                    subsumption_queue.push(cs[j]);
+                    if (!strengthen(*cs[j], ~l))
+                        return false;
+
+                    // did current candidate get deleted from cs? then check candidate at index j again
+                    if (var(l) == best)
+                        j--;
+                }
+            }
+    }
+
+    return true;
+}
+
+
+bool Solver::eliminateVar(Var v, bool fail)
+{
+    assert(hasVarProp(v, p_frozen));
+
+    vec<Clause*>  pos, neg;
+    const vec<Clause*>& cls = getOccurs(v);
+
+    if (value(v) != l_Undef || cls.size() == 0)
+        return true;
+
+    //fprintf(stderr, "trying to eliminate var %d\n", v+1);
+    for (int i = 0; i < cls.size(); i++){
+        //fprintf(stderr, "clause: "); printClause(*cls[i]); fprintf(stderr, "\n");
+        if (find(*cls[i], Lit(v)))
+            pos.push(cls[i]);
+        else{
+            assert(find(*cls[i], ~Lit(v)));
+            neg.push(cls[i]);
+        }
+    }
+
+#ifdef WEAKEN
+    vec<int> posc(pos.size(), 0);
+    vec<int> negc(neg.size(), 0);
+#endif
+    // check if number of clauses decreases
+    int      cnt = 0;
+    vec<Lit> resolvent;
+    for (int i = 0; i < pos.size(); i++)
+        for (int j = 0; j < neg.size(); j++){
+            resolvent.clear();
+            if (merge(*pos[i], *neg[j], v, resolvent)){
+                cnt++;
+#ifdef WEAKEN
+                posc[i]++;
+                negc[j]++;
+#endif
+            }
+#ifndef WEAKEN
+            if (cnt > cls.size() + grow)
+                return true;
+#else
+#ifdef MATING
+            if (cnt > cls.size() + grow)
+                if (posc[i] > 0)
+                    break;
+#endif
+#endif
+            assert(pos.size() <= n_occ[toInt(Lit(v))]);
+            assert(neg.size() <= n_occ[toInt(~Lit(v))]);
+        }
+
+#ifdef WEAKEN
+#ifdef MATING
+    for (int i = 0; i < neg.size(); i++)
+        if (negc[i] == 0)
+            for (int j = 0; j < pos.size(); j++){
+                resolvent.clear();
+                if (merge(*neg[i], *pos[j], v, resolvent)){
+                    negc[i]++;
+                    break;
+                }
+            }
+#endif
+    for (int i = 0; i < pos.size(); i++)
+        if (posc[i] == 0)
+            removeClause(*pos[i], false);
+
+    for (int i = 0; i < neg.size(); i++)
+        if (negc[i] == 0)
+            removeClause(*neg[i], false);
+
+    if (cnt > cls.size() + grow)
+        return true;
+#endif    
+    //if (pos.size() != n_occ[toInt(Lit(v))])
+    //    fprintf(stderr, "pos.size() = %d, n_occ[toInt(Lit(v))] = %d\n", pos.size(), n_occ[toInt(Lit(v))]);
+    assert(pos.size() == n_occ[toInt(Lit(v))]);
+    //if (neg.size() != n_occ[toInt(~Lit(v))])
+    //    fprintf(stderr, "neg.size() = %d, n_occ[toInt(Lit(v))] = %d\n", neg.size(), n_occ[toInt(Lit(v))]);
+    assert(neg.size() == n_occ[toInt(~Lit(v))]);
+    assert(cnt <= cls.size() + grow);
+    setVarProp(v, p_decisionvar, false);
+
+    // produce clauses in cross product
+    int top = clauses.size();
+    for (int i = 0; i < pos.size(); i++)
+        for (int j = 0; j < neg.size(); j++){
+            resolvent.clear();
+#ifdef WEAKEN
+            if (pos[i]->mark() == 1)
+                break;
+            if (neg[j]->mark() == 1)
+                continue;
+#endif
+
+            if (merge(*pos[i], *neg[j], v, resolvent)){
+                int i, j;
+                for (i = j = 0; i < resolvent.size(); i++)
+                    if (value(resolvent[i]) == l_True)
+                        goto next;
+                    else if (value(resolvent[i]) == l_Undef)
+                        resolvent[j++] = resolvent[i];
+                resolvent.shrink(i - j);
+
+                if (resolvent.size() == 1){
+                    if (!enqueue(resolvent[0]))
+                        return false;
+                }else{
+                    int apa = clauses.size();
+                    check(newClause(resolvent, false, true));
+                    assert(apa + 1 == clauses.size());
+                }
+            }
+            next:;
+        }
+
+    if (fail){
+        fprintf(stderr, "eliminated var %d, %d <= %d\n", v+1, cnt, cls.size());
+        fprintf(stderr, "previous clauses:\n");
+        for (int i = 0; i < cls.size(); i++){
+            printClause(*cls[i]);
+            fprintf(stderr, "\n");
+        }
+        
+        fprintf(stderr, "new clauses:\n");
+        for (int i = top; i < clauses.size(); i++){
+            printClause(*clauses[i]);
+            fprintf(stderr, "\n");
+        }
+
+        assert(0); }
+
+    //fprintf(stderr, "eliminated var %d, %d <= %d\n", v+1, cnt, cls.size());
+    //fprintf(stderr, "previous clauses:\n");
+    //for (int i = 0; i < cls.size(); i++){
+    //    printClause(*cls[i]);
+    //    fprintf(stderr, "\n");
+    //}
+    //
+    //fprintf(stderr, "new clauses:\n");
+    //for (int i = top; i < clauses.size(); i++){
+    //    printClause(*clauses[i]);
+    //    fprintf(stderr, "\n");
+    //}
+
+    // delete + store old clauses
+    eliminated_var.push(v);
+    eliminated_lim.push(eliminated.size());
+    for (int i = 0; i < cls.size(); i++){
+        eliminated.push(Clause_new(*cls[i]));
+
+#ifdef WEAKEN
+        if (cls[i]->mark() == 0)
+#endif
+            removeClause(*cls[i], false); 
+
+    }
+
+    assert(subsumption_queue.size() == 0);
+    for (int i = top; i < clauses.size(); i++)
+#ifdef ASSYMM
+        if (clauses[i]->mark() == 0)
+            if (!assymmetricBranching(*clauses[i]))
+                return false;
+            else
+                subsumption_queue.push(clauses[i]);
+#else
+        if (clauses[i]->mark() == 0)
+            subsumption_queue.push(clauses[i]);
+#endif
+
+    return backwardSubsumptionCheck();
+}
+
+
+void Solver::extendModel()
+{
+    assert(eliminated_var.size() == eliminated_lim.size());
+    for (int i = eliminated_var.size()-1; i >= 0; i--){
+        Var v = eliminated_var[i];
+        Lit l = lit_Undef;
+
+        //fprintf(stderr, "extending var %d\n", v+1);
+
+        for (int j = eliminated_lim[i]; j < (i+1 >= eliminated_lim.size() ? eliminated.size() : eliminated_lim[i+1]); j++){
+            assert(j < eliminated.size());
+            Clause& c = *eliminated[j];
+
+            //fprintf(stderr, "checking clause: "); printClause(c); fprintf(stderr, "\n");
+
+            for (int k = 0; k < c.size(); k++)
+                if (var(c[k]) == v)
+                    l = c[k];
+                else if (value(c[k]) != l_False)
+                    goto next;
+
+            assert(l != lit_Undef);
+            //fprintf(stderr, "Fixing var %d to %d\n", v+1, !sign(l));
+
+            assigns[v] = toInt(lbool(!sign(l)));
+            break;
+
+        next:;
+        }
+
+        if (value(v) == l_Undef)
+            assigns[v] = toInt(l_True);
+    }
+}
+
+
+bool Solver::eliminate()
+{
+    assert(subsumption);
+
+    int cnt = 0;
+    //fprintf(stderr, "eliminating variables\n");
+
+#ifdef INVARIANTS
+    // check that all clauses are simplified
+    fprintf(stderr, "Checking that all clauses are normalized prior to variable elimination\n");
+    for (int i = 0; i < clauses.size(); i++)
+        if (clauses[i]->mark() == 0){
+            Clause& c = *clauses[i];
+            for (int j = 0; j < c.size(); j++)
+                assert(value(c[j]) == l_Undef);
+        }
+    fprintf(stderr, "done.\n");
+#endif
+
+    for (;;){
+        gather(subsumption_queue);
+
+        if (subsumption_queue.size() == 0 && heap.size() == 0)
+            break;
+
+        //fprintf(stderr, "backwards subsumption: %10d\n", subsumption_queue.size());
+        if (!backwardSubsumptionCheck())
+            return false;
+
+        //fprintf(stderr, "variable elimination:  %10d\n", heap.size());
+        cnt = 0;
+        for (;;){
+            assert(!heap.empty() || heap.size() == 0);
+            if (heap.empty())
+                break;
+
+            Var elim = heap.getmin();
+
+            assert(hasVarProp(elim, p_frozen));
+
+            //for (int i = 1; i < heap.heap.size(); i++)
+            //    assert(heap.comp(elim, heap.heap[i]) || !heap.comp(elim, heap.heap[i]));
+
+            //if (cnt++ % 100 == 0)
+            //    fprintf(stderr, "left %10d\r", heap.size());
+            
+            if (!eliminateVar(elim))
+                return false;
+        }
+    }
+#ifdef INVARIANTS
+    // check that no more subsumption is possible
+    fprintf(stderr, "Checking that no more subsumption is possible\n");
+    cnt = 0;
+    for (int i = 0; i < clauses.size(); i++){
+        if (cnt++ % 1000 == 0)
+            fprintf(stderr, "left %10d\r", clauses.size() - i);
+        for (int j = 0; j < i; j++)
+            assert(clauses[i]->mark() ||
+                   clauses[j]->mark() ||
+                   subsumes(*clauses[i], *clauses[j]) == lit_Error);
+    }
+    fprintf(stderr, "done.\n");
+
+    // check that no more elimination is possible
+    fprintf(stderr, "Checking that no more elimination is possible\n");
+    for (int i = 0; i < nVars(); i++){
+        if (hasVarProp(i, p_frozen))
+            eliminateVar(i, true);
+    }
+    fprintf(stderr, "done.\n");
+
+#endif
+
+    assert(qhead == trail.size());
+
+    return true;
+}
+};
diff --git a/stp/sat/Solver.C b/stp/sat/Solver.C
new file mode 100644
index 00000000..0fcb6149
--- /dev/null
+++ b/stp/sat/Solver.C
@@ -0,0 +1,811 @@
+/****************************************************************************************[Solver.C]
+MiniSat -- Copyright (c) 2003-2005, 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.
+**************************************************************************************************/
+
+#include "Solver.h"
+#include "Sort.h"
+#include <cmath>
+
+namespace MINISAT {
+//=================================================================================================
+// Operations on clauses:
+
+
+/*_________________________________________________________________________________________________
+|
+|  newClause : (ps : const vec<Lit>&) (learnt : bool)  ->  [void]
+|  
+|  Description:
+|    Allocate and add a new clause to the SAT solvers clause database. 
+|  
+|  Input:
+|    ps     - The new clause as a vector of literals.
+|    learnt - Is the clause a learnt clause? For learnt clauses, 'ps[0]' is assumed to be the
+|             asserting literal. An appropriate 'enqueue()' operation will be performed on this
+|             literal. One of the watches will always be on this literal, the other will be set to
+|             the literal with the highest decision level.
+|  
+|  Effect:
+|    Activity heuristics are updated.
+|________________________________________________________________________________________________@*/
+bool Solver::newClause(const vec<Lit>& ps_, bool learnt, bool normalized)
+{
+    vec<Lit>    qs;
+    if (!learnt && !normalized){
+        assert(decisionLevel() == 0);
+        ps_.copyTo(qs);             // Make a copy of the input vector.
+
+        // Remove duplicates:
+        sortUnique(qs);
+
+        // Check if clause is satisfied:
+        for (int i = 0; i < qs.size()-1; i++){
+            if (qs[i] == ~qs[i+1])
+                return true; }
+        for (int i = 0; i < qs.size(); i++){
+            if (value(qs[i]) == l_True)
+                return true; }
+
+        // Remove false literals:
+        int     i, j;
+        for (i = j = 0; i < qs.size(); i++)
+            if (value(qs[i]) != l_False)
+                qs[j++] = qs[i];
+        qs.shrink(i - j);
+    }
+    const vec<Lit>& ps = learnt || normalized ? ps_ : qs;     // 'ps' is now the (possibly) reduced vector of literals.
+
+    if (ps.size() == 0)
+        return false;
+    else if (ps.size() == 1){
+        assert(decisionLevel() == 0);
+        return enqueue(ps[0]);
+    }else{
+        // Allocate clause:
+        Clause* c   = Clause_new(ps, learnt);
+
+        if (learnt){
+            // Put the second watch on the first literal with highest decision level:
+            // (requires that this method is called at the level where the clause is asserting!)
+            int i;
+            for (i = 1; i < ps.size() && position(trailpos[var(ps[i])]) < trail_lim.last(); i++)
+                ;
+            (*c)[1] = ps[i];
+            (*c)[i] = ps[1];
+
+            // Bump, enqueue, store clause:
+            claBumpActivity(*c);        // (newly learnt clauses should be considered active)
+            check(enqueue((*c)[0], c));
+            learnts.push(c);
+            stats.learnts_literals += c->size();
+        }else{
+            // Store clause:
+            clauses.push(c);
+            stats.clauses_literals += c->size();
+
+            if (subsumption){
+                c->calcAbstraction();
+                for (int i = 0; i < c->size(); i++){
+                    assert(!find(occurs[var((*c)[i])], c));
+                    occurs[var((*c)[i])].push(c);
+                    n_occ[toInt((*c)[i])]++;
+                    touched[var((*c)[i])] = 1;
+
+                    if (heap.inHeap(var((*c)[i])))
+		      updateHeap(var((*c)[i]));
+                }
+            }
+
+        }
+        // Watch clause:
+        watches[toInt(~(*c)[0])].push(c);
+        watches[toInt(~(*c)[1])].push(c);
+    }
+
+    return true;
+}
+
+
+// Disposes a clauses and removes it from watcher lists. NOTE!
+// Low-level; does NOT change the 'clauses' and 'learnts' vector.
+//
+void Solver::removeClause(Clause& c, bool dealloc)
+{
+    //fprintf(stderr, "delete %d: ", _c); printClause(c); fprintf(stderr, "\n");
+    assert(c.mark() == 0);
+
+    if (c.size() > 1){
+        assert(find(watches[toInt(~c[0])], &c));
+        assert(find(watches[toInt(~c[1])], &c));
+        remove(watches[toInt(~c[0])], &c);
+        remove(watches[toInt(~c[1])], &c); }
+
+    if (c.learnt()) stats.learnts_literals -= c.size();
+    else            stats.clauses_literals -= c.size();
+
+    if (subsumption && !c.learnt()){
+        for (int i = 0; i < c.size(); i++){
+            if (dealloc){
+                assert(find(occurs[var(c[i])], &c));
+                remove(occurs[var(c[i])], &c); 
+            }
+            n_occ[toInt(c[i])]--;
+            updateHeap(var(c[i]));
+        }
+    }
+
+    if (dealloc)
+        xfree(&c);
+    else
+        c.mark(1);
+}
+
+
+bool Solver::satisfied(Clause& c) const
+{
+    for (int i = 0; i < c.size(); i++)
+        if (value(c[i]) == l_True)
+            return true;
+    return false; }
+
+
+bool Solver::strengthen(Clause& c, Lit l)
+{
+    assert(decisionLevel() == 0);
+    assert(c.size() > 1);
+    assert(c.mark() == 0);
+
+    assert(toInt(~c[0]) < watches.size());
+    assert(toInt(~c[1]) < watches.size());
+    
+    assert(find(watches[toInt(~c[0])], &c));
+    assert(find(watches[toInt(~c[1])], &c));
+    assert(find(c,l));
+
+    if (c.learnt()) stats.learnts_literals -= 1;
+    else            stats.clauses_literals -= 1;
+
+    if (c[0] == l || c[1] == l){
+        assert(find(watches[toInt(~l)], &c));
+        remove(c,l);
+        remove(watches[toInt(~l)], &c);
+        if (c.size() > 1){
+            assert(!find(watches[toInt(~c[1])], &c));
+            watches[toInt(~c[1])].push(&c); }
+        else {
+            assert(find(watches[toInt(~c[0])], &c));
+            remove(watches[toInt(~c[0])], &c);
+            removeClause(c, false);
+        }
+    }
+    else
+        remove(c,l);
+        
+    assert(c.size() == 1 || find(watches[toInt(~c[0])], &c));
+    assert(c.size() == 1 || find(watches[toInt(~c[1])], &c));
+
+    if (subsumption){
+        assert(find(occurs[var(l)], &c));
+        remove(occurs[var(l)], &c);
+        assert(!find(occurs[var(l)], &c));
+
+        c.calcAbstraction();
+
+        n_occ[toInt(l)]--;
+        updateHeap(var(l));
+    }
+
+    return c.size() == 1 ? enqueue(c[0]) : true;
+}
+
+
+//=================================================================================================
+// Minor methods:
+
+
+// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be
+// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
+//
+Var Solver::newVar(bool polarity, bool dvar) {
+    int     index;
+    index = nVars();
+    watches     .push();          // (list for positive literal)
+    watches     .push();          // (list for negative literal)
+    reason      .push(NULL);
+    assigns     .push(toInt(l_Undef));
+    trailpos    .push(TrailPos(0,0));
+    activity    .push(0);
+    order       .newVar(polarity,dvar);
+    seen        .push(0);
+    touched     .push(0);
+    if (subsumption){
+        occurs  .push();
+        n_occ   .push(0);
+        n_occ   .push(0);
+        heap    .setBounds(index+1);
+    }
+    return index; }
+
+
+// Returns FALSE if immediate conflict.
+bool Solver::assume(Lit p) {
+    trail_lim.push(trail.size());
+    return enqueue(p); }
+
+
+// Revert to the state at given level.
+void Solver::cancelUntil(int level) {
+    if (decisionLevel() > level){
+        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
+            Var     x  = var(trail[c]);
+            assigns[x] = toInt(l_Undef);
+            reason [x] = NULL; 
+            order.undo(x); }
+        qhead = trail_lim[level];
+        trail.shrink(trail.size() - trail_lim[level]);
+        trail_lim.shrink(trail_lim.size() - level);
+    }
+}
+
+
+//=================================================================================================
+// Major methods:
+
+
+/*_________________________________________________________________________________________________
+|
+|  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->  [void]
+|  
+|  Description:
+|    Analyze conflict and produce a reason clause.
+|  
+|    Pre-conditions:
+|      * 'out_learnt' is assumed to be cleared.
+|      * Current decision level must be greater than root level.
+|  
+|    Post-conditions:
+|      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
+|  
+|  Effect:
+|    Will undo part of the trail, upto but not beyond the assumption of the current decision level.
+|________________________________________________________________________________________________@*/
+void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
+{
+    int            pathC = 0;
+    int            btpos = -1;
+    Lit            p     = lit_Undef;
+
+    // Generate conflict clause:
+    //
+    out_learnt.push();      // (leave room for the asserting literal)
+    int index = trail.size()-1;
+    do{
+        assert(confl != NULL);          // (otherwise should be UIP)
+        Clause& c = *confl;
+
+        if (c.learnt())
+            claBumpActivity(c);
+
+        for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
+            Lit q = c[j];
+            if (!seen[var(q)] && position(trailpos[var(q)]) >= trail_lim[0]){
+	      varBumpActivity(q);
+                seen[var(q)] = 1;
+                if (position(trailpos[var(q)]) >= trail_lim.last())
+                    pathC++;
+                else{
+                    out_learnt.push(q);
+                    btpos = max(btpos, position(trailpos[var(q)]));
+                }
+            }
+        }
+
+        // Select next clause to look at:
+        while (!seen[var(trail[index--])]);
+        p     = trail[index+1];
+        confl = reason[var(p)];
+        seen[var(p)] = 0;
+        pathC--;
+
+    }while (pathC > 0);
+    out_learnt[0] = ~p;
+
+    // Find correct backtrack level
+    for (out_btlevel = trail_lim.size()-1; out_btlevel > 0 && trail_lim[out_btlevel-1] > btpos; out_btlevel--)
+        ;
+
+    int     i, j;
+    if (expensive_ccmin){
+        // Simplify conflict clause (a lot):
+        //
+        uint    min_level = 0;
+        for (i = 1; i < out_learnt.size(); i++)
+            min_level |= abstractLevel(trailpos[var(out_learnt[i])]);     // (maintain an abstraction of levels involved in conflict)
+
+        out_learnt.copyTo(analyze_toclear);
+        for (i = j = 1; i < out_learnt.size(); i++)
+            if (reason[var(out_learnt[i])] == NULL || !analyze_removable(out_learnt[i], min_level))
+                out_learnt[j++] = out_learnt[i];
+    }else{
+        // Simplify conflict clause (a little):
+        //
+        out_learnt.copyTo(analyze_toclear);
+        for (i = j = 1; i < out_learnt.size(); i++){
+            Clause& c = *reason[var(out_learnt[i])];
+            for (int k = 1; k < c.size(); k++)
+                if (!seen[var(c[k])] && position(trailpos[var(c[k])]) >= trail_lim[0]){
+                    out_learnt[j++] = out_learnt[i];
+                    break; }
+        }
+    }
+
+    stats.max_literals += out_learnt.size();
+    out_learnt.shrink(i - j);
+    stats.tot_literals += out_learnt.size();
+
+    for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
+}
+
+
+// Check if 'p' can be removed. 'min_level' is used to abort early if visiting literals at a level that cannot be removed.
+//
+bool Solver::analyze_removable(Lit p, uint min_level)
+{
+    analyze_stack.clear(); analyze_stack.push(p);
+    int top = analyze_toclear.size();
+    while (analyze_stack.size() > 0){
+        assert(reason[var(analyze_stack.last())] != NULL);
+        Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop();
+
+        for (int i = 1; i < c.size(); i++){
+            Lit      p   = c[i];
+            TrailPos tp = trailpos[var(p)];
+            if (!seen[var(p)] && position(tp) >= trail_lim[0]){
+                if (reason[var(p)] != NULL && (abstractLevel(tp) & min_level) != 0){
+                    seen[var(p)] = 1;
+                    analyze_stack.push(p);
+                    analyze_toclear.push(p);
+                }else{
+                    for (int j = top; j < analyze_toclear.size(); j++)
+                        seen[var(analyze_toclear[j])] = 0;
+                    analyze_toclear.shrink(analyze_toclear.size() - top);
+                    return false;
+                }
+            }
+        }
+    }
+
+    return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  analyzeFinal : (p : Lit) ->  [void]
+|  
+|  Description:
+|    Specialized analysis procedure to express the final conflict in terms of assumptions.
+|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
+|    stores the result in 'out_conflict'.
+|________________________________________________________________________________________________@*/
+void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
+{
+    out_conflict.clear();
+    out_conflict.push(p);
+
+    if (decisionLevel() == 0)
+        return;
+
+    seen[var(p)] = 1;
+
+    int start = position(trailpos[var(p)]);
+    for (int i = start; i >= trail_lim[0]; i--){
+        Var     x = var(trail[i]);
+        if (seen[x]){
+            if (reason[x] == NULL){
+                assert(position(trailpos[x]) >= trail_lim[0]);
+                out_conflict.push(~trail[i]);
+            }else{
+                Clause& c = *reason[x];
+                for (int j = 1; j < c.size(); j++)
+                    if (position(trailpos[var(c[j])]) >= trail_lim[0])
+                        seen[var(c[j])] = 1;
+            }
+            seen[x] = 0;
+        }
+    }
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  enqueue : (p : Lit) (from : Clause*)  ->  [bool]
+|  
+|  Description:
+|    Puts a new fact on the propagation queue as well as immediately updating the variable's value.
+|    Should a conflict arise, FALSE is returned.
+|  
+|  Input:
+|    p    - The fact to enqueue
+|    from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'.
+|           Default value is NULL (no reason).
+|  
+|  Output:
+|    TRUE if fact was enqueued without conflict, FALSE otherwise.
+|________________________________________________________________________________________________@*/
+bool Solver::enqueue(Lit p, Clause* from)
+{
+
+    if (value(p) != l_Undef)
+        return value(p) != l_False;
+    else{
+        assigns [var(p)] = toInt(lbool(!sign(p)));
+        trailpos[var(p)] = TrailPos(trail.size(),decisionLevel());
+        reason  [var(p)] = from;
+        trail.push(p);
+        return true;
+    }
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  propagate : [void]  ->  [Clause*]
+|  
+|  Description:
+|    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
+|    otherwise NULL.
+|  
+|    Post-conditions:
+|      * the propagation queue is empty, even if there was a conflict.
+|________________________________________________________________________________________________@*/
+Clause* Solver::propagate()
+{
+    if (decisionLevel() == 0 && subsumption)
+        return backwardSubsumptionCheck() ? NULL : propagate_tmpempty;
+
+    Clause* confl = NULL;
+    //fprintf(stderr, "propagate, qhead = %d, qtail = %d\n", qhead, qtail);
+    while (qhead < trail.size()){
+        stats.propagations++;
+        simpDB_props--;
+
+        Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
+        vec<Clause*>&  ws  = watches[toInt(p)];
+        Clause         **i, **j, **end;
+
+        for (i = j = (Clause**)ws, end = i + ws.size();  i != end;){
+            Clause& c = **i++;
+            
+            // Make sure the false literal is data[1]:
+            Lit false_lit = ~p;
+            if (c[0] == false_lit)
+                c[0] = c[1], c[1] = false_lit;
+
+            assert(c[1] == false_lit);
+
+            // If 0th watch is true, then clause is already satisfied.
+            Lit first = c[0];
+            if (value(first) == l_True){
+                *j++ = &c;
+            }else{
+                // Look for new watch:
+                for (int k = 2; k < c.size(); k++)
+                    if (value(c[k]) != l_False){
+                        c[1] = c[k]; c[k] = false_lit;
+                        watches[toInt(~c[1])].push(&c);
+                        goto FoundWatch; }
+
+                // Did not find watch -- clause is unit under assignment:
+                *j++ = &c;
+                if (!enqueue(first, &c)){
+                    confl = &c;
+                    qhead = trail.size();
+                    // Copy the remaining watches:
+                    while (i < end)
+                        *j++ = *i++;
+                }
+            FoundWatch:;
+            }
+        }
+        ws.shrink(i - j);
+    }
+
+    return confl;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  reduceDB : ()  ->  [void]
+|  
+|  Description:
+|    Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
+|    clauses are clauses that are reason to some assignment. Binary clauses are never removed.
+|________________________________________________________________________________________________@*/
+struct reduceDB_lt { bool operator () (Clause* x, Clause* y) { return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity()); } };
+void Solver::reduceDB()
+{
+    int     i, j;
+    double  extra_lim = cla_inc / learnts.size();    // Remove any clause below this activity
+
+    sort(learnts, reduceDB_lt());
+    for (i = j = 0; i < learnts.size() / 2; i++){
+        if (learnts[i]->size() > 2 && !locked(*learnts[i]))
+            removeClause(*learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    for (; i < learnts.size(); i++){
+        if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() < extra_lim)
+            removeClause(*learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    learnts.shrink(i - j);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  simplifyDB : [void]  ->  [bool]
+|  
+|  Description:
+|    Simplify the clause database according to the current top-level assigment. Currently, the only
+|    thing done here is the removal of satisfied clauses, but more things can be put here.
+|________________________________________________________________________________________________@*/
+bool Solver::simplifyDB(bool expensive)
+{
+    assert(decisionLevel() == 0);
+    if (!ok || propagate() != NULL)
+        return ok = false;
+
+    if (nAssigns() == simpDB_assigns || 
+        (!subsumption && simpDB_props > 0)) // (nothing has changed or preformed a simplification too recently)
+        return true;
+
+    if (subsumption){
+        if (expensive && !eliminate())
+            return ok = false;
+
+        // Move this cleanup code to its own method ?
+        int      i , j;
+        vec<Var> dirty;
+        for (i = 0; i < clauses.size(); i++)
+            if (clauses[i]->mark() == 1){
+                Clause& c = *clauses[i];
+                for (int k = 0; k < c.size(); k++)
+                    if (!seen[var(c[k])]){
+                        seen[var(c[k])] = 1;
+                        dirty.push(var(c[k]));
+                    }
+            }
+        
+        for (i = 0; i < dirty.size(); i++){
+            cleanOcc(dirty[i]);
+            seen[dirty[i]] = 0;
+        }
+
+        for (i = j = 0; i < clauses.size(); i++)
+            if (clauses[i]->mark() == 1)
+                xfree(clauses[i]);
+            else
+                clauses[j++] = clauses[i];
+        clauses.shrink(i - j);
+    }
+
+    // Remove satisfied clauses:
+    for (int type = 0; type < (subsumption ? 1 : 2); type++){  // (only scan learnt clauses if subsumption is on)
+        vec<Clause*>& cs = type ? learnts : clauses;
+        int     j  = 0;
+        for (int i = 0; i < cs.size(); i++){
+            assert(cs[i]->mark() == 0);
+            if (satisfied(*cs[i]))
+                removeClause(*cs[i]);
+            else
+                cs[j++] = cs[i];
+        }
+        cs.shrink(cs.size()-j);
+    }
+    order.cleanup();
+
+    simpDB_assigns = nAssigns();
+    simpDB_props   = stats.clauses_literals + stats.learnts_literals;   // (shouldn't depend on 'stats' really, but it will do for now)
+
+    return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&)  ->  [lbool]
+|  
+|  Description:
+|    Search for a model the specified number of conflicts, keeping the number of learnt clauses
+|    below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to
+|    indicate infinity.
+|  
+|  Output:
+|    'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
+|    all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
+|    if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
+|________________________________________________________________________________________________@*/
+lbool Solver::search(int nof_conflicts, int nof_learnts)
+{
+    assert(ok);
+    int         backtrack_level;
+    int         conflictC = 0;
+    vec<Lit>    learnt_clause;
+
+    stats.starts++;
+    var_decay = 1 / params.var_decay;
+    cla_decay = 1 / params.clause_decay;
+
+    for (;;){
+        Clause* confl = propagate();
+        if (confl != NULL){
+            // CONFLICT
+            stats.conflicts++; conflictC++;
+            if (decisionLevel() == 0) return l_False;
+
+            learnt_clause.clear();
+            analyze(confl, learnt_clause, backtrack_level);
+            cancelUntil(backtrack_level);
+            newClause(learnt_clause, true);
+            varDecayActivity();
+            claDecayActivity();
+
+        }else{
+            // NO CONFLICT
+
+            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+                // Reached bound on number of conflicts:
+                progress_estimate = progressEstimate();
+                cancelUntil(0);
+                return l_Undef; }
+
+            // Simplify the set of problem clauses:
+            if (decisionLevel() == 0 && !simplifyDB())
+                return l_False;
+
+            if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts)
+                // Reduce the set of learnt clauses:
+                reduceDB();
+
+            Lit next = lit_Undef;
+
+            if (decisionLevel() < assumptions.size()){
+                // Perform user provided assumption:
+                next = assumptions[decisionLevel()]; 
+                if (value(next) == l_False){
+                    analyzeFinal(~next, conflict);
+                    return l_False; }
+            }else{
+                // New variable decision:
+                stats.decisions++;
+                next = order.select(params.random_var_freq, decisionLevel());		
+	    }
+            if (next == lit_Undef)
+                // Model found:
+                return l_True;
+
+            check(assume(next));
+        }
+    }
+}
+
+
+// Return search-space coverage. Not extremely reliable.
+//
+double Solver::progressEstimate()
+{
+    double  progress = 0;
+    double  F = 1.0 / nVars();
+
+    for (int i = 0; i <= decisionLevel(); i++){
+        int beg = i == 0 ? 0 : trail_lim[i - 1];
+        int end = i == decisionLevel() ? trail.size() : trail_lim[i];
+        progress += pow(F, i) * (end - beg);
+    }
+
+    return progress / nVars();
+}
+
+
+// Divide all variable activities by 1e100.
+//
+void Solver::varRescaleActivity()
+{
+    for (int i = 0; i < nVars(); i++)
+        activity[i] *= 1e-100;
+    var_inc *= 1e-100;
+}
+
+
+// Divide all constraint activities by 1e100.
+//
+void Solver::claRescaleActivity()
+{
+    for (int i = 0; i < learnts.size(); i++)
+        learnts[i]->activity() *= 1e-20;
+    cla_inc *= 1e-20;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  solve : (assumps : const vec<Lit>&)  ->  [bool]
+|  
+|  Description:
+|    Top-level solve.
+|________________________________________________________________________________________________@*/
+bool Solver::solve(const vec<Lit>& assumps)
+{
+    model.clear();
+    conflict.clear();
+
+    if (!simplifyDB(true)) return false;
+
+
+    double  nof_conflicts = params.restart_first;
+    double  nof_learnts   = nClauses() * params.learntsize_factor;
+    lbool   status        = l_Undef;
+    assumps.copyTo(assumptions);
+
+    if (verbosity >= 1){
+        reportf("==================================[MINISAT]====================================\n");
+        reportf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
+        reportf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
+        reportf("===============================================================================\n");
+    }
+
+    // Search:
+    while (status == l_Undef){
+        if (verbosity >= 1)
+            //reportf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100);
+            reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)stats.conflicts, order.size(), nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (double)stats.learnts_literals/nLearnts(), progress_estimate*100);
+        status = search((int)nof_conflicts, (int)nof_learnts);
+        nof_conflicts *= params.restart_inc;
+        nof_learnts   *= params.learntsize_inc;
+    }
+
+    if (verbosity >= 1)
+        reportf("==============================================================================\n");
+
+    if (status == l_True){
+        // Copy model:
+        extendModel();
+#if 1
+        //fprintf(stderr, "Verifying model.\n");
+        for (int i = 0; i < clauses.size(); i++)
+            assert(satisfied(*clauses[i]));
+        for (int i = 0; i < eliminated.size(); i++)
+            assert(satisfied(*eliminated[i]));
+#endif
+        model.growTo(nVars());
+        for (int i = 0; i < nVars(); i++) model[i] = value(i);
+    }else{
+        assert(status == l_False);
+        if (conflict.size() == 0)
+            ok = false;
+    }
+
+    cancelUntil(0);
+    return status == l_True;
+}
+};//end of MINISAT namespace
diff --git a/stp/sat/Solver.h b/stp/sat/Solver.h
new file mode 100644
index 00000000..829194cc
--- /dev/null
+++ b/stp/sat/Solver.h
@@ -0,0 +1,359 @@
+/****************************************************************************************[Solver.h]
+MiniSat -- Copyright (c) 2003-2005, 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 Solver_h
+#define Solver_h
+
+#include "SolverTypes.h"
+#include "VarOrder.h"
+
+namespace MINISAT {
+// Redfine if you want output to go somewhere else:
+#define reportf(format, args...) ( printf(format , ## args), fflush(stdout) )
+
+
+//=================================================================================================
+// Solver -- the main class:
+struct SolverStats {
+    int64   starts, decisions, propagations, conflicts;
+    int64   clauses_literals, learnts_literals, max_literals, tot_literals;
+    int64   subsumption_checks, subsumption_misses, merges;
+    SolverStats() : 
+        starts(0), decisions(0), propagations(0), conflicts(0)
+      , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) 
+      , subsumption_checks(0), subsumption_misses(0), merges(0)
+    { }
+};
+
+
+struct SearchParams {
+    double  var_decay, clause_decay, random_var_freq;
+    double  restart_inc, learntsize_inc, learntsize_factor;
+    int     restart_first;
+    
+    SearchParams(double v = 0.95, double c = 0.999, double r = 0.02,
+                 double ri = 1.5, double li = 1.1, double lf = (double)1/(double)3,
+                 int rf = 100) : 
+        var_decay(v), clause_decay(c), random_var_freq(r),
+        restart_inc(ri), learntsize_inc(li), learntsize_factor(lf),
+        restart_first(rf) { }
+};
+
+  struct ElimLt {
+    const vec<int>& n_occ;
+    
+    ElimLt(const vec<int>& no) : n_occ(no) {}
+    int  cost      (Var x)        const { return n_occ[toInt(Lit(x))] * n_occ[toInt(~Lit(x))]; }
+    bool operator()(Var x, Var y) const { return cost(x) < cost(y); } 
+  };
+
+class Solver {
+protected:
+    // Solver state:    
+    bool                ok;               // If FALSE,the constraints are already unsatisfiable. 
+                                          // No part of solver state may be used!
+    vec<Clause*>        clauses;          // List of problem clauses.
+    vec<Clause*>        learnts;          // List of learnt clauses.
+    int                 n_bin_clauses;    // Keep track of number of binary clauses "inlined" into the watcher lists (we do this primarily to get identical behavior to the version without the binary clauses trick).
+    double              cla_inc;          // Amount to bump next clause with.
+    double              cla_decay;        // INVERSE decay factor for clause activity: stores 1/decay.
+
+    vec<double>         activity;         // A heuristic measurement of the activity of a variable.
+    double              var_inc;          // Amount to bump next variable with.
+    double              var_decay;        // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
+    VarOrder            order;            // Keeps track of the decision variable order.
+    vec<char>           properties;       // TODO: describe!!!
+
+    vec<vec<Clause*> >  watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
+    vec<char>           assigns;          // The current assignments (lbool:s stored as char:s).
+    vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.
+    vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail'.
+    vec<Clause*>        reason;           // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
+    vec<TrailPos>       trailpos;         // 'trailpos[var]' contains the position in the trail at wich the assigment was made.
+    int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
+    int                 simpDB_assigns;   // Number of top-level assignments since last execution of 'simplifyDB()'.
+    int64               simpDB_props;     // Remaining number of propagations that must be made before next execution of 'simplifyDB()'.
+    vec<Lit>            assumptions;      // Current set of assumptions provided to solve by the user.
+
+    bool                subsumption;
+    vec<char>           touched;
+    vec<vec<Clause*> >  occurs;
+    vec<int>            n_occ;
+    Heap<ElimLt>        heap;
+    vec<Clause*>        subsumption_queue;
+
+    vec<Clause*>        eliminated;
+    vec<int>            eliminated_lim;
+    vec<Var>            eliminated_var;
+
+    // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
+    // used, exept 'seen' wich is used in several places.
+    //
+    vec<char>           seen;
+    vec<Lit>            analyze_stack;
+    vec<Lit>            analyze_toclear;
+    Clause*             propagate_tmpempty;
+    Clause*             propagate_tmpbin;
+    Clause*             analyze_tmpbin;
+    Clause*             bwdsub_tmpunit;
+
+    vec<Lit>            addBinary_tmp;
+    vec<Lit>            addTernary_tmp;
+
+    // Main internal methods:
+    //
+    bool        assume           (Lit p);
+    void        cancelUntil      (int level);
+    void        record           (const vec<Lit>& clause);
+
+    void        analyze          (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
+    bool        analyze_removable(Lit p, uint min_level);                                 // (helper method for 'analyze()')
+    void        analyzeFinal     (Lit p, vec<Lit>& out_conflict);
+    bool        enqueue          (Lit fact, Clause* from = NULL);
+    Clause*     propagate        ();
+    void        reduceDB         ();
+    Lit         pickBranchLit    ();
+    lbool       search           (int nof_conflicts, int nof_learnts);
+    double      progressEstimate ();
+
+    // Variable properties:
+    void        setVarProp (Var v, uint prop, bool b) { order.setVarProp(v, prop, b); }
+    bool        hasVarProp (Var v, uint prop) const   { return order.hasVarProp(v, prop); }
+    void        updateHeap (Var v) { 
+        if (hasVarProp(v, p_frozen))
+            heap.update(v); }
+
+    // Simplification methods:
+    //
+    void cleanOcc (Var v) {
+        assert(subsumption);
+        vec<Clause*>& occ = occurs[v];
+        int i, j;
+        for (i = j = 0; i < occ.size(); i++)
+            if (occ[i]->mark() != 1)
+                occ[j++] = occ[i];
+        occ.shrink(i - j); 
+    }
+
+    vec<Clause*>& getOccurs                (Var x) { cleanOcc(x); return occurs[x]; }
+    void          gather                   (vec<Clause*>& clauses);
+    Lit           subsumes                 (const Clause& c, const Clause& d);
+    bool          assymmetricBranching     (Clause& c);
+    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
+    
+    bool          backwardSubsumptionCheck ();
+    bool          eliminateVar             (Var v, bool fail = false);
+    bool          eliminate                ();
+    void          extendModel              ();
+
+    // Activity:
+    //
+    void     varBumpActivity(Lit p) {
+        if (var_decay < 0) return;     // (negative decay means static variable order -- don't bump)
+        if ( (activity[var(p)] += var_inc) > 1e100 ) varRescaleActivity();
+        order.update(var(p)); }
+    void     varDecayActivity  () { if (var_decay >= 0) var_inc *= var_decay; }
+    void     varRescaleActivity();
+    void     claDecayActivity  () { cla_inc *= cla_decay; }
+    void     claRescaleActivity();
+
+    // Operations on clauses:
+    //
+    bool     newClause(const vec<Lit>& ps, bool learnt = false, bool normalized = false);
+    void     claBumpActivity (Clause& c) { if ( (c.activity() += cla_inc) > 1e20 ) claRescaleActivity(); }
+    bool     locked          (const Clause& c) const { return reason[var(c[0])] == &c; }
+    bool     satisfied       (Clause& c) const;
+    bool     strengthen      (Clause& c, Lit l);
+    void     removeClause    (Clause& c, bool dealloc = true);
+
+    int      decisionLevel() const { return trail_lim.size(); }
+
+public:
+    Solver() : ok               (true)
+             , n_bin_clauses    (0)
+             , cla_inc          (1)
+             , cla_decay        (1)
+             , var_inc          (1)
+             , var_decay        (1)
+             , order            (assigns, activity)
+             , qhead            (0)
+             , simpDB_assigns   (-1)
+             , simpDB_props     (0)
+             , subsumption      (true)
+             , heap             (n_occ)
+             , params           ()
+             , expensive_ccmin  (true)
+             , verbosity        (0)
+             , progress_estimate(0)
+             {
+                vec<Lit> dummy(2,lit_Undef);
+                propagate_tmpbin   = Clause_new(dummy);
+                analyze_tmpbin     = Clause_new(dummy);
+                dummy.pop();
+                bwdsub_tmpunit     = Clause_new(dummy);
+                dummy.pop();
+                propagate_tmpempty = Clause_new(dummy);
+                addBinary_tmp .growTo(2);
+                addTernary_tmp.growTo(3);
+             }
+
+   ~Solver() {
+       xfree(propagate_tmpbin);
+       xfree(analyze_tmpbin);
+       xfree(bwdsub_tmpunit);
+       xfree(propagate_tmpempty);
+       for (int i = 0; i < eliminated.size(); i++) xfree(eliminated[i]);
+       for (int i = 0; i < learnts.size();    i++) xfree(learnts[i]);
+       for (int i = 0; i < clauses.size();    i++) xfree(clauses[i]); }
+
+    // Helpers: (semi-internal)
+    //
+    lbool   value(Var x) const { return toLbool(assigns[x]); }
+    lbool   value(Lit p) const { return sign(p) ? ~toLbool(assigns[var(p)]) : toLbool(assigns[var(p)]); }
+
+    int     nAssigns()   { return trail.size(); }
+    int     nClauses()   { return clauses.size(); }
+    int     nLearnts()   { return learnts.size(); }
+    int     nConflicts() { return (int)stats.conflicts; }
+
+    // Statistics: (read-only member variable)
+    //
+    SolverStats     stats;
+
+    // Mode of operation:
+    //
+    SearchParams    params;             // Restart frequency etc.
+    bool            expensive_ccmin;    // Controls conflict clause minimization. TRUE by default.
+    int             verbosity;          // Verbosity level. 0=silent, 1=some progress report, 2=everything
+
+    // Problem specification:
+    //
+    Var     newVar    (bool polarity = true, bool dvar = true);
+    int     nVars     ()                    { return assigns.size(); }
+    bool    addUnit   (Lit p)               { return ok && (ok = enqueue(p)); }
+    bool    addBinary (Lit p, Lit q)        { addBinary_tmp [0] = p; addBinary_tmp [1] = q; return addClause(addBinary_tmp); }
+    bool    addTernary(Lit p, Lit q, Lit r) { addTernary_tmp[0] = p; addTernary_tmp[1] = q; addTernary_tmp[2] = r; return addClause(addTernary_tmp); }
+    bool    addClause (const vec<Lit>& ps)  { if (ok && !newClause(ps)) ok = false; return ok; }
+
+    // Variable mode:
+    // 
+    void    freezeVar    (Var v) { setVarProp(v, p_frozen, true); updateHeap(v); }
+
+    // Solving:
+    //
+    bool    okay         () { return ok; }       // FALSE means solver is in a conflicting state
+    bool    simplifyDB   (bool expensive = true);
+    bool    solve        (const vec<Lit>& assumps);
+    bool    solve        () { vec<Lit> tmp; return solve(tmp); }
+    void    turnOffSubsumption() {
+        subsumption = false;
+        occurs.clear(true);
+        n_occ.clear(true);
+    }
+
+    double      progress_estimate;  // Set by 'search()'.
+    vec<lbool>  model;              // If problem is satisfiable, this vector contains the model (if any).
+    vec<Lit>    conflict;           // If problem is unsatisfiable (possibly under assumptions), this vector represent the conflict clause expressed in the assumptions.
+
+  double  returnActivity(int i) { return activity[i];}
+  void    updateInitialActivity(int i, double act) {activity[i] = act; order.heap.update(i);}
+};
+
+
+//=================================================================================================
+// Debug:
+
+
+#define L_LIT    "%sx%d"
+#define L_lit(p) sign(p)?"~":"", var(p)
+
+// Just like 'assert()' but expression will be evaluated in the release version as well.
+inline void check(bool expr) { assert(expr); }
+
+static void printLit(Lit l)
+{
+    fprintf(stderr, "%s%d", sign(l) ? "-" : "", var(l)+1);
+}
+
+template<class C>
+static void printClause(const C& c)
+{
+    for (int i = 0; i < c.size(); i++){
+        printLit(c[i]);
+        fprintf(stderr, " ");
+    }
+}
+
+//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+#ifdef _MSC_VER
+
+#include <ctime>
+
+static inline double cpuTime(void) {
+    return (double)clock() / CLOCKS_PER_SEC; }
+
+static inline int64 memUsed() {
+    return 0; }
+
+//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+#else
+
+#include <sys/time.h>
+#include <sys/resource.h>
+
+static inline double cpuTime(void) {
+    struct rusage ru;
+    getrusage(RUSAGE_SELF, &ru);
+    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
+
+#if defined(__linux__) || defined(__CYGWIN__)
+static inline int memReadStat(int field)
+{
+    char    name[256];
+    pid_t pid = getpid();
+    sprintf(name, "/proc/%d/statm", pid);
+    FILE*   in = fopen(name, "rb");
+    if (in == NULL) return 0;
+    int     value;
+    for (; field >= 0; field--) {
+      int res = fscanf(in, "%d", &value);
+      (void) res;
+    }
+    fclose(in);
+    return value;
+}
+
+static inline int64 memUsed() { return (int64)memReadStat(0) * (int64)getpagesize(); }
+#else
+// use this by default. Mac OS X (Darwin) does not define an os type
+//defined(__FreeBSD__)
+
+static inline int64 memUsed(void) {
+    struct rusage ru;
+    getrusage(RUSAGE_SELF, &ru);
+    return ru.ru_maxrss*1024; }
+
+#endif
+
+//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+#endif
+
+//=================================================================================================
+};
+#endif
diff --git a/stp/sat/SolverTypes.h b/stp/sat/SolverTypes.h
new file mode 100644
index 00000000..2b98b8ca
--- /dev/null
+++ b/stp/sat/SolverTypes.h
@@ -0,0 +1,127 @@
+/***********************************************************************************[SolverTypes.h]
+MiniSat -- Copyright (c) 2003-2005, 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 SolverTypes_h
+#define SolverTypes_h
+
+#include "Global.h"
+
+namespace MINISAT {
+
+//=================================================================================================
+// Variables, literals, clause IDs:
+
+
+// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
+// so that they can be used as array indices.
+
+typedef int Var;
+#define var_Undef (-1)
+
+
+struct Lit {
+    int     x;
+
+    Lit() : x(2*var_Undef)                                              { }   // (lit_Undef)
+    explicit Lit(Var var, bool sign = false) : x((var+var) + (int)sign) { }
+};
+
+// Don't use these for constructing/deconstructing literals. Use the normal constructors instead.
+inline  int  toInt       (Lit p)           { return p.x; }                   // A "toInt" method that guarantees small, positive integers suitable for array indexing.
+inline  Lit  toLit       (int i)           { Lit p; p.x = i; return p; }     // Inverse of 'toInt()'
+
+inline  Lit  operator   ~(Lit p)           { Lit q; q.x = p.x ^ 1; return q; }
+inline  bool sign        (Lit p)           { return p.x & 1; }
+inline  int  var         (Lit p)           { return p.x >> 1; }
+inline  Lit  unsign      (Lit p)           { Lit q; q.x = p.x & ~1; return q; }
+inline  Lit  id          (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; }
+
+inline  bool operator == (Lit p, Lit q)    { return toInt(p) == toInt(q); }
+inline  bool operator != (Lit p, Lit q)    { return toInt(p) != toInt(q); }
+inline  bool operator <  (Lit p, Lit q)    { return toInt(p)  < toInt(q); }  // '<' guarantees that p, ~p are adjacent in the ordering.
+
+
+const Lit lit_Undef(var_Undef, false);  // }- Useful special constants.
+const Lit lit_Error(var_Undef, true );  // }
+
+
+//=================================================================================================
+// Clause -- a simple class for representing a clause:
+
+class Clause {
+    uint    size_etc;
+    union { float act; uint abst; } apa;
+    Lit     data[0];
+public:
+    // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
+    template<class V>
+    Clause(const V& ps, bool learnt) {
+        size_etc = (ps.size() << 3) | (uint)learnt;
+        for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
+        if (learnt) apa.act = 0; else apa.abst = 0; }
+
+    // -- use this function instead:
+    template<class V>
+    friend Clause* Clause_new(const V& ps, bool learnt = false) {
+        assert(sizeof(Lit)      == sizeof(uint));
+        assert(sizeof(float)    == sizeof(uint));
+        void*   mem = xmalloc<char>(sizeof(Clause) + sizeof(uint)*(ps.size()));
+        return new (mem) Clause(ps, learnt); }
+
+    int       size        ()      const { return size_etc >> 3; }
+    void      shrink      (int i)       { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); }
+    void      pop         ()            { shrink(1); }
+    bool      learnt      ()      const { return size_etc & 1; }
+    uint      mark        ()      const { return (size_etc >> 1) & 3; }
+    void      mark        (uint m)      { size_etc = (size_etc & ~6) | ((m & 3) << 1); }
+    Lit       operator [] (int i) const { return data[i]; }
+    Lit&      operator [] (int i)       { return data[i]; }
+
+    float&    activity    ()       { return apa.act; }
+
+    uint      abstraction () const { return apa.abst; }
+
+    void calcAbstraction() {
+        uint abstraction = 0;
+        for (int i = 0; i < size(); i++)
+            abstraction |= 1 << (var(data[i]) & 31);
+        apa.abst = abstraction;  }
+};
+
+
+//=================================================================================================
+// TrailPos -- Stores an index into the trail as well as an approximation of a level. This data
+// is recorded for each assigment. (Replaces the old level information)
+
+
+class TrailPos {
+    int tp;
+ public:
+    explicit TrailPos(int index, int level) : tp( (index << 5) + (level & 31) ) { }
+
+    friend int abstractLevel(const TrailPos& p) { return 1 << (p.tp & 31); }
+    friend int position     (const TrailPos& p) { return p.tp >> 5; }
+
+    bool operator ==  (TrailPos other) const { return tp == other.tp; }
+    bool operator <   (TrailPos other) const { return tp <  other.tp; }
+};
+
+};
+#endif
diff --git a/stp/sat/Sort.h b/stp/sat/Sort.h
new file mode 100644
index 00000000..a7011edb
--- /dev/null
+++ b/stp/sat/Sort.h
@@ -0,0 +1,133 @@
+/******************************************************************************************[Sort.h]
+MiniSat -- Copyright (c) 2003-2005, 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
+
+
+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, double& seed)
+{
+    if (size <= 15)
+        selectionSort(array, size, lt);
+
+    else{
+        T           pivot = array[irand(seed, size)];
+        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, seed);
+        sort(&array[i], size-i, lt, seed);
+    }
+}
+template <class T, class LessThan> void sort(T* array, int size, LessThan lt) {
+    double  seed = 91648253; sort(array, size, lt, seed); }
+template <class T> static inline void sort(T* array, int size) {
+    sort(array, size, LessThan_default<T>()); }
+
+
+template <class T, class LessThan>
+void sortUnique(T* array, int& size, LessThan lt)
+{
+    int         i, j;
+    T           last;
+
+    if (size == 0) return;
+
+    sort(array, size, lt);
+
+    i    = 1;
+    last = array[0];
+    for (j = 1; j < size; j++){
+        if (lt(last, array[j])){
+            last = array[i] = array[j];
+            i++; }
+    }
+
+    size = i;
+}
+template <class T> static inline void sortUnique(T* array, int& size) {
+    sortUnique(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>()); }
+
+
+template <class T, class LessThan> void sortUnique(vec<T>& v, LessThan lt) {
+    int     size = v.size();
+    T*      data = v.release();
+    sortUnique(data, size, lt);
+    v.~vec<T>();
+    new (&v) vec<T>(data, size); }
+template <class T> void sortUnique(vec<T>& v) {
+    sortUnique(v, LessThan_default<T>()); }
+
+
+//=================================================================================================
+};
+#endif
diff --git a/stp/sat/VarOrder.h b/stp/sat/VarOrder.h
new file mode 100644
index 00000000..6ad1bfb1
--- /dev/null
+++ b/stp/sat/VarOrder.h
@@ -0,0 +1,146 @@
+/**************************************************************************************[VarOrder.h]
+MiniSat -- Copyright (c) 2003-2005, 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 VarOrder_h
+#define VarOrder_h
+
+#include "SolverTypes.h"
+#include "Solver.h"
+#include "Heap.h"
+#include "../AST/ASTUtil.h"
+
+namespace MINISAT {
+  //=================================================================================================
+
+  struct VarOrder_lt {
+    const vec<double>&  activity;
+    bool operator () (Var x, Var y) { return activity[x] > activity[y]; }
+    VarOrder_lt(const vec<double>&  act) : activity(act) { }
+  };
+  
+
+  enum { p_decisionvar = 0, p_polarity = 1, p_frozen = 2, p_dontcare = 3 };
+  
+  
+  class VarOrder {
+    const vec<char>&    assigns;     // var->val. Pointer to external assignment table.
+    const vec<double>&  activity;    // var->act. Pointer to external activity table.
+    vec<char>           properties;
+    //Heap<VarOrder_lt>   heap;
+    //double              random_seed; // For the internal random number generator
+    
+    friend class VarFilter;
+  public:
+    //FIXME: Vijay: delete after experiments
+    Heap<VarOrder_lt>   heap;
+    double              random_seed; // For the internal random number generator
+    //FIXME ENDS HERE
+
+    VarOrder(const vec<char>& ass, const vec<double>& act) :
+      assigns(ass), activity(act), heap(VarOrder_lt(act)), random_seed(2007)
+      //assigns(ass), activity(act), heap(VarOrder_lt(act))
+    { }
+    
+    int  size       ()                         { return heap.size(); }
+    void setVarProp (Var v, uint prop, bool b) { properties[v] = (properties[v] & ~(1 << prop)) | (b << prop); }
+    bool hasVarProp (Var v, uint prop) const   { return properties[v] & (1 << prop); }
+    inline void cleanup    ();
+    
+    inline void newVar(bool polarity, bool dvar);
+    inline void update(Var x);                  // Called when variable increased in activity.
+    inline void undo(Var x);                    // Called when variable is unassigned and may be selected again.
+    //Selects a new, unassigned variable (or 'var_Undef' if none exists).
+    inline Lit  select(double random_freq =.0, int decision_level = 0); 
+  };
+  
+  
+  struct VarFilter {
+    const VarOrder& o;
+    VarFilter(const VarOrder& _o) : o(_o) {}
+    bool operator()(Var v) const { return toLbool(o.assigns[v]) == l_Undef  && o.hasVarProp(v, p_decisionvar); }
+    //bool operator()(Var v) const { return toLbool(o.assigns[v]) == l_Undef; }
+  };
+  
+  void VarOrder::cleanup()
+  {
+    VarFilter f(*this);
+    heap.filter(f);
+  }
+  
+  void VarOrder::newVar(bool polarity, bool dvar)
+  {
+    Var v = assigns.size()-1;
+    heap.setBounds(v+1);
+    properties.push(0);
+    setVarProp(v, p_decisionvar, dvar);
+    setVarProp(v, p_polarity, polarity);
+    undo(v);
+  }
+  
+  
+  void VarOrder::update(Var x)
+  {
+    if (heap.inHeap(x))
+      heap.increase(x);
+  }
+  
+  
+  void VarOrder::undo(Var x)
+  {
+    if (!heap.inHeap(x) && hasVarProp(x, p_decisionvar))
+      heap.insert(x);
+  }
+  
+  
+  Lit VarOrder::select(double random_var_freq, int decision_level)
+  {
+    Var next = var_Undef;
+    
+    if (drand(random_seed) < random_var_freq && !heap.empty())
+      next = irand(random_seed,assigns.size());
+
+    // Activity based decision:
+    while (next == var_Undef || toLbool(assigns[next]) != l_Undef || !hasVarProp(next, p_decisionvar))
+      if (heap.empty()){
+	next = var_Undef;
+	break;
+      }else
+	next = heap.getmin();
+    
+    //printing
+    if(BEEV::print_sat_varorder) {
+      if (next != var_Undef) {
+	BEEV::Convert_MINISATVar_To_ASTNode_Print(next,
+						  decision_level,
+						  hasVarProp(next, p_polarity));
+	// fprintf(stderr,"var = %d, prop = %d, decision = %d, polarity = %d, frozen = %d\n", 
+	// 		next+1, properties[next], hasVarProp(next, p_decisionvar), 
+	// 		hasVarProp(next, p_polarity), hasVarProp(next, p_frozen));
+      }
+      else
+	fprintf(stderr, "var = undef\n");
+    }
+    
+    return next == var_Undef ? lit_Undef : Lit(next, hasVarProp(next, p_polarity));
+  }
+  
+  
+  //=================================================================================================
+};
+#endif