Reorganizing the code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/sat/luby.cpp

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    luby.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-03-04.
+
+Revision History:
+
+--*/
+#include<cmath>
+
+unsigned get_luby(unsigned i) {
+    if (i == 1) 
+        return 1;
+    double k = log(static_cast<double>(i+1))/log(static_cast<double>(2));
+    
+    if (k == floor(k + 0.5))
+        return static_cast<unsigned>(pow(2,k-1));
+    else {
+        k = static_cast<unsigned>(floor(k));
+        return get_luby(i - static_cast<unsigned>(pow(2, k)) + 1);
+    }
+}
+

src/sat/luby.h

@@ -0,0 +1,31 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    luby.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-03-04.
+
+Revision History:
+
+--*/
+#ifndef _LUBY_H_
+#define _LUBY_H_
+
+/**
+   \brief Return the i-th element of the Luby sequence: 1,1,2,1,1,2,4,1,1,2,1,1,2,4,8,...
+
+   get_luby(i) = 2^{i-1}                     if  i = 2^k -1
+   get_luby(i) = get_luby(i - 2^{k-1} + 1)   if  2^{k-1} <= i < 2^k - 1
+*/
+unsigned get_luby(unsigned i);
+
+#endif /* _LUBY_H_ */
+

src/sat/sat_asymm_branch.cpp

@@ -0,0 +1,218 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_asymm_branch.cpp
+
+Abstract:
+
+    SAT solver asymmetric branching
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-30.
+
+Revision History:
+
+--*/
+#include"sat_asymm_branch.h"
+#include"sat_solver.h"
+#include"stopwatch.h"
+#include"trace.h"
+
+namespace sat {
+
+    asymm_branch::asymm_branch(solver & _s, params_ref const & p):
+        s(_s),
+        m_counter(0) {
+        updt_params(p);
+        reset_statistics();
+    }
+
+    struct clause_size_lt {
+        bool operator()(clause * c1, clause * c2) const { return c1->size() > c2->size(); }
+    };
+
+    struct asymm_branch::report {
+        asymm_branch & m_asymm_branch;
+        stopwatch      m_watch;
+        unsigned       m_elim_literals;
+        report(asymm_branch & a):
+            m_asymm_branch(a),
+            m_elim_literals(a.m_elim_literals) {
+            m_watch.start();
+        }
+        
+        ~report() {
+            m_watch.stop();
+            IF_VERBOSE(SAT_VB_LVL, 
+                       verbose_stream() << " (sat-asymm-branch :elim-literals "
+                       << (m_asymm_branch.m_elim_literals - m_elim_literals)
+                       << " :cost " << m_asymm_branch.m_counter
+                       << mem_stat()
+                       << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
+        }
+    };
+    
+    void asymm_branch::operator()(bool force) {
+        if (!m_asymm_branch)
+            return;
+        s.propagate(false); // must propagate, since it uses s.push()
+        if (s.m_inconsistent)
+            return;
+        if (!force && m_counter > 0)
+            return;
+        CASSERT("asymm_branch", s.check_invariant());
+        TRACE("asymm_branch_detail", s.display(tout););
+        report rpt(*this);
+        svector<char> saved_phase(s.m_phase);
+        m_counter  = 0; // counter is moving down to capture propagate cost.
+        int limit  = -static_cast<int>(m_asymm_branch_limit);
+        std::stable_sort(s.m_clauses.begin(), s.m_clauses.end(), clause_size_lt());
+        m_counter -= s.m_clauses.size();
+        clause_vector::iterator it  = s.m_clauses.begin();
+        clause_vector::iterator it2 = it;
+        clause_vector::iterator end = s.m_clauses.end();
+        try {
+            for (; it != end; ++it) {
+                SASSERT(s.m_qhead == s.m_trail.size());
+                if (m_counter < limit || s.inconsistent()) {
+                    *it2 = *it;
+                    ++it2;
+                    continue;
+                }
+                s.checkpoint();
+                clause & c = *(*it);
+                m_counter -= c.size();
+                if (!process(c))
+                    continue; // clause was removed
+                *it2 = *it;
+                // throw exception to test bug fix: if (it2 != it) throw solver_exception("trigger bug");
+                ++it2;
+            }
+            s.m_clauses.set_end(it2);
+        }
+        catch (solver_exception & ex) {
+            // put m_clauses in a consistent state...
+            for (; it != end; ++it, ++it2) {
+                *it2 = *it;
+            }
+            s.m_clauses.set_end(it2);
+            m_counter = -m_counter;
+            throw ex;
+        }
+        m_counter = -m_counter;
+        s.m_phase = saved_phase;
+        CASSERT("asymm_branch", s.check_invariant());
+    }
+
+    bool asymm_branch::process(clause & c) {
+        TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";);
+        SASSERT(s.scope_lvl() == 0);
+#ifdef Z3DEBUG
+        unsigned trail_sz = s.m_trail.size();
+#endif
+        SASSERT(!s.inconsistent());
+        unsigned sz = c.size();
+        SASSERT(sz > 0);
+        unsigned i;
+        // check if the clause is already satisfied
+        for (i = 0; i < sz; i++) {
+            if (s.value(c[i]) == l_true) {
+                s.dettach_clause(c);
+                s.del_clause(c);
+                return false;
+            }
+        }
+        // try asymmetric branching
+        // clause must not be used for propagation
+        s.dettach_clause(c);
+        s.push();
+        for (i = 0; i < sz - 1; i++) {
+            literal l = c[i];
+            SASSERT(!s.inconsistent());
+            TRACE("asymm_branch_detail", tout << "assigning: " << ~l << "\n";);
+            s.assign(~l, justification());
+            s.propagate_core(false); // must not use propagate(), since check_missed_propagation may fail for c
+            if (s.inconsistent())
+                break;
+        }
+        s.pop(1);
+        SASSERT(!s.inconsistent());
+        SASSERT(s.scope_lvl() == 0);
+        SASSERT(trail_sz == s.m_trail.size());
+        if (i == sz - 1) {
+            // clause size can't be reduced.
+            s.attach_clause(c);
+            return true;
+        }
+        // clause can be reduced 
+        unsigned new_sz = i+1;
+        SASSERT(new_sz >= 1);
+        SASSERT(new_sz < sz);
+        TRACE("asymm_branch", tout << c << "\nnew_size: " << new_sz << "\n";
+              for (unsigned i = 0; i < c.size(); i++) tout << static_cast<int>(s.value(c[i])) << " "; tout << "\n";);
+        // cleanup reduced clause
+        unsigned j = 0;
+        for (i = 0; i < new_sz; i++) {
+            literal l = c[i];
+            switch (s.value(l)) {
+            case l_undef:
+                c[j] = l;
+                j++;
+                break;
+            case l_false:
+                break;
+            case l_true:
+                UNREACHABLE();
+                break;
+            }
+        }
+        new_sz = j;
+        m_elim_literals += sz - new_sz;
+        switch(new_sz) {
+        case 0:
+            s.set_conflict(justification());
+            return false;
+        case 1:
+            TRACE("asymm_branch", tout << "produced unit clause: " << c[0] << "\n";);
+            s.assign(c[0], justification());
+            s.del_clause(c);
+            s.propagate_core(false); 
+            return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.
+        case 2:
+            SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
+            s.mk_bin_clause(c[0], c[1], false);
+            s.del_clause(c);
+            return false;
+        default:
+            c.shrink(new_sz);
+            s.attach_clause(c);
+            return true;
+        }
+    }
+    
+    void asymm_branch::updt_params(params_ref const & p) {
+        m_asymm_branch        = p.get_bool(":asymm-branch", true);
+        m_asymm_branch_rounds = p.get_uint(":asymm-branch-rounds", 32);
+        m_asymm_branch_limit  = p.get_uint(":asymm-branch-limit", 100000000);
+        if (m_asymm_branch_limit > INT_MAX)
+            m_asymm_branch_limit = INT_MAX;
+    }
+
+    void asymm_branch::collect_param_descrs(param_descrs & d) {
+        d.insert(":asymm-branch", CPK_BOOL, "(default: true) asymmetric branching.");
+        d.insert(":asymm-branch-rounds", CPK_UINT, "(default: 32) maximum number of rounds of asymmetric branching.");
+        d.insert(":asymm-branch-limit", CPK_UINT, "approx. maximum number of literals visited during asymmetric branching.");
+    }
+    
+    void asymm_branch::collect_statistics(statistics & st) {
+        st.update("elim literals", m_elim_literals);
+    }
+
+    void asymm_branch::reset_statistics() {
+        m_elim_literals = 0;
+    }
+
+};

src/sat/sat_asymm_branch.h

@@ -0,0 +1,60 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_asymm_branch.h
+
+Abstract:
+
+    SAT solver asymmetric branching
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-30.
+
+Revision History:
+
+--*/
+#ifndef _SAT_ASYMM_BRANCH_H_
+#define _SAT_ASYMM_BRANCH_H_
+
+#include"sat_types.h"
+#include"statistics.h"
+#include"params.h"
+
+namespace sat {
+    class solver;
+
+    class asymm_branch {
+        struct report;
+        
+        solver & s;
+        int      m_counter;
+
+        // config
+        bool                   m_asymm_branch;
+        unsigned               m_asymm_branch_rounds;
+        unsigned               m_asymm_branch_limit;
+
+        // stats
+        unsigned m_elim_literals;
+
+        bool process(clause & c);
+    public:
+        asymm_branch(solver & s, params_ref const & p);
+
+        void operator()(bool force = false);
+
+        void updt_params(params_ref const & p);
+        static void collect_param_descrs(param_descrs & d);
+
+        void collect_statistics(statistics & st);
+        void reset_statistics();
+
+        void dec(unsigned c) { m_counter -= c; }
+    };
+
+};
+
+#endif

src/sat/sat_clause.cpp

@@ -0,0 +1,236 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_clause.cpp
+
+Abstract:
+
+    Clauses
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+Revision History:
+
+--*/
+#include"memory.h"
+#include"sat_clause.h"
+#include"z3_exception.h"
+
+namespace sat {
+
+    clause::clause(unsigned id, unsigned sz, literal const * lits, bool learned):
+        m_id(id),
+        m_size(sz),
+        m_capacity(sz),
+        m_removed(false),
+        m_learned(learned),
+        m_used(false),
+        m_frozen(false),
+        m_reinit_stack(false),
+        m_inact_rounds(0) {
+        memcpy(m_lits, lits, sizeof(literal) * sz);
+        mark_strengthened();
+        SASSERT(check_approx());
+    }
+
+    var_approx_set clause::approx(unsigned num, literal const * lits) {
+        var_approx_set r;
+        for (unsigned i = 0; i < num; i++) 
+            r.insert(lits[i].var());
+        return r;
+    }
+    
+    void clause::update_approx() {
+        m_approx = approx(m_size, m_lits);
+    }
+
+    bool clause::check_approx() const {
+        var_approx_set curr = m_approx;
+        const_cast<clause*>(this)->update_approx();
+        SASSERT(may_eq(curr, m_approx));
+        return true;
+    }
+
+    bool clause::contains(literal l) const {
+        for (unsigned i = 0; i < m_size; i++)
+            if (m_lits[i] == l)
+                return true;
+        return false;
+    }
+
+    bool clause::contains(bool_var v) const {
+        for (unsigned i = 0; i < m_size; i++)
+            if (m_lits[i].var() == v)
+                return true;
+        return false;
+    }
+
+    void clause::elim(literal l) {
+        unsigned i;
+        for (i = 0; i < m_size; i++)
+            if (m_lits[i] == l)
+                break;
+        SASSERT(i < m_size);
+        i++;
+        for (; i < m_size; i++)
+            m_lits[i-1] = m_lits[i];
+        m_size--;
+        mark_strengthened();
+    }
+
+    bool clause::satisfied_by(model const & m) const {
+        for (unsigned i = 0; i < m_size; i++) {
+            literal  l = m_lits[i];
+            if (l.sign()) {
+                if (m[l.var()] == l_false)
+                    return true;
+            }
+            else {
+                if (m[l.var()] == l_true)
+                    return true;
+            }
+        }
+        return false;
+    }
+
+    void tmp_clause::set(unsigned num_lits, literal const * lits, bool learned) {
+        if (m_clause && m_clause->m_capacity < num_lits) {
+            dealloc_svect(m_clause);
+            m_clause = 0;
+        }
+        if (!m_clause) {
+            void * mem = alloc_svect(char, clause::get_obj_size(num_lits));
+            m_clause   = new (mem) clause(UINT_MAX, num_lits, lits, learned);
+        }
+        else {
+            SASSERT(m_clause->m_id == UINT_MAX);
+            m_clause->m_size = num_lits;
+            m_clause->m_learned = learned;
+            memcpy(m_clause->m_lits, lits, sizeof(literal) * num_lits);
+        }
+        SASSERT(m_clause->m_size <= m_clause->m_capacity);
+        for (unsigned i = 0; i < num_lits; i++) {
+            SASSERT((*m_clause)[i] == lits[i]);
+        }
+    }
+
+    clause_allocator::clause_allocator():
+        m_allocator("clause-allocator") {
+#ifdef _AMD64_
+        m_num_segments = 0;
+#endif
+    }
+
+    clause * clause_allocator::get_clause(clause_offset cls_off) const {
+#ifdef _AMD64_
+        return reinterpret_cast<clause *>(m_segments[cls_off & c_aligment_mask] + (static_cast<size_t>(cls_off) & ~c_aligment_mask));
+#else
+        return reinterpret_cast<clause *>(cls_off);
+#endif
+    }
+
+#ifdef _AMD64_
+    unsigned clause_allocator::get_segment(size_t ptr) {
+        SASSERT((ptr & c_aligment_mask) == 0);
+        ptr &= ~0xFFFFFFFFull; // Keep only high part
+        unsigned i = 0;
+        for (i = 0; i < m_num_segments; ++i)
+            if (m_segments[i] == ptr)
+                return i;
+        i = m_num_segments;
+        m_num_segments++;
+        if (i > c_max_segments)
+            throw default_exception("segment out of range");
+        m_segments[i] = ptr;
+        return i;
+    }
+#endif
+
+    clause_offset clause_allocator::get_offset(clause const * ptr) const {
+#ifdef _AMD64_
+        return static_cast<unsigned>(reinterpret_cast<size_t>(ptr)) + const_cast<clause_allocator*>(this)->get_segment(reinterpret_cast<size_t>(ptr));
+#else
+        return reinterpret_cast<size_t>(ptr);
+#endif
+    }
+    
+    clause * clause_allocator::mk_clause(unsigned num_lits, literal const * lits, bool learned) {
+        size_t size = clause::get_obj_size(num_lits);
+#ifdef _AMD64_
+        size_t slot = size >> c_cls_alignment;
+        if ((size & c_aligment_mask) != 0)
+            slot++;
+        size = slot << c_cls_alignment;
+#endif
+        void * mem = m_allocator.allocate(size);
+        clause * cls = new (mem) clause(m_id_gen.mk(), num_lits, lits, learned);
+        SASSERT(!learned || cls->is_learned());
+        return cls;
+    }
+
+    void clause_allocator::del_clause(clause * cls) {
+        m_id_gen.recycle(cls->id());
+        size_t size = clause::get_obj_size(cls->m_capacity);
+#ifdef _AMD64_
+        size_t slot = size >> c_cls_alignment;
+        if ((size & c_aligment_mask) != 0)
+            slot++;
+        size = slot << c_cls_alignment;
+#endif
+        cls->~clause();
+        m_allocator.deallocate(size, cls);
+    }
+
+    std::ostream & operator<<(std::ostream & out, clause const & c) {
+        out << "(";
+        for (unsigned i = 0; i < c.size(); i++) {
+            if (i > 0) out << " ";
+            out << c[i];
+        }
+        out << ")";
+        if (c.was_removed()) out << "x";
+        if (c.strengthened()) out << "+";
+        if (c.is_learned()) out << "*";
+        return out;
+    }
+
+    std::ostream & operator<<(std::ostream & out, clause_vector const & cs) {
+        clause_vector::const_iterator it  = cs.begin();
+        clause_vector::const_iterator end = cs.end();
+        for (; it != end; ++it) {
+            out << *(*it) << "\n";
+        }
+        return out;
+    }
+    
+    bool clause_wrapper::contains(literal l) const { 
+        unsigned sz = size();
+        for (unsigned i = 0; i < sz; i++)
+            if (operator[](i) == l)
+                return true;
+        return false;
+    }
+    
+    bool clause_wrapper::contains(bool_var v) const { 
+        unsigned sz = size();
+        for (unsigned i = 0; i < sz; i++)
+            if (operator[](i).var() == v)
+                return true;
+        return false;
+    }
+
+    std::ostream & operator<<(std::ostream & out, clause_wrapper const & c) {
+        out << "(";
+        for (unsigned i = 0; i < c.size(); i++) {
+            if (i > 0) out << " ";
+            out << c[i];
+        }
+        out << ")";
+        return out;
+    }
+
+};

src/sat/sat_clause.h

@@ -0,0 +1,179 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_clause.h
+
+Abstract:
+
+    Clauses
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+Revision History:
+
+--*/
+#ifndef _SAT_CLAUSE_H_
+#define _SAT_CLAUSE_H_
+
+#include"sat_types.h"
+#include"small_object_allocator.h"
+#include"id_gen.h"
+
+#ifdef _MSC_VER
+#pragma warning(disable : 4200)
+#pragma warning(disable : 4355)
+#endif
+
+namespace sat {
+
+    class clause_allocator;
+
+    class clause {
+        friend class clause_allocator;
+        friend class tmp_clause;
+        unsigned           m_id;
+        unsigned           m_size;
+        unsigned           m_capacity;
+        var_approx_set     m_approx;
+        unsigned           m_strengthened:1;
+        unsigned           m_removed:1;
+        unsigned           m_learned:1;
+        unsigned           m_used:1;
+        unsigned           m_frozen:1;
+        unsigned           m_reinit_stack:1;
+        unsigned           m_inact_rounds:8;
+        unsigned           m_glue:8; 
+        unsigned           m_psm:8;  // transient field used during gc
+        literal            m_lits[0];
+
+        static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); }
+        size_t get_size() const { return get_obj_size(m_capacity); }
+        clause(unsigned id, unsigned sz, literal const * lits, bool learned);
+    public:
+        unsigned id() const { return m_id; }
+        unsigned size() const { return m_size; }
+        literal & operator[](unsigned idx) { SASSERT(idx < m_size); return m_lits[idx]; }
+        literal const & operator[](unsigned idx) const { SASSERT(idx < m_size); return m_lits[idx]; }
+        bool is_learned() const { return m_learned; }
+        void unset_learned() { SASSERT(is_learned()); m_learned = false; }
+        void shrink(unsigned num_lits) { SASSERT(num_lits <= m_size); if (num_lits < m_size) { m_size = num_lits; mark_strengthened(); } }
+        bool strengthened() const { return m_strengthened; }
+        void mark_strengthened() { m_strengthened = true; update_approx(); }
+        void unmark_strengthened() { m_strengthened = false; }
+        void elim(literal l);
+        bool was_removed() const { return m_removed; }
+        void set_removed(bool f) { m_removed = f; }
+        var_approx_set approx() const { return m_approx; }
+        void update_approx();
+        bool check_approx() const; // for debugging
+        literal * begin() { return m_lits; }
+        literal * end() { return m_lits + m_size; }
+        bool contains(literal l) const;
+        bool contains(bool_var v) const;
+        bool satisfied_by(model const & m) const;
+        void mark_used() { m_used = true; }
+        void unmark_used() { m_used = false; }
+        bool was_used() const { return m_used; }
+        void inc_inact_rounds() { m_inact_rounds++; }
+        void reset_inact_rounds() { m_inact_rounds = 0; }
+        unsigned inact_rounds() const { return m_inact_rounds; }
+        bool frozen() const { return m_frozen; }
+        void freeze() { SASSERT(is_learned()); SASSERT(!frozen()); m_frozen = true; }
+        void unfreeze() { SASSERT(is_learned()); SASSERT(frozen()); m_frozen = false; }
+        static var_approx_set approx(unsigned num, literal const * lits);
+        void set_glue(unsigned glue) { m_glue = glue > 255 ? 255 : glue; }
+        unsigned glue() const { return m_glue; }
+        void set_psm(unsigned psm) { m_psm = psm > 255 ? 255 : psm; }
+        unsigned psm() const { return m_psm; }
+
+        bool on_reinit_stack() const { return m_reinit_stack; }
+        void set_reinit_stack(bool f) { m_reinit_stack = f; }
+    };
+
+    std::ostream & operator<<(std::ostream & out, clause const & c);
+    std::ostream & operator<<(std::ostream & out, clause_vector const & cs);
+
+    class bin_clause {
+        unsigned m_val1;
+        unsigned m_val2;
+    public:
+        bin_clause(literal l1, literal l2, bool learned):m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast<unsigned>(learned)) {}
+        literal get_literal1() const { return to_literal(m_val1); }
+        literal get_literal2() const { return to_literal(m_val2 >> 1); }
+        bool is_learned() const { return (m_val2 & 1) == 1; }
+    };
+
+    class tmp_clause {
+        clause * m_clause;
+    public:
+        tmp_clause():m_clause(0) {}
+        ~tmp_clause() { if (m_clause) dealloc_svect(m_clause); }
+        clause * get() const { return m_clause; }
+        void set(unsigned num_lits, literal const * lits, bool learned);
+        void set(literal l1, literal l2, bool learned) { literal ls[2] = { l1, l2 }; set(2, ls, learned); }
+        void set(bin_clause const & c) { set(c.get_literal1(), c.get_literal2(), c.is_learned()); }
+    };
+
+    /**
+       \brief Simple clause allocator that allows uint (32bit integers) to be used to reference clauses (even in 64bit machines).
+    */
+    class clause_allocator {
+        small_object_allocator m_allocator;
+        id_gen                 m_id_gen;
+#ifdef _AMD64_
+        unsigned get_segment(size_t ptr);
+        static const unsigned  c_cls_alignment = 3; 
+        static const unsigned  c_max_segments  = 1 << c_cls_alignment;
+        static const size_t    c_aligment_mask = (1ull << c_cls_alignment) - 1ull;
+        unsigned               m_num_segments;
+        size_t                 m_segments[c_max_segments];
+#endif
+    public:
+        clause_allocator();
+        clause *      get_clause(clause_offset cls_off) const;
+        clause_offset get_offset(clause const * ptr) const;
+        clause *      mk_clause(unsigned num_lits, literal const * lits, bool learned);
+        void          del_clause(clause * cls);
+    };
+
+    /**
+       \brief Wrapper for clauses & binary clauses.
+       I do not create clause objects for binary clauses.
+       clause_ref wraps a clause object or a pair of literals (i.e., a binary clause). 
+    */
+    class clause_wrapper {
+        union {
+            clause * m_cls;
+            unsigned m_l1_idx;
+        };
+        unsigned m_l2_idx;
+    public:
+        clause_wrapper(literal l1, literal l2):m_l1_idx(l1.to_uint()), m_l2_idx(l2.to_uint()) {}
+        clause_wrapper(clause & c):m_cls(&c), m_l2_idx(null_literal.to_uint()) {}
+
+        bool is_binary() const { return m_l2_idx != null_literal.to_uint(); }
+        unsigned size() const { return is_binary() ? 2 : m_cls->size(); }
+        literal operator[](unsigned idx) const { 
+            SASSERT(idx < size());
+            if (is_binary())
+                return idx == 0 ? to_literal(m_l1_idx) : to_literal(m_l2_idx);
+            else
+                return m_cls->operator[](idx);
+        }
+
+        bool contains(literal l) const;
+        bool contains(bool_var v) const;
+        clause * get_clause() const { SASSERT(!is_binary()); return m_cls; }
+    };
+
+    typedef svector<clause_wrapper> clause_wrapper_vector;
+
+    std::ostream & operator<<(std::ostream & out, clause_wrapper const & c);
+
+};
+
+#endif

src/sat/sat_clause_set.cpp

@@ -0,0 +1,84 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_clause_set.cpp
+
+Abstract:
+
+    Set of clauses
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-25.
+
+Revision History:
+
+--*/
+#include"sat_clause_set.h"
+
+namespace sat {
+
+    void clause_set::insert(clause & c) {
+        unsigned id  = c.id();
+        m_id2pos.reserve(id+1, UINT_MAX);
+        if (m_id2pos[id] != UINT_MAX)
+            return; // already in the set
+        unsigned pos = m_set.size();
+        m_id2pos[id] = pos;
+        m_set.push_back(&c);
+        CASSERT("clause_set", check_invariant());
+    }
+
+    void clause_set::erase(clause & c) { 
+        unsigned id = c.id();
+        if (id >= m_id2pos.size())
+            return;
+        unsigned pos = m_id2pos[id];
+        if (pos == UINT_MAX)
+            return;
+        m_id2pos[id] = UINT_MAX;
+        unsigned last_pos = m_set.size() - 1;
+        if (pos != last_pos) {
+            clause * last_c = m_set[last_pos];
+            m_set[pos] = last_c; 
+            m_id2pos[last_c->id()] = pos;
+        }
+        m_set.pop_back();
+        CASSERT("clause_set", check_invariant());
+    }
+
+    clause & clause_set::erase() {
+        SASSERT(!empty());
+        clause & c = *m_set.back(); 
+        m_id2pos[c.id()] = UINT_MAX;
+        m_set.pop_back();
+        return c;
+    }
+
+    bool clause_set::check_invariant() const {
+        {
+            clause_vector::const_iterator it  = m_set.begin();
+            clause_vector::const_iterator end = m_set.end();
+            for (unsigned pos = 0; it != end; ++it, ++pos) {
+                clause & c = *(*it);
+                SASSERT(c.id() < m_id2pos.size());
+                SASSERT(m_id2pos[c.id()] == pos);
+            }
+        }
+        {
+            unsigned_vector::const_iterator it  = m_id2pos.begin();
+            unsigned_vector::const_iterator end = m_id2pos.end();
+            for (unsigned id = 0; it != end; ++it, ++id) {
+                unsigned pos = *it;
+                if (pos == UINT_MAX)
+                    continue;
+                SASSERT(pos < m_set.size());
+                SASSERT(m_set[pos]->id() == id);
+            }
+        }
+        return true;
+    }
+
+};

src/sat/sat_clause_set.h

@@ -0,0 +1,56 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_clause_set.h
+
+Abstract:
+
+    Set of clauses
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-25.
+
+Revision History:
+
+--*/
+#ifndef _SAT_CLAUSE_SET_H_
+#define _SAT_CLAUSE_SET_H_
+
+#include"sat_clause.h"
+
+namespace sat {
+
+    class clause_set {
+        unsigned_vector m_id2pos; 
+        clause_vector   m_set;
+    public:
+        typedef clause_vector::const_iterator iterator;
+
+        bool contains(clause const & cls) const { 
+            if (cls.id() >= m_id2pos.size()) 
+                return false; 
+            return m_id2pos[cls.id()] != UINT_MAX; 
+        }
+        bool empty() const { return m_set.empty(); }
+        unsigned size() const { return m_set.size(); }
+        void insert(clause & c);
+        void erase(clause & c);
+
+        // erase some clause from the set
+        clause & erase();
+
+        void reset() { m_id2pos.reset(); m_set.reset(); }
+        void finalize() { m_id2pos.finalize(); m_set.finalize(); }
+
+        iterator begin() const { return m_set.begin(); }
+        iterator end() const { return m_set.end(); }
+
+        bool check_invariant() const;
+    };
+    
+};
+
+#endif

src/sat/sat_clause_use_list.cpp

@@ -0,0 +1,57 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_clause_use_list.cpp
+
+Abstract:
+
+    Clause use list
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-31.
+
+Revision History:
+
+--*/
+#include"sat_clause.h"
+#include"sat_clause_use_list.h"
+
+namespace sat {
+
+    bool clause_use_list::check_invariant() const {
+#ifdef LAZY_USE_LIST
+        unsigned sz = 0;
+        for (unsigned i = 0; i < m_clauses.size(); i++) 
+            if (!m_clauses[i]->was_removed())
+                sz++;
+        SASSERT(sz == m_size);
+#endif
+        return true;
+    }
+
+#ifdef LAZY_USE_LIST
+    void clause_use_list::iterator::consume() {
+        while (true) {
+            if (m_i == m_size)
+                return;
+            if (!m_clauses[m_i]->was_removed()) {
+                m_clauses[m_j] = m_clauses[m_i];
+                return;
+            }
+            m_i++;
+        }
+    }
+#endif
+
+    clause_use_list::iterator::~iterator() {
+#ifdef LAZY_USE_LIST
+        while (m_i < m_size)
+            next();
+        m_clauses.shrink(m_j);
+#endif
+    }
+
+};

src/sat/sat_clause_use_list.h

@@ -0,0 +1,118 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_clause_use_list.h
+
+Abstract:
+
+    Clause use list
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-31.
+
+Revision History:
+
+--*/
+#ifndef _SAT_CLAUSE_USE_LIST_H_
+#define _SAT_CLAUSE_USE_LIST_H_
+
+#include"sat_types.h"
+
+namespace sat {
+
+#define LAZY_USE_LIST
+
+    /**
+       \brief Clause use list with delayed deletion.
+    */
+    class clause_use_list {
+        clause_vector   m_clauses;
+#ifdef LAZY_USE_LIST
+        unsigned        m_size;
+#endif
+    public:
+        clause_use_list() {
+#ifdef LAZY_USE_LIST
+            m_size = 0; 
+#endif
+        }
+        
+        unsigned size() const { 
+#ifdef LAZY_USE_LIST
+            return m_size; 
+#else
+            return m_clauses.size();
+#endif
+        }
+
+        bool empty() const { return size() == 0; }
+        
+        void insert(clause & c) { 
+            SASSERT(!m_clauses.contains(&c)); SASSERT(!c.was_removed()); 
+            m_clauses.push_back(&c); 
+#ifdef LAZY_USE_LIST
+            m_size++; 
+#endif
+        }
+        void erase_not_removed(clause & c) { 
+#ifdef LAZY_USE_LIST
+            SASSERT(m_clauses.contains(&c)); SASSERT(!c.was_removed()); m_clauses.erase(&c); m_size--; 
+#else
+            m_clauses.erase(&c);
+#endif
+        }
+        void erase(clause & c) { 
+#ifdef LAZY_USE_LIST
+            SASSERT(m_clauses.contains(&c)); SASSERT(c.was_removed()); m_size--; 
+#else
+            m_clauses.erase(&c);
+#endif
+        }
+        
+        void reset() { 
+            m_clauses.finalize(); 
+#ifdef LAZY_USE_LIST
+            m_size = 0; 
+#endif
+        }
+        
+        bool check_invariant() const;
+        // iterate & compress
+        class iterator {
+            clause_vector & m_clauses;
+            unsigned        m_size;
+            unsigned        m_i;
+#ifdef LAZY_USE_LIST
+            unsigned        m_j;
+            void consume();
+#endif
+        public:
+            iterator(clause_vector & v):m_clauses(v), m_size(v.size()), m_i(0) {
+#ifdef LAZY_USE_LIST
+                m_j = 0;
+                consume(); 
+#endif
+            }
+            ~iterator();
+            bool at_end() const { return m_i == m_size; }
+            clause & curr() const { SASSERT(!at_end()); return *(m_clauses[m_i]); }
+            void next() { 
+                SASSERT(!at_end()); 
+                SASSERT(!m_clauses[m_i]->was_removed()); 
+                m_i++; 
+#ifdef LAZY_USE_LIST
+                m_j++; 
+                consume(); 
+#endif
+            }
+        };
+        
+        iterator mk_iterator() const { return iterator(const_cast<clause_use_list*>(this)->m_clauses); }
+    };
+
+};
+
+#endif

src/sat/sat_cleaner.cpp

@@ -0,0 +1,214 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_cleaner.h
+
+Abstract:
+
+    Eliminate satisfied clauses, and literals assigned to false.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-24.
+
+Revision History:
+
+--*/
+#include"sat_cleaner.h"
+#include"sat_solver.h"
+#include"trace.h"
+#include"stopwatch.h"
+
+namespace sat {
+
+    cleaner::cleaner(solver & _s):
+        s(_s),
+        m_last_num_units(0), 
+        m_cleanup_counter(0) {
+        reset_statistics();
+    }
+    
+    /**
+       - Delete watch lists of assigned literals.
+       - Delete satisfied binary watched binary clauses
+       - Delete watched clauses (they will be reinserted after they are cleaned).
+    */
+    void cleaner::cleanup_watches() {
+        vector<watch_list>::iterator it  = s.m_watches.begin();
+        vector<watch_list>::iterator end = s.m_watches.end();
+        unsigned l_idx = 0;
+        for (; it != end; ++it, ++l_idx) {
+            if (s.value(to_literal(l_idx)) != l_undef) {
+                it->finalize();
+                SASSERT(it->empty());
+                continue;
+            }
+            TRACE("cleanup_bug", tout << "processing wlist of " << to_literal(l_idx) << "\n";);
+            watch_list & wlist = *it;
+            watch_list::iterator it2      = wlist.begin();
+            watch_list::iterator it_prev  = it2;
+            watch_list::iterator end2     = wlist.end();
+            for (; it2 != end2; ++it2) {
+                switch (it2->get_kind()) {
+                case watched::BINARY:
+                    SASSERT(s.value(it2->get_literal()) == l_true || s.value(it2->get_literal()) == l_undef);
+                    if (s.value(it2->get_literal()) == l_undef) {
+                        *it_prev = *it2;
+                        ++it_prev;
+                    }
+                    TRACE("cleanup_bug", tout << "keeping: " << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";);
+                    break;
+                case watched::TERNARY:
+                case watched::CLAUSE:
+                    // skip
+                    break;
+                case watched::EXT_CONSTRAINT:
+                    *it_prev = *it2;
+                    ++it_prev;
+                    break;
+                default:
+                    UNREACHABLE();
+                    break;
+                }
+            }
+            wlist.set_end(it_prev);
+        }
+    }
+
+    void cleaner::cleanup_clauses(clause_vector & cs) {
+        clause_vector::iterator it  = cs.begin();
+        clause_vector::iterator it2 = it;
+        clause_vector::iterator end = cs.end();
+        for (; it != end; ++it) {
+            clause & c = *(*it);
+            TRACE("sat_cleaner_bug", tout << "cleaning: " << c << "\n";
+                  for (unsigned i = 0; i < c.size(); i++) tout << c[i] << ": " << s.value(c[i]) << "\n";);
+            CTRACE("sat_cleaner_frozen", c.frozen(), tout << c << "\n";);
+            unsigned sz = c.size();
+            unsigned i = 0, j = 0;
+            bool sat = false;
+            m_cleanup_counter += sz;
+            for (; i < sz; i++) {
+                switch (s.value(c[i])) {
+                case l_true:
+                    sat = true;
+                    goto end_loop;
+                case l_false:
+                    m_elim_literals++;
+                    break;
+                case l_undef:
+                    c[j] = c[i];
+                    j++;
+                    break;
+                }
+            }
+        end_loop:
+            CTRACE("sat_cleaner_frozen", c.frozen(),
+                   tout << "sat: " << sat << ", new_size: " << j << "\n";
+                   tout << mk_lits_pp(j, c.begin()) << "\n";);
+            if (sat) {
+                m_elim_clauses++;
+                s.del_clause(c);
+            }
+            else {
+                unsigned new_sz = j;
+                CTRACE("sat_cleaner_bug", new_sz < 2, tout << "new_sz: " << new_sz << "\n";
+                       if (c.size() > 0) tout << "unit: " << c[0] << "\n";);
+                SASSERT(c.frozen() || new_sz >= 2);
+                if (new_sz == 0) {
+                    // It can only happen with frozen clauses.
+                    // active clauses would have signed the conflict.
+                    SASSERT(c.frozen());
+                    s.set_conflict(justification());
+                    s.del_clause(c);
+                }
+                else if (new_sz == 1) {
+                    // It can only happen with frozen clauses.
+                    // active clauses would have propagated the literal
+                    SASSERT(c.frozen());
+                    s.assign(c[0], justification());
+                    s.del_clause(c);
+                }
+                else {
+                    SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
+                    if (new_sz == 2) {
+                        TRACE("cleanup_bug", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
+                        s.mk_bin_clause(c[0], c[1], c.is_learned());
+                        s.del_clause(c);
+                    }
+                    else {
+                        c.shrink(new_sz);
+                        *it2 = *it;
+                        it2++;
+                        if (!c.frozen()) {
+                            if (new_sz == 3)
+                                s.attach_ter_clause(c);
+                            else
+                                s.attach_nary_clause(c);
+                        }
+                    }
+                }
+            }
+        }
+        cs.set_end(it2);
+    }
+
+    struct cleaner::report {
+        cleaner & m_cleaner;
+        stopwatch m_watch;
+        unsigned  m_elim_clauses;
+        unsigned  m_elim_literals;
+        report(cleaner & c):
+            m_cleaner(c),
+            m_elim_clauses(c.m_elim_clauses),
+            m_elim_literals(c.m_elim_literals) {
+            m_watch.start();
+        }
+        ~report() {
+            m_watch.stop();
+            IF_VERBOSE(SAT_VB_LVL, 
+                       verbose_stream() << " (sat-cleaner :elim-literals " << (m_cleaner.m_elim_literals - m_elim_literals)
+                       << " :elim-clauses " << (m_cleaner.m_elim_clauses - m_elim_clauses)
+                       << " :cost " << m_cleaner.m_cleanup_counter
+                       << mk_stat(m_cleaner.s)
+                       << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
+        }
+    };
+
+    /**
+       \brief Return true if cleaner executed.
+    */
+    bool cleaner::operator()(bool force) {
+        CASSERT("cleaner_bug", s.check_invariant());
+        unsigned trail_sz = s.m_trail.size();
+        s.propagate(false); // make sure that everything was propagated.
+        if (s.m_inconsistent)
+            return false;
+        if (m_last_num_units == trail_sz)
+            return false; // there are no new assigned literals since last time... nothing to be done
+        if (!force && m_cleanup_counter > 0)
+            return false; // prevent simplifier from being executed over and over again.
+        report rpt(*this);
+        m_last_num_units = trail_sz;
+        m_cleanup_counter = 0;
+        cleanup_watches();
+        cleanup_clauses(s.m_clauses);
+        cleanup_clauses(s.m_learned);
+        s.propagate(false);
+        CASSERT("cleaner_bug", s.check_invariant());
+        return true;
+    }
+    
+    void cleaner::reset_statistics() {
+        m_elim_clauses = 0;
+        m_elim_literals = 0;
+    }
+    
+    void cleaner::collect_statistics(statistics & st) {
+        st.update("elim clauses", m_elim_clauses);
+        st.update("elim literals", m_elim_literals);
+    }
+
+};

src/sat/sat_cleaner.h

@@ -0,0 +1,53 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_cleaner.h
+
+Abstract:
+
+    Eliminate satisfied clauses, and literals assigned to false.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-24.
+
+Revision History:
+
+--*/
+#ifndef _SAT_CLEANER_H_
+#define _SAT_CLEANER_H_
+
+#include"sat_types.h"
+#include"statistics.h"
+
+namespace sat {
+
+    class cleaner {
+        struct report;
+
+        solver & s;
+        unsigned m_last_num_units;
+        int      m_cleanup_counter;
+
+        // stats
+        unsigned m_elim_clauses;
+        unsigned m_elim_literals;
+
+        void cleanup_watches();
+        void cleanup_clauses(clause_vector & cs);
+    public:
+        cleaner(solver & s);
+
+        bool operator()(bool force = false);
+
+        void collect_statistics(statistics & st);
+        void reset_statistics();
+
+        void dec() { m_cleanup_counter--; }
+    };
+
+};
+
+#endif

src/sat/sat_config.cpp

@@ -0,0 +1,126 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_config.cpp
+
+Abstract:
+
+    SAT configuration options
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+Revision History:
+
+--*/
+#include"sat_config.h"
+#include"sat_types.h"
+
+namespace sat {
+
+    config::config(params_ref const & p):
+        m_always_true("always-true"),
+        m_always_false("always-false"),
+        m_caching("caching"),
+        m_random("random"),
+        m_geometric("geometric"),
+        m_luby("luby"),
+        m_dyn_psm("dyn-psm"),
+        m_psm("psm"),
+        m_glue("glue"),
+        m_glue_psm("glue-psm"),
+        m_psm_glue("psm-glue") {
+        updt_params(p); 
+    }
+
+    void config::updt_params(params_ref const & p) {
+        m_max_memory  = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
+
+        symbol s = p.get_sym(":restart", m_luby);
+        if (s == m_luby)
+            m_restart = RS_LUBY;
+        else if (s == m_geometric)
+            m_restart = RS_GEOMETRIC;
+        else
+            throw sat_param_exception("invalid restart strategy");
+
+        s = p.get_sym(":phase", m_caching);
+        if (s == m_always_false) 
+            m_phase = PS_ALWAYS_FALSE;
+        else if (s == m_always_true)
+            m_phase = PS_ALWAYS_TRUE;
+        else if (s == m_caching)
+            m_phase = PS_CACHING;
+        else if (s == m_random)
+            m_phase = PS_RANDOM;
+        else
+            throw sat_param_exception("invalid phase selection strategy");
+
+        m_phase_caching_on  = p.get_uint(":phase-caching-on", 400);
+        m_phase_caching_off = p.get_uint(":phase-caching-off", 100);
+
+        m_restart_initial = p.get_uint(":restart-initial", 100);
+        m_restart_factor  = p.get_double(":restart-factor", 1.5);
+        
+        m_random_freq     = p.get_double(":random-freq", 0.01);
+
+        m_burst_search    = p.get_uint(":burst-search", 100);
+        
+        m_max_conflicts   = p.get_uint(":max-conflicts", UINT_MAX);
+
+        m_simplify_mult1  = p.get_uint(":simplify-mult1", 300);
+        m_simplify_mult2  = p.get_double(":simplify-mult2", 1.5);
+        m_simplify_max    = p.get_uint(":simplify-max", 500000);
+
+        s = p.get_sym(":gc-strategy", m_glue_psm);
+        if (s == m_dyn_psm) {
+            m_gc_strategy     = GC_DYN_PSM;
+            m_gc_initial      = p.get_uint(":gc-initial", 500);
+            m_gc_increment    = p.get_uint(":gc-increment", 100);
+            m_gc_small_lbd    = p.get_uint(":gc-small-lbd", 3);
+            m_gc_k            = p.get_uint(":gc-k", 7);
+            if (m_gc_k > 255)
+                m_gc_k = 255;
+        }
+        else {
+            if (s == m_glue_psm)
+                m_gc_strategy = GC_GLUE_PSM;
+            else if (s == m_glue)
+                m_gc_strategy = GC_GLUE;
+            else if (s == m_psm)
+                m_gc_strategy = GC_PSM;
+            else if (s == m_psm_glue)
+                m_gc_strategy = GC_PSM_GLUE;
+            else 
+                throw sat_param_exception("invalid gc strategy");
+            m_gc_initial      = p.get_uint(":gc-initial", 20000);
+            m_gc_increment    = p.get_uint(":gc-increment", 500);
+        }
+        m_minimize_lemmas = p.get_bool(":minimize-lemmas", true);
+        m_dyn_sub_res     = p.get_bool(":dyn-sub-res", true);
+    }
+
+    void config::collect_param_descrs(param_descrs & r) {
+        insert_max_memory(r);
+        r.insert(":phase", CPK_SYMBOL, "(default: caching) phase selection strategy: always-false, always-true, caching, random.");
+        r.insert(":phase-caching-on", CPK_UINT, "(default: 400)");
+        r.insert(":phase-caching-off", CPK_UINT, "(default: 100)");
+        r.insert(":restart", CPK_SYMBOL, "(default: luby) restart strategy: luby or geometric.");
+        r.insert(":restart-initial", CPK_UINT, "(default: 100) initial restart (number of conflicts).");  
+        r.insert(":restart-factor", CPK_DOUBLE, "(default: 1.5) restart increment factor for geometric strategy.");
+        r.insert(":random-freq", CPK_DOUBLE, "(default: 0.01) frequency of random case splits.");                                                      
+        r.insert(":burst-search", CPK_UINT, "(default: 100) number of conflicts before first global simplification.");
+        r.insert(":max-conflicts", CPK_UINT, "(default: inf) maximum number of conflicts.");
+        r.insert(":gc-strategy", CPK_SYMBOL, "(default: glue-psm) garbage collection strategy: psm, glue, glue-psm, dyn-psm.");
+        r.insert(":gc-initial", CPK_UINT, "(default: 20000) learned clauses garbage collection frequence.");
+        r.insert(":gc-increment", CPK_UINT, "(default: 500) increment to the garbage collection threshold.");
+        r.insert(":gc-small-lbd", CPK_UINT, "(default: 3) learned clauses with small LBD are never deleted (only used in dyn-psm).");
+        r.insert(":gc-k", CPK_UINT, "(default: 7) learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn-psm).");
+        r.insert(":minimize-lemmas", CPK_BOOL, "(default: true) minimize learned clauses.");
+        r.insert(":dyn-sub-res", CPK_BOOL, "(default: true) dynamic subsumption resolution for minimizing learned clauses.");
+    }
+
+};

src/sat/sat_config.h

@@ -0,0 +1,91 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_config.h
+
+Abstract:
+
+    SAT main configuration options.
+    Sub-components have their own options.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+Revision History:
+
+--*/
+#ifndef _SAT_CONFIG_H_
+#define _SAT_CONFIG_H_
+
+#include"params.h"
+
+namespace sat {
+
+    enum phase_selection {
+        PS_ALWAYS_TRUE,
+        PS_ALWAYS_FALSE,
+        PS_CACHING,
+        PS_RANDOM
+    };
+
+    enum restart_strategy {
+        RS_GEOMETRIC,
+        RS_LUBY
+    };
+
+    enum gc_strategy {
+        GC_DYN_PSM,
+        GC_PSM,
+        GC_GLUE,
+        GC_GLUE_PSM,
+        GC_PSM_GLUE
+    };
+
+    struct config {
+        unsigned long long m_max_memory;
+        phase_selection    m_phase;
+        unsigned           m_phase_caching_on;
+        unsigned           m_phase_caching_off;
+        restart_strategy   m_restart;
+        unsigned           m_restart_initial;
+        double             m_restart_factor; // for geometric case
+        double             m_random_freq;
+        unsigned           m_burst_search;
+        unsigned           m_max_conflicts;
+
+        unsigned           m_simplify_mult1;
+        double             m_simplify_mult2;
+        unsigned           m_simplify_max;
+
+        gc_strategy        m_gc_strategy;
+        unsigned           m_gc_initial;
+        unsigned           m_gc_increment;
+        unsigned           m_gc_small_lbd;
+        unsigned           m_gc_k;
+
+        bool               m_minimize_lemmas;
+        bool               m_dyn_sub_res;
+
+        symbol             m_always_true;
+        symbol             m_always_false;
+        symbol             m_caching;
+        symbol             m_random;
+        symbol             m_geometric;
+        symbol             m_luby;
+        
+        symbol             m_dyn_psm;
+        symbol             m_psm;        
+        symbol             m_glue;        
+        symbol             m_glue_psm;        
+        symbol             m_psm_glue;        
+        
+        config(params_ref const & p);
+        void updt_params(params_ref const & p);
+        static void collect_param_descrs(param_descrs & d);
+    };
+};
+
+#endif

src/sat/sat_elim_eqs.cpp

@@ -0,0 +1,220 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_elim_eqs.cpp
+
+Abstract:
+
+    Helper class for eliminating eqs.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-27.
+
+Revision History:
+
+--*/
+#include"sat_elim_eqs.h"
+#include"sat_solver.h"
+#include"trace.h"
+
+namespace sat {
+    
+    elim_eqs::elim_eqs(solver & s):
+        m_solver(s) {
+    }
+
+    inline literal norm(literal_vector const & roots, literal l) {
+        if (l.sign()) 
+            return ~roots[l.var()];
+        else
+            return roots[l.var()];
+    }
+
+    void elim_eqs::cleanup_bin_watches(literal_vector const & roots) {
+        vector<watch_list>::iterator it  = m_solver.m_watches.begin();
+        vector<watch_list>::iterator end = m_solver.m_watches.end();
+        for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
+            watch_list & wlist = *it;
+            literal l1 = ~to_literal(l_idx);
+            literal r1 = norm(roots, l1);
+            watch_list::iterator it2    = wlist.begin();
+            watch_list::iterator itprev = it2;
+            watch_list::iterator end2   = wlist.end();
+            for (; it2 != end2; ++it2) {
+                if (it2->is_binary_clause()) {
+                    literal l2 = it2->get_literal();
+                    literal r2 = norm(roots, l2);
+                    if (r1 == r2) {
+                        m_solver.assign(r1, justification());
+                        if (m_solver.inconsistent())
+                            return;
+                        // consume unit
+                        continue;
+                    }
+                    if (r1 == ~r2) {
+                        // consume tautology
+                        continue;
+                    }
+                    if (l1 != r1) {
+                        // add half r1 => r2, the other half ~r2 => ~r1 is added when traversing l2 
+                        m_solver.m_watches[(~r1).index()].push_back(watched(r2, it2->is_learned()));
+                        continue;
+                    }
+                    it2->set_literal(r2); // keep it
+                }
+                *itprev = *it2;
+                itprev++;
+            }
+            wlist.set_end(itprev);
+        }
+    }
+
+    void elim_eqs::cleanup_clauses(literal_vector const & roots, clause_vector & cs) {
+        clause_vector::iterator it  = cs.begin();
+        clause_vector::iterator it2 = it;
+        clause_vector::iterator end = cs.end();
+        for (; it != end; ++it) {
+            clause & c     = *(*it);
+            TRACE("elim_eqs", tout << "processing: " << c << "\n";);
+            unsigned sz    = c.size();
+            unsigned i;
+            for (i = 0; i < sz; i++) {
+                literal l = c[i];
+                literal r = norm(roots, l);
+                if (l != r)
+                    break;
+            }
+            if (i == sz) {
+                // clause was not affected
+                *it2 = *it;
+                it2++;
+                continue;
+            }
+            if (!c.frozen())
+                m_solver.dettach_clause(c);
+            // apply substitution
+            for (i = 0; i < sz; i++) {
+                SASSERT(!m_solver.was_eliminated(c[i].var()));
+                c[i] = norm(roots, c[i]);
+            }
+            std::sort(c.begin(), c.end());
+            TRACE("elim_eqs", tout << "after normalization/sorting: " << c << "\n";);
+            // remove duplicates, and check if it is a tautology
+            literal l_prev = null_literal;
+            unsigned j = 0;
+            for (i = 0; i < sz; i++) {
+                literal l = c[i];
+                if (l == l_prev)
+                    continue;
+                if (l == ~l_prev)
+                    break;
+                l_prev = l;
+                lbool val = m_solver.value(l);
+                if (val == l_true)
+                    break; // clause was satisfied
+                if (val == l_false)
+                    continue; // skip
+                c[j] = l;
+                j++;
+            }
+            if (i < sz) {
+                // clause is a tautology or was simplified
+                m_solver.del_clause(c);
+                continue; 
+            }
+            if (j == 0) {
+                // empty clause
+                m_solver.set_conflict(justification());
+                return;
+            }
+            TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";);
+            if (j < sz)
+                c.shrink(j);
+            else
+                c.update_approx();
+            SASSERT(c.size() == j);
+            DEBUG_CODE({
+                for (unsigned i = 0; i < c.size(); i++) {
+                    SASSERT(c[i] == norm(roots, c[i]));
+                }
+            });
+            SASSERT(j >= 1);
+            switch (j) {
+            case 1:
+                m_solver.assign(c[0], justification());
+                m_solver.del_clause(c);
+                break;
+            case 2:
+                m_solver.mk_bin_clause(c[0], c[1], c.is_learned());
+                m_solver.del_clause(c);
+                break;
+            default:
+                SASSERT(*it == &c);
+                *it2 = *it;
+                it2++;
+                if (!c.frozen())
+                    m_solver.attach_clause(c);
+                break;
+            }
+        }
+        cs.set_end(it2);
+    }
+
+    void elim_eqs::save_elim(literal_vector const & roots, bool_var_vector const & to_elim) {
+        model_converter & mc = m_solver.m_mc;
+        bool_var_vector::const_iterator it  = to_elim.begin();
+        bool_var_vector::const_iterator end = to_elim.end();
+        for (; it != end; ++it) {
+            bool_var v = *it;
+            literal  l(v, false);
+            literal r  = roots[v];
+            SASSERT(v != r.var());
+            if (m_solver.is_external(v)) {
+                // cannot really eliminate v, since we have to notify extension of future assignments
+                m_solver.mk_bin_clause(~l, r, false);
+                m_solver.mk_bin_clause(l, ~r, false);
+            }
+            else {
+                model_converter::entry & e = mc.mk(model_converter::ELIM_VAR, v);
+                TRACE("save_elim", tout << "marking as deleted: " << v << " l: " << l << " r: " << r << "\n";);
+                m_solver.m_eliminated[v] = true;
+                mc.insert(e, ~l, r);
+                mc.insert(e,  l, ~r);
+            }
+        }
+    }
+
+    bool elim_eqs::check_clauses(literal_vector const & roots) const {
+        clause_vector * vs[2] = { &m_solver.m_clauses, &m_solver.m_learned };
+        for (unsigned i = 0; i < 2; i++) {
+            clause_vector & cs  = *(vs[i]);
+            clause_vector::iterator it  = cs.begin();
+            clause_vector::iterator end = cs.end();
+            for (; it != end; ++it) {
+                clause & c  = *(*it);
+                unsigned sz = c.size();
+                for (unsigned i = 0; i < sz; i++) {
+                    CTRACE("elim_eqs_bug", m_solver.was_eliminated(c[i].var()), tout << "lit: " << c[i] << " " << norm(roots, c[i]) << "\n";
+                           tout << c << "\n";);
+                    SASSERT(!m_solver.was_eliminated(c[i].var()));
+                }
+            }
+        }
+        return true;
+    }
+
+    void elim_eqs::operator()(literal_vector const & roots, bool_var_vector const & to_elim) {
+        cleanup_bin_watches(roots);
+        TRACE("elim_eqs", tout << "after bin cleanup\n"; m_solver.display(tout););
+        cleanup_clauses(roots, m_solver.m_clauses);
+        if (m_solver.inconsistent()) return;
+        cleanup_clauses(roots, m_solver.m_learned);
+        if (m_solver.inconsistent()) return;
+        save_elim(roots, to_elim);
+        m_solver.propagate(false);
+        SASSERT(check_clauses(roots));
+    }
+};

src/sat/sat_elim_eqs.h

@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_elim_eqs.h
+
+Abstract:
+
+    Helper class for eliminating eqs.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-27.
+
+Revision History:
+
+--*/
+#ifndef _SAT_ELIM_EQS_H_
+#define _SAT_ELIM_EQS_H_
+
+#include"sat_types.h"
+
+namespace sat {
+    class solver;
+    
+    class elim_eqs {
+        solver & m_solver;
+        void save_elim(literal_vector const & roots, bool_var_vector const & to_elim);
+        void cleanup_clauses(literal_vector const & roots, clause_vector & cs);
+        void cleanup_bin_watches(literal_vector const & roots);
+        bool check_clauses(literal_vector const & roots) const;
+    public:
+        elim_eqs(solver & s);
+        void operator()(literal_vector const & roots, bool_var_vector const & to_elim);
+    };
+
+};
+
+#endif

src/sat/sat_extension.h

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_extension.h
+
+Abstract:
+
+    An abstract class for SAT extensions.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+Revision History:
+
+--*/
+#ifndef _SAT_EXTENSION_H_
+#define _SAT_EXTENSION_H_
+
+#include"sat_types.h"
+#include"params.h"
+
+namespace sat {
+
+    enum check_result {
+        CR_DONE, CR_CONTINUE, CR_GIVEUP
+    };
+
+    class extension {
+    public:
+        virtual void propagate(literal l, ext_constraint_idx idx, bool & keep) = 0;
+        virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0;
+        virtual void asserted(literal l) = 0;
+        virtual check_result check() = 0;
+        virtual void push() = 0;
+        virtual void pop(unsigned n) = 0;
+        virtual void simplify() = 0;
+        virtual void clauses_modifed() = 0;
+        virtual lbool get_phase(bool_var v) = 0;
+    };
+
+};
+
+#endif

src/sat/sat_iff3_finder.cpp

@@ -0,0 +1,214 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_iff3_finder.cpp
+
+Abstract:
+
+    Find constraints of the form   x = l1 = l2
+    That is, search for clauses of the form
+      ~x \/ l1  \/ ~l2
+      ~x \/ ~l1 \/ l2
+       x \/ l1  \/ l2
+       x \/ ~l1 \/ ~l2
+       
+    The basic idea is to sort the watch lists.
+    
+    This information can be used to propagate equivalences
+    during probing (and search).
+
+    The initial experiments were disappointing.
+    Not using it on the solver.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-06-04.
+
+Revision History:
+
+--*/
+#include"sat_iff3_finder.h"
+#include"sat_solver.h"
+
+namespace sat {
+
+    struct iff3_lt {
+        bool operator()(watched const & w1, watched const & w2) const {
+            // keep th binary clauses in the beginning
+            if (w2.is_binary_clause()) return false;
+            if (w1.is_binary_clause()) return true;
+            //
+            if (w2.is_ternary_clause()) {
+                if (w1.is_ternary_clause()) {
+                    literal l1_1 = w1.get_literal1();
+                    literal l1_2 = w1.get_literal2();
+                    literal l2_1 = w2.get_literal1();
+                    literal l2_2 = w2.get_literal2();
+                    if (l1_1.index() < l2_1.index()) return true;
+                    if (l1_1.index() > l2_1.index()) return false;
+                    return l1_2.index() < l2_2.index();
+                }
+                return false;
+            }
+            if (w1.is_ternary_clause()) return true;
+            return false;
+        }
+    };
+
+    static void unmark(svector<bool> & marks, literal_vector & to_unmark) {
+        literal_vector::const_iterator it  = to_unmark.begin();
+        literal_vector::const_iterator end = to_unmark.end();
+        for (; it != end; ++it) {
+            marks[it->index()] = false;
+        }
+        to_unmark.reset();
+    }
+
+#define SMALL_WLIST 16
+
+    /**
+       \brief Return true if wlist contains (l1, l2)
+       It assumes wlist have been sorted using iff3_lt
+    */
+    static bool contains(watch_list const & wlist, literal l1, literal l2) {
+        watched k(l1, l2);
+        if (wlist.size() < SMALL_WLIST)
+            return wlist.contains(k);
+        iff3_lt lt;
+        int low  = 0;
+        int high = wlist.size(); 
+        while (true) {
+            int mid = low + ((high - low) / 2);
+            watched const & m = wlist[mid];
+            if (m == k)
+                return true;
+            if (lt(m, k)) {
+                low = mid + 1;
+            }
+            else {
+                SASSERT(lt(k, m));
+                high = mid - 1;
+            }
+            if (low > high)
+                return false;
+        }
+    }
+
+    iff3_finder::iff3_finder(solver & _s):
+        s(_s) {
+    }
+
+    void iff3_finder::sort_watches() {
+        vector<watch_list>::iterator it  = s.m_watches.begin();
+        vector<watch_list>::iterator end = s.m_watches.end();
+        for (; it != end; ++it) {
+            watch_list & wlist = *it;
+            std::stable_sort(wlist.begin(), wlist.end(), iff3_lt());
+        }
+    }
+
+    void iff3_finder::mk_eq(literal l1, literal l2) {
+        s.mk_clause(l1, ~l2);
+        s.mk_clause(~l1, l2);
+    }
+
+    void iff3_finder::operator()() {
+        TRACE("iff3_finder", tout << "starting iff3_finder\n";);
+        sort_watches();
+        
+        unsigned counter = 0;
+
+        svector<bool>   found;
+        found.resize(s.num_vars()*2, false);
+        literal_vector to_unmark;
+
+        typedef std::pair<literal, literal> lit_pair;
+        svector<lit_pair> pairs;
+
+        for (bool_var x = 0; x < s.num_vars(); x++) {
+            literal pos_x(x, false);
+            literal neg_x(x, true);
+            watch_list & pos_wlist = s.get_wlist(neg_x);
+            watch_list & neg_wlist = s.get_wlist(pos_x);
+            // 
+            TRACE("iff3_finder", 
+                  tout << "visiting: " << x << "\n";
+                  tout << "pos:\n";
+                  display(tout, s.m_cls_allocator, pos_wlist);
+                  tout << "\nneg:\n";
+                  display(tout, s.m_cls_allocator, neg_wlist);
+                  tout << "\n--------------\n";);
+            // traverse the ternary clauses x \/ l1 \/ l2
+            bool_var curr_v1 = null_bool_var;
+            watch_list::iterator it  = pos_wlist.begin();
+            watch_list::iterator end = pos_wlist.end();
+            for (; it != end; ++it) {
+                if (it->is_binary_clause())
+                    continue;
+                if (it->is_ternary_clause()) {
+                    literal l1  = it->get_literal1();
+                    if (l1.index() < pos_x.index())
+                        break; // stop
+                    literal l2  = it->get_literal2();
+                    bool_var v1 = l1.var();
+                    if (v1 != curr_v1) {
+                        curr_v1 = v1;
+                        unmark(found, to_unmark);
+                        pairs.reset();
+                    }
+                    if (!l1.sign()) {
+                        if (!found[l2.index()]) {
+                            found[l2.index()] = true;
+                            to_unmark.push_back(l2);
+                        }
+                    }
+                    else {
+                        l2.neg();
+                        if (found[l2.index()]) {
+                            // Found clauses x \/ v1 \/ l2 and x \/ ~v1 \/ ~l2
+                            // So, I have to find the clauses
+                            // ~x \/  v1 \/ ~l2
+                            // ~x \/ ~v1 \/ l2
+                            if (contains(neg_wlist, literal(v1, false), ~l2) &&
+                                contains(neg_wlist, literal(v1, true),  l2)) {
+                                // found new iff3
+                                // x = v1 = l2
+                                counter++;
+                                // verbose_stream() << counter << ": " << x << " = " << v1 << " = " << l2 << "\n";
+                                TRACE("iff3_finder", tout << counter << ": " << x << " = " << v1 << " = " << l2 << "\n";);
+                                l1.neg();
+                                svector<lit_pair>::iterator it2  = pairs.begin();
+                                svector<lit_pair>::iterator end2 = pairs.end();
+                                for (; it2 != end2; ++it2) {
+                                    if (it2->first == l1) {
+                                        // l2 == it2->second
+                                        mk_eq(l2, it2->second);
+                                    }
+                                    else if (it2->second == l1) {
+                                        // l2 == it2->first
+                                        mk_eq(l2, it2->first);
+                                    }
+                                    else if (it2->first == l2) {
+                                        // l1 == it2->second
+                                        mk_eq(l1, it2->second);
+                                    }
+                                    else if (it2->second == l2) {
+                                        // l1 == it2->first
+                                        mk_eq(l1, it2->first);
+                                    }
+                                }
+                                pairs.push_back(lit_pair(l1, l2));
+                            }
+                        }
+                    }
+                }
+                else {
+                    break; // stop, no more ternary clauses from this point
+                }
+            }
+        }
+    }
+    
+};

src/sat/sat_iff3_finder.h

@@ -0,0 +1,48 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_iff3_finder.h
+
+Abstract:
+
+    Find constraints of the form   x = l1 = l2
+    That is, search for clauses of the form
+      ~x \/ l1  \/ ~l2
+      ~x \/ ~l1 \/ l2
+       x \/ l1  \/ l2
+       x \/ ~l1 \/ ~l2
+       
+    The basic idea is to sort the watch lists.
+    
+    This information can be used to propagate equivalences
+    during probing (and search).
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-06-04.
+
+Revision History:
+
+--*/
+#ifndef _SAT_IFF3_FINDER_H_
+#define _SAT_IFF3_FINDER_H_
+
+#include"sat_types.h"
+
+namespace sat {
+    
+    class iff3_finder {
+        solver & s;
+        void sort_watches();
+        void mk_eq(literal l1, literal l2);
+    public:
+        iff3_finder(solver & s);
+        
+        void operator()();
+    };
+
+};
+
+#endif

src/sat/sat_integrity_checker.cpp

@@ -0,0 +1,221 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_integrity_checker.cpp
+
+Abstract:
+
+    Checker whether the SAT solver internal datastructures 
+    are consistent or not.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+Revision History:
+
+--*/
+#include"sat_integrity_checker.h"
+#include"sat_solver.h"
+#include"trace.h"
+
+namespace sat {
+    
+    integrity_checker::integrity_checker(solver const & _s):
+        s(_s) {
+    }
+
+    // for ternary clauses 
+    static bool contains_watched(watch_list const & wlist, literal l1, literal l2) {
+        return wlist.contains(watched(l1, l2));
+    }
+    
+    // for nary clauses
+    static bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) {
+        watch_list::const_iterator it  = wlist.begin();
+        watch_list::const_iterator end = wlist.end();
+        for (; it != end; ++it) {
+            if (it->is_clause()) {
+                if (it->get_clause_offset() == cls_off) {
+                    // the blocked literal must be in the clause.
+                    literal l = it->get_blocked_literal();
+                    SASSERT(c.contains(l));
+                    return true;
+                }
+            }
+        }
+        UNREACHABLE();
+        return false;
+    }
+
+    bool integrity_checker::check_clause(clause const & c) const {
+        SASSERT(!c.was_removed());
+        for (unsigned i = 0; i < c.size(); i++) {
+            SASSERT(c[i].var() <= s.num_vars());
+            CTRACE("sat_bug", s.was_eliminated(c[i].var()),
+                   tout << "l: " << c[i].var() << "\n";
+                   tout << "c: " << c << "\n";
+                   s.display(tout););
+            SASSERT(!s.was_eliminated(c[i].var()));
+        }
+
+        SASSERT(c.check_approx());
+        
+        if (c.frozen())
+            return true;
+
+        if (c.size() == 3) {
+            CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n";
+                   tout << "watch_list:\n";
+                   sat::display(tout, s.m_cls_allocator, s.get_wlist(~c[0]));
+                   tout << "\n";);
+            SASSERT(contains_watched(s.get_wlist(~c[0]), c[1], c[2]));
+            SASSERT(contains_watched(s.get_wlist(~c[1]), c[0], c[2]));
+            SASSERT(contains_watched(s.get_wlist(~c[2]), c[0], c[1]));
+        }
+        else {
+            if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) {
+                bool on_prop_stack = false;
+                for (unsigned i = s.m_qhead; i < s.m_trail.size(); i++) {
+                    if (s.m_trail[i].var() == c[0].var() ||
+                        s.m_trail[i].var() == c[1].var()) {
+                        on_prop_stack = true;
+                        break;
+                    }
+                }
+                // the clause has been satisfied or all other literals are assigned to false.
+                if (!on_prop_stack && s.status(c) != l_true) {
+                    for (unsigned i = 2; i < c.size(); i++) {
+                        CTRACE("sat_bug", s.value(c[i]) != l_false,
+                               tout << c << " status: " << s.status(c) << "\n";
+                               for (unsigned i = 0; i < c.size(); i++) tout << "val(" << i << "): " << s.value(c[i]) << "\n";);
+                        SASSERT(s.value(c[i]) == l_false);
+                    }
+                }
+            }
+            
+            // the first two literals must be watched.
+            SASSERT(contains_watched(s.get_wlist(~c[0]), c, s.get_offset(c)));
+            SASSERT(contains_watched(s.get_wlist(~c[1]), c, s.get_offset(c)));
+        }
+        return true;
+    }
+
+    bool integrity_checker::check_clauses(clause * const * begin, clause * const * end) const {
+        for (clause * const * it = begin; it != end; ++it) {
+            SASSERT(check_clause(*(*it)));
+        }
+        return true;
+    }
+
+    bool integrity_checker::check_clauses() const {
+        return check_clauses(s.begin_clauses(), s.end_clauses());
+    }
+
+    bool integrity_checker::check_learned_clauses() const {
+        unsigned num_frozen = 0;
+        clause * const * end = s.end_clauses();
+        for (clause * const * it = s.begin_clauses(); it != end; ++it) {
+            clause & c = *(*it);
+            if (c.frozen())
+                num_frozen++;
+        }
+        SASSERT(num_frozen == s.m_num_frozen);
+        return check_clauses(s.begin_learned(), s.end_learned());
+    }
+
+    bool integrity_checker::check_assignment() const {
+        return true;
+    }
+
+    bool integrity_checker::check_bool_vars() const {
+        SASSERT(s.m_watches.size() == s.num_vars() * 2);
+        SASSERT(s.m_assignment.size() == s.num_vars() * 2);
+        SASSERT(s.m_lit_mark.size() == s.num_vars() * 2);
+        SASSERT(s.m_justification.size() == s.num_vars());
+        SASSERT(s.m_decision.size() == s.num_vars());
+        SASSERT(s.m_eliminated.size() == s.num_vars());
+        SASSERT(s.m_external.size() == s.num_vars());
+        SASSERT(s.m_level.size() == s.num_vars());
+        SASSERT(s.m_mark.size() == s.num_vars());
+        SASSERT(s.m_activity.size() == s.num_vars());
+        SASSERT(s.m_phase.size() == s.num_vars());
+        SASSERT(s.m_prev_phase.size() == s.num_vars());
+        SASSERT(s.m_assigned_since_gc.size() == s.num_vars());
+        for (bool_var v = 0; v < s.num_vars(); v++) {
+            if (s.was_eliminated(v)) {
+                SASSERT(s.get_wlist(literal(v, false)).empty());
+                SASSERT(s.get_wlist(literal(v, true)).empty());
+            }
+        }
+        return true;
+    }
+
+    bool integrity_checker::check_watches() const {
+        vector<watch_list>::const_iterator it  = s.m_watches.begin();
+        vector<watch_list>::const_iterator end = s.m_watches.end();
+        for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
+            literal l = ~to_literal(l_idx);
+            watch_list const & wlist = *it;
+            CTRACE("sat_bug", s.was_eliminated(l.var()) && !wlist.empty(),
+                   tout << "l: " << l << "\n";
+                   s.display_watches(tout);
+                   s.display(tout););
+            SASSERT(!s.was_eliminated(l.var()) || wlist.empty());
+            watch_list::const_iterator it2  = wlist.begin();
+            watch_list::const_iterator end2 = wlist.end();
+            for (; it2 != end2; ++it2) {
+                switch (it2->get_kind()) {
+                case watched::BINARY:
+                    SASSERT(!s.was_eliminated(it2->get_literal().var()));
+                    CTRACE("sat_watched_bug", !s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned())),
+                           tout << "l: " << l << " l2: " << it2->get_literal() << "\n"; 
+                           tout << "was_eliminated1: " << s.was_eliminated(l.var());
+                           tout << " was_eliminated2: " << s.was_eliminated(it2->get_literal().var());
+                           tout << " learned: " << it2->is_learned() << "\n";
+                           sat::display(tout, s.m_cls_allocator, wlist);
+                           tout << "\n";
+                           sat::display(tout, s.m_cls_allocator, s.get_wlist(~(it2->get_literal())));
+                           tout << "\n";);
+                    SASSERT(s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned())));
+                    break;
+                case watched::TERNARY:
+                    SASSERT(!s.was_eliminated(it2->get_literal1().var()));
+                    SASSERT(!s.was_eliminated(it2->get_literal2().var()));
+                    SASSERT(it2->get_literal1().index() < it2->get_literal2().index());
+                    break;
+                case watched::CLAUSE:
+                    SASSERT(!s.m_cls_allocator.get_clause(it2->get_clause_offset())->was_removed());
+                    break;
+                default:
+                    break;
+                }
+            }
+        }
+        return true;
+    }
+
+    bool integrity_checker::check_reinit_stack() const {
+        clause_wrapper_vector::const_iterator it  = s.m_clauses_to_reinit.begin();
+        clause_wrapper_vector::const_iterator end = s.m_clauses_to_reinit.end();
+        for (; it != end; ++it) {
+            if (it->is_binary())
+                continue;
+            SASSERT(it->get_clause()->on_reinit_stack());
+        }
+        return true;
+    }
+    
+    bool integrity_checker::operator()() const {
+        if (s.inconsistent())
+            return true;
+        SASSERT(check_clauses());
+        SASSERT(check_learned_clauses());
+        SASSERT(check_watches());
+        SASSERT(check_bool_vars());
+        SASSERT(check_reinit_stack());
+        return true;
+    }
+};

src/sat/sat_integrity_checker.h

@@ -0,0 +1,42 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_integrity_checker.h
+
+Abstract:
+
+    Checker whether the SAT solver internal datastructures 
+    are consistent or not.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+Revision History:
+
+--*/
+#ifndef _SAT_INTEGRITY_CHECKER_H_
+#define _SAT_INTEGRITY_CHECKER_H_
+
+#include"sat_types.h"
+
+namespace sat {
+    class integrity_checker {
+        solver const & s;
+    public:
+        integrity_checker(solver const & s);
+        
+        bool check_clause(clause const & c) const;
+        bool check_clauses(clause * const * begin, clause * const * end) const;
+        bool check_clauses() const;
+        bool check_learned_clauses() const;
+        bool check_assignment() const;
+        bool check_bool_vars() const;
+        bool check_watches() const;
+        bool check_reinit_stack() const;
+        bool operator()() const;
+    };
+};
+#endif

src/sat/sat_justification.h

@@ -0,0 +1,57 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_justification.h
+
+Abstract:
+
+    Justifications for SAT assignments
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+Revision History:
+
+--*/
+#ifndef _SAT_JUSTIFICATIONS_H_
+#define _SAT_JUSTIFICATIONS_H_
+
+namespace sat {
+    
+    class justification {
+    public:
+        enum kind { NONE, BINARY, TERNARY, CLAUSE, EXT_JUSTIFICATION };
+    private:
+        unsigned m_val1;
+        unsigned m_val2; 
+        justification(ext_justification_idx idx, kind k):m_val1(idx), m_val2(k) {}
+    public:
+        justification():m_val1(0), m_val2(NONE) {}
+        justification(literal l):m_val1(l.to_uint()), m_val2(BINARY) {}
+        justification(literal l1, literal l2):m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {}
+        justification(clause_offset cls_off):m_val1(cls_off), m_val2(CLAUSE) {}
+        justification mk_ext_justification(ext_justification_idx idx) { return justification(idx, EXT_JUSTIFICATION); }
+        
+        kind get_kind() const { return static_cast<kind>(m_val2 & 7); }
+        
+        bool is_none() const { return m_val2 == NONE; }
+        
+        bool is_binary_clause() const { return m_val2 == BINARY; }
+        literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(m_val1); }
+
+        bool is_ternary_clause() const { return get_kind() == TERNARY; }
+        literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(m_val1); }
+        literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 3); }
+
+        bool is_clause() const { return m_val2 == CLAUSE; }
+        clause_offset get_clause_offset() const { return m_val1; }
+        
+        bool is_ext_justification() const { return m_val2 == EXT_JUSTIFICATION; }
+        ext_justification_idx get_ext_justification_idx() const { return m_val1; }
+    };
+};
+
+#endif

src/sat/sat_model_converter.cpp

@@ -0,0 +1,240 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_model_converter.cpp
+
+Abstract:
+
+    Low level model converter for SAT solver.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-26.
+
+Revision History:
+
+--*/
+#include"sat_model_converter.h"
+#include"sat_clause.h"
+#include"trace.h"
+
+namespace sat {
+
+    model_converter::model_converter() {
+    }
+
+    model_converter::~model_converter() {
+        reset();
+    }
+
+    void model_converter::reset() {
+        m_entries.finalize();
+    }
+    
+    void model_converter::operator()(model & m) const {
+        vector<entry>::const_iterator begin = m_entries.begin();
+        vector<entry>::const_iterator it    = m_entries.end();
+        while (it != begin) {
+            --it;
+            SASSERT(it->get_kind() != ELIM_VAR || m[it->var()] == l_undef);
+            // if it->get_kind() == BLOCK_LIT, then it might be the case that m[it->var()] != l_undef,
+            // and the following procedure flips its value.
+            bool sat = false;
+            bool var_sign;
+            literal_vector::const_iterator it2  = it->m_clauses.begin();
+            literal_vector::const_iterator end2 = it->m_clauses.end();
+            for (; it2 != end2; ++it2) {
+                literal l  = *it2;
+                if (l == null_literal) {
+                    // end of clause
+                    if (!sat) {
+                        m[it->var()] = var_sign ? l_false : l_true;
+                        break;
+                    }
+                    sat = false;
+                    continue;
+                }
+                if (sat)
+                    continue;
+                bool sign  = l.sign();
+                bool_var v = l.var();
+                if (v == it->var())
+                    var_sign = sign;
+                if (value_at(l, m) == l_true)
+                    sat = true;
+                else if (!sat && v != it->var() && m[v] == l_undef) {
+                    // clause can be satisfied by assigning v.
+                    m[v] = sign ? l_false : l_true;
+                    sat = true;
+                }
+            }
+            DEBUG_CODE({
+                // all clauses must be satisfied
+                bool sat = false;
+                it2 = it->m_clauses.begin();
+                for (; it2 != end2; ++it2) {
+                    literal l = *it2;
+                    if (l == null_literal) {
+                        SASSERT(sat);
+                        sat = false;
+                        continue;
+                    }
+                    if (sat)
+                        continue;
+                    if (value_at(l, m) == l_true)
+                        sat = true;
+                }
+            });
+        }
+    }
+
+    /**
+       \brief Test if after applying the model converter, all eliminated clauses are
+       satisfied by m.
+    */
+    bool model_converter::check_model(model const & m) const {
+        bool ok = true;
+        vector<entry>::const_iterator begin = m_entries.begin();
+        vector<entry>::const_iterator it    = m_entries.end();
+        while (it != begin) {
+            --it;
+            bool sat = false;
+            literal_vector::const_iterator it2     = it->m_clauses.begin();
+            literal_vector::const_iterator itbegin = it2;
+            literal_vector::const_iterator end2    = it->m_clauses.end();
+            for (; it2 != end2; ++it2) {
+                literal l  = *it2;
+                if (l == null_literal) {
+                    // end of clause
+                    if (!sat) {
+                        TRACE("sat_model_bug", tout << "failed eliminated: " << mk_lits_pp(static_cast<unsigned>(it2 - itbegin), itbegin) << "\n";);
+                        ok = false;
+                    }
+                    sat = false;
+                    itbegin = it2;
+                    itbegin++;
+                    continue;
+                }
+                if (sat)
+                    continue;
+                if (value_at(l, m) == l_true)
+                    sat = true;
+            }
+        }
+        return ok;
+    }
+    
+    model_converter::entry & model_converter::mk(kind k, bool_var v) {
+        m_entries.push_back(entry(k, v));
+        entry & e = m_entries.back();
+        SASSERT(e.var() == v);
+        SASSERT(e.get_kind() == k);
+        return e;
+    }
+
+    void model_converter::insert(entry & e, clause const & c) {
+        SASSERT(c.contains(e.var()));
+        SASSERT(m_entries.begin() <= &e);
+        SASSERT(&e < m_entries.end());
+        unsigned sz = c.size();
+        for (unsigned i = 0; i < sz; i++) {
+            e.m_clauses.push_back(c[i]);
+        }
+        e.m_clauses.push_back(null_literal);
+        TRACE("sat_mc_bug", tout << "adding: " << c << "\n";);
+    }
+
+    void model_converter::insert(entry & e, literal l1, literal l2) {
+        SASSERT(l1.var() == e.var() || l2.var() == e.var());
+        SASSERT(m_entries.begin() <= &e);
+        SASSERT(&e < m_entries.end());
+        e.m_clauses.push_back(l1);
+        e.m_clauses.push_back(l2);
+        e.m_clauses.push_back(null_literal);
+        TRACE("sat_mc_bug", tout << "adding (binary): " << l1 << " " << l2 << "\n";);
+    }
+
+    void model_converter::insert(entry & e, clause_wrapper const & c) {
+        SASSERT(c.contains(e.var()));
+        SASSERT(m_entries.begin() <= &e);
+        SASSERT(&e < m_entries.end());
+        unsigned sz = c.size();
+        for (unsigned i = 0; i < sz; i++)
+            e.m_clauses.push_back(c[i]);
+        e.m_clauses.push_back(null_literal);
+        TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (unsigned i = 0; i < c.size(); i++) tout << c[i] << " "; tout << "\n";);
+    }
+
+    bool model_converter::check_invariant(unsigned num_vars) const {
+        // After a variable v occurs in an entry n and the entry has kind ELIM_VAR,
+        // then the variable must not occur in any other entry occurring after it.
+        vector<entry>::const_iterator it  = m_entries.begin();
+        vector<entry>::const_iterator end = m_entries.end();
+        for (; it != end; ++it) {
+            SASSERT(it->var() < num_vars);
+            if (it->get_kind() == ELIM_VAR) {
+                svector<entry>::const_iterator it2 = it;
+                it2++;
+                for (; it2 != end; ++it2) {
+                    SASSERT(it2->var() != it->var());
+                    literal_vector::const_iterator it3  = it2->m_clauses.begin();
+                    literal_vector::const_iterator end3 = it2->m_clauses.end();
+                    for (; it3 != end3; ++it3) {
+                        CTRACE("sat_model_converter", it3->var() == it->var(), tout << "var: " << it->var() << "\n"; display(tout););
+                        SASSERT(it3->var() != it->var());
+                        SASSERT(*it3 == null_literal || it3->var() < num_vars);
+                    }
+                }
+            }
+        }
+        return true;
+    }
+
+    void model_converter::display(std::ostream & out) const {
+        out << "(sat::model-converter";
+        vector<entry>::const_iterator it  = m_entries.begin();
+        vector<entry>::const_iterator end = m_entries.end();
+        for (; it != end; ++it) {
+            out << "\n  (" << (it->get_kind() == ELIM_VAR ? "elim" : "blocked") << " " << it->var();
+            bool start = true;
+            literal_vector::const_iterator it2  = it->m_clauses.begin();
+            literal_vector::const_iterator end2 = it->m_clauses.end();
+            for (; it2 != end2; ++it2) {
+                if (start) {
+                    out << "\n    (";
+                    start = false;
+                }
+                else {
+                    if (*it2 != null_literal)
+                        out << " ";
+                }
+                if (*it2 == null_literal) {
+                    out << ")";
+                    start = true;
+                    continue;
+                }
+                out << *it2;
+            }
+            out << ")";
+        }    
+        out << ")\n";
+    }
+
+    void model_converter::copy(model_converter const & src) {
+        vector<entry>::const_iterator it  = src.m_entries.begin();
+        vector<entry>::const_iterator end = src.m_entries.end();
+        for (; it != end; ++it)
+            m_entries.push_back(*it);
+    }
+
+    void model_converter::collect_vars(bool_var_set & s) const {
+        vector<entry>::const_iterator it  = m_entries.begin();
+        vector<entry>::const_iterator end = m_entries.end();
+        for (; it != end; ++it) {
+            s.insert(it->m_var);
+        }
+    }
+
+};

src/sat/sat_model_converter.h

@@ -0,0 +1,81 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_model_converter.h
+
+Abstract:
+
+    Low level model converter for SAT solver.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-26.
+
+Revision History:
+
+--*/
+#ifndef _SAT_MODEL_CONVERTER_H_
+#define _SAT_MODEL_CONVERTER_H_
+
+#include"sat_types.h"
+
+namespace sat {
+    /**
+       \brief Stores eliminated variables and Blocked clauses.
+       It uses these clauses to extend/patch the model produced for the
+       simplified CNF formula.
+       
+       This information may also be used to support incremental solving.
+       If new clauses are asserted into the SAT engine, then we can
+       restore the state by re-asserting all clauses in the model
+       converter.
+
+       This is a low-level model_converter. Given a mapping from bool_var to expr,
+       it can be converted into a general Z3 model_converter
+    */
+    class model_converter {
+    public:
+        enum kind { ELIM_VAR = 0, BLOCK_LIT };
+        class entry {
+            friend class model_converter;
+            unsigned           m_var:31;
+            unsigned           m_kind:1;
+            literal_vector     m_clauses; // the different clauses are separated by null_literal
+            entry(kind k, bool_var v):m_var(v), m_kind(k) {}
+        public:
+            entry(entry const & src):
+                m_var(src.m_var),
+                m_kind(src.m_kind),
+                m_clauses(src.m_clauses) {
+            }
+            bool_var var() const { return m_var; } 
+            kind get_kind() const { return static_cast<kind>(m_kind); }
+        };
+    private:
+        vector<entry>          m_entries;
+    public:
+        model_converter();
+        ~model_converter();
+        void operator()(model & m) const;
+
+        entry & mk(kind k, bool_var v);
+        void insert(entry & e, clause const & c);
+        void insert(entry & e, literal l1, literal l2);
+        void insert(entry & e, clause_wrapper const & c);
+
+        bool empty() const { return m_entries.empty(); }
+
+        void reset();
+        bool check_invariant(unsigned num_vars) const;
+        void display(std::ostream & out) const;
+        bool check_model(model const & m) const;
+
+        void copy(model_converter const & src);
+        void collect_vars(bool_var_set & s) const;
+    };
+    
+};
+
+#endif

src/sat/sat_probing.cpp

@@ -0,0 +1,269 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_probing.cpp
+
+Abstract:
+
+    Probing (aka failed literal detection).
+
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-06-04.
+
+Revision History:
+
+--*/
+#include"sat_probing.h"
+#include"sat_solver.h"
+
+namespace sat {
+    probing::probing(solver & _s, params_ref const & p):
+        s(_s) {
+        updt_params(p);
+        reset_statistics();
+        m_stopped_at = 0;
+        m_counter    = 0;
+    }
+
+    // reset the cache for the given literal
+    void probing::reset_cache(literal l) {
+        if (l.index() < m_cached_bins.size()) {
+            m_cached_bins[l.index()].m_available = false;
+            m_cached_bins[l.index()].m_lits.finalize();
+        }
+    }
+
+    // l implied the literals on the trail stack starting at position old_tr_sz
+    // Thus, ~l \/ l2 is a binary clause for every l2 on this fragment of the trail stack.
+    void probing::cache_bins(literal l, unsigned old_tr_sz) {
+        if (!m_probing_cache)
+            return;
+        if (memory::get_allocation_size() > m_probing_cache_limit)
+            return; // not enough memory to spare
+        m_cached_bins.reserve(l.index() + 1);
+        cache_entry & entry = m_cached_bins[l.index()];
+        entry.m_available = true;
+        entry.m_lits.reset();
+        unsigned tr_sz = s.m_trail.size();
+        for (unsigned i = old_tr_sz; i < tr_sz; i++) {
+            entry.m_lits.push_back(s.m_trail[i]);
+        }
+    }
+
+    // Return true if should keep going.
+    // It will assert literals implied by l that are already marked
+    // as assigned.
+    bool probing::try_lit(literal l, bool updt_cache) {
+        SASSERT(s.m_qhead == s.m_trail.size());
+        SASSERT(s.value(l.var()) == l_undef);
+        literal_vector * implied_lits = updt_cache ? 0 : cached_implied_lits(l);
+        if (implied_lits) {
+            literal_vector::iterator it  = implied_lits->begin();
+            literal_vector::iterator end = implied_lits->end();
+            for (; it != end; ++it) {
+                if (m_assigned.contains(*it)) {
+                    s.assign(*it, justification());
+                    m_num_assigned++;
+                }
+            }
+        }
+        else {
+            m_to_assert.reset();
+            s.push();
+            s.assign(l, justification());
+            m_counter--;
+            unsigned old_tr_sz = s.m_trail.size();
+            s.propagate(false);
+            if (s.inconsistent()) {
+                // ~l must be true
+                s.pop(1);
+                s.assign(~l, justification());
+                s.propagate(false);
+                return false;
+            }
+            // collect literals that were assigned after assigning l
+            unsigned tr_sz = s.m_trail.size();
+            for (unsigned i = old_tr_sz; i < tr_sz; i++) {
+                if (m_assigned.contains(s.m_trail[i])) {
+                    m_to_assert.push_back(s.m_trail[i]);
+                }
+            }
+            if (updt_cache)
+                cache_bins(l, old_tr_sz);
+            s.pop(1);
+            
+            literal_vector::iterator it  = m_to_assert.begin();
+            literal_vector::iterator end = m_to_assert.end();
+            for (; it != end; ++it) {
+                s.assign(*it, justification());
+                m_num_assigned++;
+            }
+        }
+        s.propagate(false);
+        return !s.inconsistent();
+    }
+
+    void probing::process_core(bool_var v) {
+        TRACE("probing", tout << "processing: " << v << " counter: " << -m_counter << "\n";);
+        SASSERT(s.m_qhead == s.m_trail.size());
+        SASSERT(s.value(v) == l_undef);
+        m_counter--;
+        s.push();
+        literal l(v, false);
+        s.assign(l, justification());
+        unsigned old_tr_sz = s.m_trail.size();
+        s.propagate(false);
+        if (s.inconsistent()) {
+            // ~l must be true
+            s.pop(1);
+            s.assign(~l, justification());
+            s.propagate(false);
+            m_num_assigned++;
+            return;
+        }
+        // collect literals that were assigned after assigning l
+        m_assigned.reset();
+        unsigned tr_sz = s.m_trail.size();
+        for (unsigned i = old_tr_sz; i < tr_sz; i++) {
+            m_assigned.insert(s.m_trail[i]);
+        }
+        cache_bins(l, old_tr_sz);
+        s.pop(1);
+
+        if (!try_lit(~l, true))
+            return;
+
+        if (m_probing_binary) {
+            watch_list & wlist = s.get_wlist(~l);
+            watch_list::iterator it  = wlist.begin();
+            watch_list::iterator end = wlist.end();
+            for (; it != end ; ++it) {
+                if (!it->is_binary_clause())
+                    break;
+                literal l2 = it->get_literal();
+                if (l.index() > l2.index())
+                    continue;
+                if (s.value(l2) != l_undef)
+                    continue;
+                // verbose_stream() << "probing " << l << " " << l2 << " " << m_counter << "\n";
+                if (!try_lit(l2, false))
+                    return;
+                if (s.inconsistent())
+                    return;
+            }
+        }
+    }
+
+    void probing::process(bool_var v) {
+        int old_counter = m_counter;
+        unsigned old_num_assigned = m_num_assigned;
+        process_core(v);
+        if (m_num_assigned > old_num_assigned) {
+            // if new variables were assigned when probing x,
+            // then assume the cost is 0.
+            m_counter = old_counter;
+        }
+    }
+
+    struct probing::report {
+        probing    & m_probing;
+        stopwatch    m_watch;
+        unsigned     m_num_assigned;
+        report(probing & p):
+            m_probing(p),
+            m_num_assigned(p.m_num_assigned) {
+            m_watch.start();
+        }
+        
+        ~report() {
+            m_watch.stop();
+            IF_VERBOSE(SAT_VB_LVL, 
+                       verbose_stream() << " (sat-probing :probing-assigned "
+                       << (m_probing.m_num_assigned - m_num_assigned)
+                       << " :cost " << m_probing.m_counter;
+                       if (m_probing.m_stopped_at != 0) verbose_stream() << " :stopped-at " << m_probing.m_stopped_at;
+                       verbose_stream() << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
+        }
+    };
+     
+    bool probing::operator()(bool force) {
+        if (!m_probing)
+            return true;
+        s.propagate(false); // make sure propagation queue is empty
+        if (s.inconsistent())
+            return true;
+        CASSERT("probing", s.check_invariant());
+        if (!force && m_counter > 0)
+            return true;
+        
+        if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit) 
+            m_cached_bins.finalize();
+
+        report rpt(*this);
+        bool r    = true;
+        m_counter = 0;
+        int limit = -static_cast<int>(m_probing_limit);
+        unsigned i;
+        unsigned num = s.num_vars();
+        for (i = 0; i < num; i++) {
+            bool_var v = (m_stopped_at + i) % num;
+            if (m_counter < limit) {
+                m_stopped_at = v;
+                r = false;
+                break;
+            }
+            if (s.inconsistent()) {
+                break;
+            }
+            if (s.value(v) != l_undef || s.was_eliminated(v)) {
+                if (m_probing_cache) {
+                    // cache for v literals is not needed anymore.
+                    reset_cache(literal(v, false));
+                    reset_cache(literal(v, true));
+                }
+                continue;
+            }
+            s.checkpoint();
+            process(v);
+        }
+        if (r)
+            m_stopped_at = 0;
+        m_counter = -m_counter;
+        if (rpt.m_num_assigned == m_num_assigned) {
+            // penalize
+            m_counter *= 2;
+        }
+        CASSERT("probing", s.check_invariant());
+        free_memory();
+        return r;
+    }
+
+    void probing::updt_params(params_ref const & p) {
+        m_probing             = p.get_bool(":probing", true);
+        m_probing_limit       = p.get_uint(":probing-limit", 5000000);
+        m_probing_cache       = p.get_bool(":probing-cache", true);
+        m_probing_binary      = p.get_bool(":probing-binary", true);
+        m_probing_cache_limit = megabytes_to_bytes(p.get_uint(":probing-chache-limit", 1024));
+    }
+
+    void probing::collect_param_descrs(param_descrs & d) {
+        // TODO
+    }
+
+    void probing::free_memory() {
+        m_assigned.cleanup();
+        m_to_assert.finalize();
+    }
+    
+    void probing::collect_statistics(statistics & st) {
+        st.update("probing assigned", m_num_assigned);
+    }
+    
+    void probing::reset_statistics() {
+        m_num_assigned = 0;
+    }
+};

src/sat/sat_probing.h

@@ -0,0 +1,92 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_probing.h
+
+Abstract:
+
+    Probing (aka failed literal detection).
+
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-06-04.
+
+Revision History:
+
+--*/
+#ifndef _SAT_PROBING_H_
+#define _SAT_PROBING_H_
+
+#include"sat_types.h"
+#include"params.h"
+#include"statistics.h"
+
+namespace sat {
+
+    class probing {
+        solver &        s;
+        unsigned        m_stopped_at;  // where did it stop
+        literal_set     m_assigned;    // literals assigned in the first branch
+        literal_vector  m_to_assert;
+
+        // counters
+        int             m_counter;       // track cost
+
+        // config
+        bool               m_probing;             // enabled/disabled
+        unsigned           m_probing_limit;       // max cost per round
+        bool               m_probing_cache;       // cache implicit binary clauses
+        bool               m_probing_binary;      // try l1 and l2 for binary clauses l1 \/ l2
+        unsigned long long m_probing_cache_limit; // memory limit for enabling caching.
+
+        // stats
+        unsigned           m_num_assigned;
+        
+        struct cache_entry {
+            bool           m_available;
+            literal_vector m_lits; 
+            cache_entry():m_available(false) {}
+        };
+
+        vector<cache_entry> m_cached_bins;  
+
+        struct report;
+
+        void reset_cache(literal l);
+        void cache_bins(literal l, unsigned old_tr_sz);
+        bool try_lit(literal l, bool updt_cache);
+        void process(bool_var v);
+        void process_core(bool_var v);
+
+    public:
+        probing(solver & s, params_ref const & p);
+        
+        bool operator()(bool force = false);
+
+        void updt_params(params_ref const & p);
+        static void collect_param_descrs(param_descrs & d);
+
+        void free_memory();
+
+        void collect_statistics(statistics & st);
+        void reset_statistics();
+
+        // return the literals implied by l.
+        // return 0, if the cache is not available
+        literal_vector * cached_implied_lits(literal l) {
+            if (!m_probing_cache) return 0;
+            if (l.index() >= m_cached_bins.size()) return 0;
+            cache_entry & e = m_cached_bins[l.index()];
+            if (!e.m_available) return 0;
+            return &(e.m_lits);
+        }
+
+        void dec(unsigned c) { m_counter -= c; }
+    };
+
+};
+
+#endif

src/sat/sat_scc.cpp

@@ -0,0 +1,241 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_scc.cpp
+
+Abstract:
+
+    Use binary clauses to compute strongly connected components.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-26.
+
+Revision History:
+
+--*/
+#include"sat_scc.h"
+#include"sat_solver.h"
+#include"sat_elim_eqs.h"
+#include"stopwatch.h"
+#include"trace.h"
+
+namespace sat {
+
+    scc::scc(solver & s, params_ref const & p):
+        m_solver(s) {
+        reset_statistics();
+        updt_params(p);
+    }
+
+    struct frame {
+        unsigned  m_lidx;
+        bool      m_first;
+        watched * m_it;
+        watched * m_end;
+        frame(unsigned lidx, watched * it, watched * end):m_lidx(lidx), m_first(true), m_it(it), m_end(end) {}
+    };
+    typedef svector<frame> frames;
+
+    struct scc::report {
+        scc &     m_scc;
+        stopwatch m_watch;
+        unsigned  m_num_elim;
+        report(scc & c):
+            m_scc(c),
+            m_num_elim(c.m_num_elim) {
+            m_watch.start();
+        }
+        ~report() {
+            m_watch.stop();
+            IF_VERBOSE(SAT_VB_LVL, 
+                       verbose_stream() << " (sat-scc :elim-vars " << (m_scc.m_num_elim - m_num_elim)
+                       << mk_stat(m_scc.m_solver)
+                       << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
+        }
+    };
+
+    unsigned scc::operator()() {
+        if (m_solver.m_inconsistent)
+            return 0;
+        if (!m_scc)
+            return 0;
+        CASSERT("scc_bug", m_solver.check_invariant());
+        report rpt(*this);
+        TRACE("scc", m_solver.display(tout););
+        TRACE("scc_details", m_solver.display_watches(tout););
+        unsigned_vector index;
+        unsigned_vector lowlink;
+        unsigned_vector s;
+        svector<char>   in_s;
+        unsigned num_lits = m_solver.num_vars() * 2;
+        index.resize(num_lits, UINT_MAX);
+        lowlink.resize(num_lits, UINT_MAX);
+        in_s.resize(num_lits, false);
+        literal_vector roots;
+        roots.resize(m_solver.num_vars(), null_literal);
+        unsigned next_index = 0;
+        svector<frame>   frames;
+        bool_var_vector  to_elim;
+        
+        for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
+            if (index[l_idx] != UINT_MAX)
+                continue;
+            if (m_solver.was_eliminated(to_literal(l_idx).var()))
+                continue;
+            
+            m_solver.checkpoint();
+
+#define NEW_NODE(LIDX) {                                                        \
+                index[LIDX]   = next_index;                                     \
+                lowlink[LIDX] = next_index;                                     \
+                next_index++;                                                   \
+                s.push_back(LIDX);                                              \
+                in_s[LIDX] = true;                                              \
+                watch_list & wlist = m_solver.get_wlist(LIDX);                  \
+                frames.push_back(frame(LIDX, wlist.begin(), wlist.end()));      \
+            }
+            
+            NEW_NODE(l_idx);
+            
+            while (!frames.empty()) {
+            loop:
+                frame & fr         = frames.back();
+                unsigned l_idx     = fr.m_lidx;
+                if (!fr.m_first) {
+                    // after visiting child
+                    literal l2 = fr.m_it->get_literal();
+                    unsigned l2_idx = l2.index();
+                    SASSERT(index[l2_idx] != UINT_MAX);
+                    if (lowlink[l2_idx] < lowlink[l_idx])
+                        lowlink[l_idx] = lowlink[l2_idx];
+                    fr.m_it++;
+                }
+                fr.m_first = false;
+                while (fr.m_it != fr.m_end) {
+                    if (!fr.m_it->is_binary_clause()) {
+                        fr.m_it++;
+                        continue;
+                    }
+                    literal l2 = fr.m_it->get_literal();
+                    unsigned l2_idx = l2.index();
+                    if (index[l2_idx] == UINT_MAX) {
+                        NEW_NODE(l2_idx);
+                        goto loop;
+                    }
+                    else if (in_s[l2_idx]) {
+                        if (index[l2_idx] < lowlink[l_idx])
+                            lowlink[l_idx] = index[l2_idx];
+                    }
+                    fr.m_it++;
+                }
+                // visited all successors
+                if (lowlink[l_idx] == index[l_idx]) {
+                    // found new SCC
+                    CTRACE("scc_cycle", s.back() != l_idx, {
+                          tout << "cycle: ";
+                          unsigned j = s.size() - 1;
+                          unsigned l2_idx;
+                          do {
+                              l2_idx = s[j];
+                              j--;
+                              tout << to_literal(l2_idx) << " ";
+                          }
+                          while (l2_idx != l_idx);
+                          tout << "\n";
+                    });
+                    
+                    SASSERT(!s.empty());
+                    literal l  = to_literal(l_idx);
+                    bool_var v = l.var();
+                    if (roots[v] != null_literal) {
+                        // variable was already assigned... just consume stack
+                        TRACE("scc_detail", tout << "consuming stack...\n";);
+                        unsigned l2_idx;
+                        do {
+                            l2_idx = s.back();
+                            s.pop_back();
+                            in_s[l2_idx]  = false;
+                            SASSERT(roots[to_literal(l2_idx).var()].var() == roots[v].var());
+                        }
+                        while (l2_idx != l_idx);
+                    }
+                    else {
+                        // check if the SCC has an external variable, and check for conflicts
+                        TRACE("scc_detail", tout << "assigning roots...\n";);
+                        literal  r = null_literal;
+                        unsigned j = s.size() - 1;
+                        unsigned l2_idx;
+                        do {
+                            l2_idx = s[j];
+                            j--;
+                            if (to_literal(l2_idx) == ~l) {
+                                m_solver.set_conflict(justification());
+                                return 0;
+                            }
+                            if (m_solver.is_external(to_literal(l2_idx).var())) {
+                                r = to_literal(l2_idx);
+                                break;
+                            }
+                        }
+                        while (l2_idx != l_idx);
+                        
+                        if (r == null_literal) {
+                            // SCC does not contain external variable
+                            r = to_literal(l_idx);
+                        }
+                        
+                        TRACE("scc_detail", tout << "r: " << r << "\n";);
+
+                        do {
+                            l2_idx = s.back();
+                            s.pop_back();
+                            in_s[l2_idx]  = false;
+                            literal  l2 = to_literal(l2_idx);
+                            bool_var v2 = l2.var();
+                            if (roots[v2] == null_literal) {
+                                if (l2.sign()) {
+                                    roots[v2] = ~r;
+                                }
+                                else {
+                                    roots[v2] = r;
+                                }
+                                if (v2 != r.var()) 
+                                    to_elim.push_back(v2);
+                            }
+                        }
+                        while (l2_idx != l_idx);
+                    }
+                }
+                frames.pop_back();
+            }
+        }
+        TRACE("scc", for (unsigned i = 0; i < roots.size(); i++) { tout << i << " -> " << roots[i] << "\n"; }
+              tout << "to_elim: "; for (unsigned i = 0; i < to_elim.size(); i++) tout << to_elim[i] << " "; tout << "\n";);
+        m_num_elim += to_elim.size();
+        elim_eqs eliminator(m_solver);
+        eliminator(roots, to_elim);
+        TRACE("scc_detail", m_solver.display(tout););
+        CASSERT("scc_bug", m_solver.check_invariant());
+        return to_elim.size();
+    }
+
+    void scc::collect_statistics(statistics & st) {
+        st.update("elim bool vars", m_num_elim);
+    }
+    
+    void scc::reset_statistics() {
+        m_num_elim = 0;
+    }
+
+    void scc::updt_params(params_ref const & p) {
+        m_scc = p.get_bool(":scc", true);
+    }
+
+    void scc::collect_param_descrs(param_descrs & d) {
+        d.insert(":scc", CPK_BOOL, "(default: true) eliminate Boolean variables by computing strongly connected components.");
+    }
+
+};

src/sat/sat_scc.h

@@ -0,0 +1,48 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_scc.h
+
+Abstract:
+
+    Use binary clauses to compute strongly connected components.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-26.
+
+Revision History:
+
+--*/
+#ifndef _SAT_SCC_H_
+#define _SAT_SCC_H_
+
+#include"sat_types.h"
+#include"statistics.h"
+#include"params.h"
+
+namespace sat {
+    class solver;
+
+    class scc {
+        struct report;
+        solver &   m_solver;
+        // config
+        bool       m_scc;
+        // stats
+        unsigned   m_num_elim;
+    public:
+        scc(solver & s, params_ref const & p);
+        unsigned operator()();
+
+        void updt_params(params_ref const & p);
+        static void collect_param_descrs(param_descrs & d);
+
+        void collect_statistics(statistics & st);
+        void reset_statistics();
+    };
+};
+
+#endif

src/sat/sat_simplifier.h

@@ -0,0 +1,188 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_simplifier.h
+
+Abstract:
+
+    SAT simplification procedures that use a "full" occurrence list:
+    Subsumption, Blocked Clause Removal, Variable Elimination, ...
+    
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-24.
+
+Revision History:
+
+--*/
+#ifndef _SAT_SIMPLIFIER_H_
+#define _SAT_SIMPLIFIER_H_
+
+#include"sat_types.h"
+#include"sat_clause.h"
+#include"sat_clause_set.h"
+#include"sat_clause_use_list.h"
+#include"sat_watched.h"
+#include"sat_model_converter.h"
+#include"heap.h"
+#include"statistics.h"
+#include"params.h"
+
+namespace sat {
+    class solver;
+
+    class use_list {
+        vector<clause_use_list> m_use_list;
+    public:
+        void init(unsigned num_vars);
+        void insert(clause & c);
+        void erase(clause & c);
+        void erase(clause & c, literal l);
+        clause_use_list & get(literal l) { return m_use_list[l.index()]; }
+        clause_use_list const & get(literal l) const { return m_use_list[l.index()]; }
+        void finalize() { m_use_list.finalize(); }
+    };
+
+    class simplifier {
+        solver &               s;
+        unsigned               m_num_calls;
+        use_list               m_use_list;
+        clause_set             m_sub_todo;
+        svector<bin_clause>    m_sub_bin_todo;
+        unsigned               m_last_sub_trail_sz; // size of the trail since last cleanup
+        bool_var_set           m_elim_todo;
+        bool                   m_need_cleanup;
+        tmp_clause             m_dummy;
+
+        // simplifier extra variable fields.
+        svector<char>          m_visited; // transient
+
+        // counters
+        int                    m_sub_counter;
+        int                    m_elim_counter;
+
+        // config
+        bool                   m_elim_blocked_clauses;
+        unsigned               m_elim_blocked_clauses_at;
+        unsigned               m_blocked_clause_limit;
+        bool                   m_resolution;
+        unsigned               m_res_limit;
+        unsigned               m_res_occ_cutoff;
+        unsigned               m_res_occ_cutoff1;
+        unsigned               m_res_occ_cutoff2;
+        unsigned               m_res_occ_cutoff3;
+        unsigned               m_res_lit_cutoff1;
+        unsigned               m_res_lit_cutoff2;
+        unsigned               m_res_lit_cutoff3;
+        unsigned               m_res_cls_cutoff1;
+        unsigned               m_res_cls_cutoff2;
+
+        bool                   m_subsumption;
+        unsigned               m_subsumption_limit;
+        
+        // stats
+        unsigned               m_num_blocked_clauses;
+        unsigned               m_num_subsumed;
+        unsigned               m_num_elim_vars;
+        unsigned               m_num_sub_res;
+        unsigned               m_num_elim_lits;
+
+        struct size_lt {
+            bool operator()(clause const * c1, clause const * c2) const { return c1->size() > c2->size(); }
+        };
+
+        void checkpoint();
+
+        void init_visited();
+        void mark_visited(literal l) { m_visited[l.index()] = true; }
+        void unmark_visited(literal l) { m_visited[l.index()] = false; }
+        bool is_marked(literal l) const { return m_visited[l.index()] != 0; }
+        void mark_all_but(clause const & c, literal l);
+        void unmark_all(clause const & c);
+
+        void register_clauses(clause_vector & cs);
+
+        void remove_clause_core(clause & c);
+        void remove_clause(clause & c);
+        void remove_clause(clause & c, literal l);
+        void remove_bin_clause_half(literal l1, literal l2, bool learned);
+
+        bool_var get_min_occ_var(clause const & c) const;
+        bool subsumes1(clause const & c1, clause const & c2, literal & l);
+        void collect_subsumed1_core(clause const & c, clause_vector & out, literal_vector & out_lits, literal target);
+        void collect_subsumed1(clause const & c, clause_vector & out, literal_vector & out_lits);
+        clause_vector  m_bs_cs;
+        literal_vector m_bs_ls;
+        void back_subsumption1(clause & c);
+        void back_subsumption1(literal l1, literal l2, bool learned);
+
+        literal get_min_occ_var0(clause const & c) const;
+        bool subsumes0(clause const & c1, clause const & c2);
+        void collect_subsumed0_core(clause const & c1, clause_vector & out, literal target);
+        void collect_subsumed0(clause const & c1, clause_vector & out);
+        void back_subsumption0(clause & c1);
+
+        bool cleanup_clause(clause & c);
+        bool cleanup_clause(literal_vector & c);
+        void propagate_unit(literal l);
+        void elim_lit(clause & c, literal l);
+        void elim_dup_bins();
+        bool subsume_with_binaries();
+        void mark_as_not_learned_core(watch_list & wlist, literal l2);
+        void mark_as_not_learned(literal l1, literal l2);
+        void subsume();
+        
+        void cleanup_watches();
+        void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated);
+
+        bool is_external(bool_var v) const;
+        bool was_eliminated(bool_var v) const;
+        lbool value(bool_var v) const;
+        lbool value(literal l) const;
+        watch_list & get_wlist(literal l);
+        watch_list const & get_wlist(literal l) const;
+        
+        struct blocked_clause_elim;
+        void elim_blocked_clauses();
+
+        unsigned get_num_non_learned_bin(literal l) const;
+        unsigned get_to_elim_cost(bool_var v) const;
+        void order_vars_for_elim(bool_var_vector & r);
+        void collect_clauses(literal l, clause_wrapper_vector & r);
+        clause_wrapper_vector m_pos_cls;
+        clause_wrapper_vector m_neg_cls;
+        literal_vector m_new_cls;
+        bool resolve(clause_wrapper const & c1, clause_wrapper const & c2, literal l, literal_vector & r);
+        void save_clauses(model_converter::entry & mc_entry, clause_wrapper_vector const & cs);
+        void add_non_learned_binary_clause(literal l1, literal l2);
+        void remove_bin_clauses(literal l);
+        void remove_clauses(clause_use_list const & cs, literal l);
+        bool try_eliminate(bool_var v);
+        void elim_vars();
+
+        struct blocked_cls_report;
+        struct subsumption_report;
+        struct elim_var_report;
+
+    public:
+        simplifier(solver & s, params_ref const & p);
+        ~simplifier();
+
+        void insert_todo(bool_var v) { m_elim_todo.insert(v); }
+
+        void operator()(bool learned);
+
+        void updt_params(params_ref const & p);
+        static void collect_param_descrs(param_descrs & d);
+        
+        void free_memory();
+
+        void collect_statistics(statistics & st);
+        void reset_statistics();
+    };
+};
+
+#endif

src/sat/sat_solver.h

@@ -0,0 +1,428 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_solver.h
+
+Abstract:
+
+    SAT solver main class.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+Revision History:
+
+--*/
+#ifndef _SAT_SOLVER_H_
+#define _SAT_SOLVER_H_
+
+#include"sat_types.h"
+#include"sat_clause.h"
+#include"sat_watched.h"
+#include"sat_justification.h"
+#include"sat_var_queue.h"
+#include"sat_extension.h"
+#include"sat_config.h"
+#include"sat_cleaner.h"
+#include"sat_simplifier.h"
+#include"sat_scc.h"
+#include"sat_asymm_branch.h"
+#include"sat_iff3_finder.h"
+#include"sat_probing.h"
+#include"params.h"
+#include"statistics.h"
+#include"stopwatch.h"
+#include"trace.h"
+
+namespace sat {
+
+    /**
+       \brief Main statistic counters.
+    */
+    struct stats {
+        unsigned m_mk_var;
+        unsigned m_mk_bin_clause;
+        unsigned m_mk_ter_clause;
+        unsigned m_mk_clause;
+        unsigned m_conflict;
+        unsigned m_propagate;
+        unsigned m_bin_propagate;
+        unsigned m_ter_propagate;
+        unsigned m_decision;
+        unsigned m_restart;
+        unsigned m_gc_clause;
+        unsigned m_del_clause;
+        unsigned m_minimized_lits;
+        unsigned m_dyn_sub_res;
+        stats() { reset(); }
+        void reset();
+        void collect_statistics(statistics & st) const;
+    };
+    
+    class solver {
+    public:
+        struct abort_solver {};
+    protected:
+        volatile bool           m_cancel;
+        config                  m_config;
+        stats                   m_stats;
+        extension *             m_ext;
+        random_gen              m_rand;
+        clause_allocator        m_cls_allocator;
+        cleaner                 m_cleaner;
+        model                   m_model;
+        model_converter         m_mc;
+        simplifier              m_simplifier;
+        scc                     m_scc;
+        asymm_branch            m_asymm_branch;
+        probing                 m_probing;
+        bool                    m_inconsistent;
+        // A conflict is usually a single justification. That is, a justification
+        // for false. If m_not_l is not null_literal, then m_conflict is a
+        // justification for l, and the conflict is union of m_no_l and m_conflict;
+        justification           m_conflict;
+        literal                 m_not_l;
+        clause_vector           m_clauses;
+        clause_vector           m_learned;
+        unsigned                m_num_frozen;
+        vector<watch_list>      m_watches;
+        svector<lbool>          m_assignment;
+        svector<justification>  m_justification; 
+        svector<char>           m_decision;
+        svector<char>           m_mark;
+        svector<char>           m_lit_mark;
+        svector<char>           m_eliminated;
+        svector<char>           m_external;
+        svector<unsigned>       m_level; 
+        svector<unsigned>       m_activity;
+        unsigned                m_activity_inc;
+        svector<char>           m_phase; 
+        svector<char>           m_prev_phase;
+        svector<char>           m_assigned_since_gc;
+        bool                    m_phase_cache_on;
+        unsigned                m_phase_counter; 
+        var_queue               m_case_split_queue;
+        unsigned                m_qhead;
+        unsigned                m_scope_lvl;
+        literal_vector          m_trail;
+        clause_wrapper_vector   m_clauses_to_reinit;
+        struct scope {
+            unsigned m_trail_lim;
+            unsigned m_clauses_to_reinit_lim;
+            bool     m_inconsistent;
+        };
+        svector<scope>          m_scopes;
+        stopwatch               m_stopwatch;
+        params_ref              m_params;
+        scoped_ptr<solver>      m_clone; // for debugging purposes
+
+        void del_clauses(clause * const * begin, clause * const * end);
+
+        friend class integrity_checker;
+        friend class cleaner;
+        friend class simplifier;
+        friend class scc;
+        friend class elim_eqs;
+        friend class asymm_branch;
+        friend class probing;
+        friend class iff3_finder;
+        friend struct mk_stat;
+    public:
+        solver(params_ref const & p, extension * ext);
+        ~solver();
+
+        // -----------------------
+        //
+        // Misc
+        //
+        // -----------------------
+        void updt_params(params_ref const & p);
+        static void collect_param_descrs(param_descrs & d);
+
+        void set_cancel(bool f);
+        void collect_statistics(statistics & st);
+        void reset_statistics();
+        void display_status(std::ostream & out) const;
+        
+        /**
+           \brief Copy (non learned) clauses from src to this solver.
+           Create missing variables if needed.
+           
+           \pre the model converter of src and this must be empty
+        */
+        void copy(solver const & src);
+        
+        // -----------------------
+        //
+        // Variable & Clause creation
+        //
+        // -----------------------
+        bool_var mk_var(bool ext = false, bool dvar = true);
+        void mk_clause(unsigned num_lits, literal * lits);
+        void mk_clause(literal l1, literal l2);
+        void mk_clause(literal l1, literal l2, literal l3);
+
+    protected:
+        void del_clause(clause & c) { m_cls_allocator.del_clause(&c); m_stats.m_del_clause++; }
+        clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned);
+        void mk_bin_clause(literal l1, literal l2, bool learned);
+        bool propagate_bin_clause(literal l1, literal l2);
+        clause * mk_ter_clause(literal * lits, bool learned);
+        void attach_ter_clause(clause & c, bool & reinit);
+        void attach_ter_clause(clause & c) { bool reinit; attach_ter_clause(c, reinit); }
+        clause * mk_nary_clause(unsigned num_lits, literal * lits, bool learned);
+        void attach_nary_clause(clause & c, bool & reinit);
+        void attach_nary_clause(clause & c) { bool reinit; attach_nary_clause(c, reinit); }
+        void attach_clause(clause & c, bool & reinit);
+        void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
+        unsigned select_watch_lit(clause const & cls, unsigned starting_at) const;
+        unsigned select_learned_watch_lit(clause const & cls) const;
+        bool simplify_clause(unsigned & num_lits, literal * lits) const;
+        template<bool lvl0>
+        bool simplify_clause_core(unsigned & num_lits, literal * lits) const;
+        void dettach_bin_clause(literal l1, literal l2, bool learned);
+        void dettach_clause(clause & c);
+        void dettach_nary_clause(clause & c);
+        void dettach_ter_clause(clause & c);
+        void push_reinit_stack(clause & c);
+
+        // -----------------------
+        //
+        // Basic
+        //
+        // -----------------------
+    public:
+        bool inconsistent() const { return m_inconsistent; }
+        unsigned num_vars() const { return m_level.size(); }
+        bool is_external(bool_var v) const { return m_external[v] != 0; }
+        bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
+        unsigned scope_lvl() const { return m_scope_lvl; }
+        lbool value(literal l) const { return m_assignment[l.index()]; }
+        lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; }
+        unsigned lvl(bool_var v) const { return m_level[v]; }
+        unsigned lvl(literal l) const { return m_level[l.var()]; }
+        void assign(literal l, justification j) {
+            TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";);
+            switch (value(l)) {
+            case l_false: set_conflict(j, ~l); break;
+            case l_undef: assign_core(l, j); break;
+            case l_true:  return;
+            }
+        }
+        void assign_core(literal l, justification jst);
+        void set_conflict(justification c, literal not_l);
+        void set_conflict(justification c) { set_conflict(c, null_literal); }
+        lbool status(clause const & c) const;
+        clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
+        void checkpoint() {
+            if (m_cancel) throw solver_exception(TACTIC_CANCELED_MSG);
+            if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(TACTIC_MAX_MEMORY_MSG);
+        }
+    protected:
+        watch_list & get_wlist(literal l) { return m_watches[l.index()]; }
+        watch_list const & get_wlist(literal l) const { return m_watches[l.index()]; }
+        watch_list & get_wlist(unsigned l_idx) { return m_watches[l_idx]; }
+        bool is_marked(bool_var v) const { return m_mark[v] != 0; }
+        void mark(bool_var v) { SASSERT(!is_marked(v)); m_mark[v] = true; }
+        void reset_mark(bool_var v) { SASSERT(is_marked(v)); m_mark[v] = false; }
+        bool is_marked_lit(literal l) const { return m_lit_mark[l.index()] != 0; }
+        void mark_lit(literal l) { SASSERT(!is_marked_lit(l)); m_lit_mark[l.index()] = true; }
+        void unmark_lit(literal l) { SASSERT(is_marked_lit(l)); m_lit_mark[l.index()] = false; }
+
+        // -----------------------
+        //
+        // Propagation
+        //
+        // -----------------------
+    public:
+        // if update == true, then glue of learned clauses is updated.
+        bool propagate(bool update);
+
+    protected:
+        bool propagate_core(bool update);
+        
+        // -----------------------
+        //
+        // Search
+        //
+        // -----------------------
+    public:
+        lbool check();
+        model const & get_model() const { return m_model; }
+        model_converter const & get_model_converter() const { return m_mc; }
+
+    protected:
+        unsigned m_conflicts;
+        unsigned m_conflicts_since_restart;
+        unsigned m_restart_threshold;
+        unsigned m_luby_idx;
+        unsigned m_conflicts_since_gc;
+        unsigned m_gc_threshold;
+        double   m_min_d_tk;
+        unsigned m_next_simplify;
+        bool decide();
+        bool_var next_var();
+        lbool bounded_search();
+        void init_search();
+        void simplify_problem();
+        void mk_model();
+        bool check_model(model const & m) const;
+        void restart();
+        void sort_watch_lits();
+
+        // -----------------------
+        //
+        // GC
+        //
+        // -----------------------
+    protected:
+        void gc();
+        void gc_glue();
+        void gc_psm();
+        void gc_glue_psm();
+        void gc_psm_glue();
+        void save_psm();
+        void gc_half(char const * st_name);
+        void gc_dyn_psm();
+        bool activate_frozen_clause(clause & c);
+        unsigned psm(clause const & c) const;
+        bool can_delete(clause const & c) const {
+            if (c.on_reinit_stack())
+                return false;
+            if (c.size() == 3)
+                return true; // not needed to justify anything.
+            literal l0 = c[0];
+            if (value(l0) != l_true)
+                return true;
+            justification const & jst = m_justification[l0.var()];
+            return !jst.is_clause() || m_cls_allocator.get_clause(jst.get_clause_offset()) != &c;
+        }
+        
+        // -----------------------
+        //
+        // Conflict resolution
+        //
+        // -----------------------
+    protected:
+        unsigned       m_conflict_lvl;
+        literal_vector m_lemma;
+        literal_vector m_ext_antecedents;
+        bool resolve_conflict();
+        bool resolve_conflict_core();
+        unsigned get_max_lvl(literal consequent, justification js);
+        void process_antecedent(literal antecedent, unsigned & num_marks);
+        void fill_ext_antecedents(literal consequent, justification js);
+        unsigned skip_literals_above_conflict_level();
+        void forget_phase_of_vars(unsigned from_lvl);
+        void updt_phase_counters();
+        svector<char> m_diff_levels;
+        unsigned num_diff_levels(unsigned num, literal const * lits);
+
+        // lemma minimization
+        typedef approx_set_tpl<unsigned, u2u, unsigned> level_approx_set;
+        bool_var_vector   m_unmark;
+        level_approx_set  m_lvl_set;
+        bool_var_vector   m_lemma_min_stack;
+        bool process_antecedent_for_minimization(literal antecedent);
+        bool implied_by_marked(literal lit);
+        void reset_unmark(unsigned old_size);
+        void updt_lemma_lvl_set();
+        void minimize_lemma();
+        void reset_lemma_var_marks();
+        void dyn_sub_res();
+
+        // -----------------------
+        //
+        // Backtracking
+        //
+        // -----------------------
+    public:
+        void push();
+        void pop(unsigned num_scopes);
+
+    protected:
+        void unassign_vars(unsigned old_sz);
+        void reinit_clauses(unsigned old_sz);
+
+        // -----------------------
+        //
+        // Simplification
+        //
+        // -----------------------
+    public:
+        void cleanup();
+        void simplify(bool learned = true);
+        void asymmetric_branching();
+        unsigned scc_bin();
+
+        // -----------------------
+        //
+        // Activity related stuff
+        //
+        // -----------------------
+    public:
+        void inc_activity(bool_var v) {
+            unsigned & act = m_activity[v];
+            act += m_activity_inc;
+            m_case_split_queue.activity_increased_eh(v);
+            if (act > (1 << 24))
+                rescale_activity();
+        }
+
+        void decay_activity() {
+            m_activity_inc *= 11;
+            m_activity_inc /= 10;
+        }
+
+    private:
+        void rescale_activity();
+
+        // -----------------------
+        //
+        // Iterators
+        //
+        // -----------------------
+    public:
+        clause * const * begin_clauses() const { return m_clauses.begin(); }
+        clause * const * end_clauses() const { return m_clauses.end(); }
+        clause * const * begin_learned() const { return m_learned.begin(); }
+        clause * const * end_learned() const { return m_learned.end(); }
+        typedef std::pair<literal, literal> bin_clause;
+        void collect_bin_clauses(svector<bin_clause> & r, bool learned) const;
+
+        // -----------------------
+        //
+        // Debugging
+        //
+        // -----------------------
+    public:
+        bool check_invariant() const;
+        void display(std::ostream & out) const;
+        void display_watches(std::ostream & out) const;
+        void display_dimacs(std::ostream & out) const;
+
+    protected:
+        void display_binary(std::ostream & out) const;
+        void display_units(std::ostream & out) const;
+        void display_assignment(std::ostream & out) const;
+        unsigned num_clauses() const;
+        bool is_unit(clause const & c) const;
+        bool is_empty(clause const & c) const;
+        bool check_missed_propagation(clause_vector const & cs) const;
+        bool check_missed_propagation() const;
+        bool check_marks() const;
+    };
+    
+    struct mk_stat {
+        solver const & m_solver;
+        mk_stat(solver const & s):m_solver(s) {}
+        void display(std::ostream & out) const;
+    };
+
+    std::ostream & operator<<(std::ostream & out, mk_stat const & stat);
+};
+
+#endif

src/sat/sat_types.h

@@ -0,0 +1,237 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_types.h
+
+Abstract:
+
+    Basic types used in the SAT solver
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+Revision History:
+
+--*/
+#ifndef _SAT_TYPES_H_
+#define _SAT_TYPES_H_
+
+#include"debug.h"
+#include"approx_set.h"
+#include"lbool.h"
+#include"tactic_exception.h"
+#include"vector.h"
+#include<iomanip>
+
+namespace sat {
+#define SAT_VB_LVL 10
+
+    // TODO: there is some duplication in the sat and smt namespaces.
+    // The sat namespace should be the base.
+    // I should cleanup the smt namespace later.
+
+    /**
+       \brief A boolean variable is just an integer.
+    */
+    typedef unsigned bool_var;
+
+    typedef svector<bool_var> bool_var_vector;
+    
+    const bool_var null_bool_var  = UINT_MAX >> 1;
+    
+    /**
+       \brief The literal b is represented by the value 2*b, and
+       the literal (not b) by the value 2*b + 1
+    */
+    class literal {
+        unsigned  m_val;
+        explicit literal(unsigned v):m_val(v) {}
+    public:
+        literal():m_val(null_bool_var << 1) {
+            SASSERT(var() == null_bool_var && !sign());
+        }
+        
+        literal(bool_var v, bool _sign):
+            m_val((v << 1) + static_cast<unsigned>(_sign)) {
+            SASSERT(var() == v);
+            SASSERT(sign() == _sign);
+        }
+        
+        bool_var var() const { 
+            return m_val >> 1; 
+        }
+        
+        bool sign() const {
+            return m_val & 1; 
+        }
+
+        literal unsign() const {
+            return literal(m_val & ~1);
+        }
+         
+        unsigned index() const {
+            return m_val;
+        }
+        
+        void neg() {
+            m_val = m_val ^ 1;
+        }
+        
+        friend literal operator~(literal l) {
+            return literal(l.m_val ^ 1);
+        }
+
+        unsigned to_uint() const { return m_val; }
+
+        unsigned hash() const { return to_uint(); }
+
+        friend literal to_literal(unsigned x);
+        friend bool operator<(literal const & l1, literal const & l2);
+        friend bool operator==(literal const & l1, literal const & l2);
+        friend bool operator!=(literal const & l1, literal const & l2);
+    };
+
+    const literal null_literal;
+
+    inline literal to_literal(unsigned x) { return literal(x); }
+    inline bool operator<(literal const & l1, literal const & l2) { return l1.m_val < l2.m_val;  }
+    inline bool operator==(literal const & l1, literal const & l2) { return l1.m_val == l2.m_val; }
+    inline bool operator!=(literal const & l1, literal const & l2) { return l1.m_val != l2.m_val; }
+
+    inline std::ostream & operator<<(std::ostream & out, literal l) { out << (l.sign() ? "-" : "") << l.var(); return out; }
+
+    typedef svector<literal> literal_vector;
+
+    typedef unsigned clause_offset;
+    typedef unsigned ext_constraint_idx;
+    typedef unsigned ext_justification_idx;
+
+    struct literal2unsigned { unsigned operator()(literal l) const { return l.to_uint(); } };
+
+    typedef approx_set_tpl<literal, literal2unsigned, unsigned> literal_approx_set;
+
+    typedef approx_set_tpl<bool_var, u2u, unsigned> var_approx_set;
+   
+    enum phase {
+        POS_PHASE, NEG_PHASE, PHASE_NOT_AVAILABLE
+    };
+
+    class solver;
+    class clause;
+    class clause_wrapper;
+    class integrity_checker;
+    typedef ptr_vector<clause> clause_vector;
+
+    class solver_exception : public tactic_exception {
+    public:                                                
+        solver_exception(char const * msg):tactic_exception(msg) {}
+    };
+
+    typedef default_exception sat_param_exception;
+
+    typedef svector<lbool> model;
+
+    inline lbool value_at(bool_var v, model const & m) { return m[v]; }
+    inline lbool value_at(literal l, model const & m) { lbool r = value_at(l.var(), m); return l.sign() ? ~r : r; }
+    
+    inline std::ostream & operator<<(std::ostream & out, model const & m) {
+        bool first = true;
+        for (bool_var v = 0; v < m.size(); v++) {
+            if (m[v] == l_undef) continue;
+            if (first) first = false; else out << " ";
+            if (m[v] == l_true) out << v; else out << "-" << v;
+        }
+        return out;
+    }
+
+    class uint_set {
+        svector<char>        m_in_set;
+        svector<unsigned>    m_set;
+    public:
+        typedef svector<unsigned>::const_iterator iterator;
+        void insert(unsigned v) { 
+            m_in_set.reserve(v+1, false);
+            if (m_in_set[v]) 
+                return; 
+            m_in_set[v] = true; 
+            m_set.push_back(v); 
+        }
+        
+        bool contains(unsigned v) const { 
+            return v < m_in_set.size() && m_in_set[v] != 0; 
+        }
+        
+        bool empty() const { 
+            return m_set.empty(); 
+        }
+
+        // erase some variable from the set
+        unsigned erase() { 
+            SASSERT(!empty()); 
+            unsigned v = m_set.back(); 
+            m_set.pop_back(); 
+            m_in_set[v] = false; 
+            return v; 
+        }
+        iterator begin() const { return m_set.begin(); }
+        iterator end() const { return m_set.end(); }
+        void reset() { m_set.reset(); m_in_set.reset(); }
+        void cleanup() { m_set.finalize(); m_in_set.finalize(); }
+    };
+
+    typedef uint_set bool_var_set;
+
+    class literal_set {
+        uint_set m_set;
+    public:
+        void insert(literal l) { m_set.insert(l.index()); }
+        bool contains(literal l) const { return m_set.contains(l.index()); }
+        bool empty() const { return m_set.empty(); }
+        void reset() { m_set.reset(); }
+        void cleanup() { m_set.cleanup(); }
+    };
+    
+    struct mem_stat {
+    };
+    
+    inline std::ostream & operator<<(std::ostream & out, mem_stat const & m) {
+        double mem = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
+        out << " :memory " << std::fixed << std::setprecision(2) << mem;
+        return out;
+    }
+
+    struct dimacs_lit {
+        literal m_lit;
+        dimacs_lit(literal l):m_lit(l) {}
+    };
+
+    inline std::ostream & operator<<(std::ostream & out, dimacs_lit const & dl) {
+        literal l = dl.m_lit;
+        if (l.sign()) out << "-" << (l.var() + 1);
+        else out << (l.var() + 1);
+        return out;
+    }
+
+    struct mk_lits_pp {
+        unsigned        m_num;
+        literal const * m_lits;
+        mk_lits_pp(unsigned num, literal const * ls):m_num(num), m_lits(ls) {}
+    };
+
+    inline std::ostream & operator<<(std::ostream & out, mk_lits_pp const & ls) {
+        for (unsigned i = 0; i < ls.m_num; i++) {
+            if (i > 0) out << " ";
+            out << ls.m_lits[i];
+        }
+        return out;
+    }
+
+    inline std::ostream & operator<<(std::ostream & out, literal_vector const & ls) {
+        return out << mk_lits_pp(ls.size(), ls.c_ptr());
+    }
+};
+
+#endif

src/sat/sat_var_queue.h

@@ -0,0 +1,67 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_var_queue.h
+
+Abstract:
+
+    SAT variable priority queue.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+Revision History:
+
+--*/
+#ifndef _SAT_VAR_QUEUE_H_
+#define _SAT_VAR_QUEUE_H_
+
+#include"heap.h"
+#include"sat_types.h"
+
+namespace sat {
+    
+    class var_queue {
+        struct lt {
+            svector<unsigned> & m_activity;
+            lt(svector<unsigned> & act):m_activity(act) {}
+            bool operator()(bool_var v1, bool_var v2) const { return m_activity[v1] > m_activity[v2]; }
+        };
+        heap<lt>  m_queue;
+    public:
+        var_queue(svector<unsigned> & act):m_queue(128, lt(act)) {}
+        
+        void activity_increased_eh(bool_var v) {
+            if (m_queue.contains(v))
+                m_queue.decreased(v);
+        }
+
+        void mk_var_eh(bool_var v) {
+            m_queue.reserve(v+1);
+            m_queue.insert(v);
+        }
+
+        void del_var_eh(bool_var v) {
+            if (m_queue.contains(v))
+                m_queue.erase(v);
+        }
+
+        void unassign_var_eh(bool_var v) {
+            if (!m_queue.contains(v))
+                m_queue.insert(v);
+        }
+
+        void reset() {
+            m_queue.reset();
+        }
+
+        bool empty() const { return m_queue.empty(); }
+
+        bool_var next_var() { SASSERT(!empty()); return m_queue.erase_min(); }
+    };
+};
+
+#endif

src/sat/sat_watched.cpp

@@ -0,0 +1,71 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_watched.cpp
+
+Abstract:
+
+    Element of the SAT solver watchlist.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-24.
+
+Revision History:
+
+--*/
+#include"sat_watched.h"
+#include"sat_clause.h"
+
+namespace sat {
+
+    bool erase_clause_watch(watch_list & wlist, clause_offset c) {
+        watch_list::iterator it  = wlist.begin();              
+        watch_list::iterator end = wlist.end();                
+        for (; it != end; ++it) {                              
+            if (it->is_clause() && it->get_clause_offset() == c) {                                        
+                watch_list::iterator it2 = it;                 
+                ++it;                                          
+                for (; it != end; ++it) {                      
+                    *it2 = *it;                                
+                    ++it2;
+                }                    
+                wlist.set_end(it2);
+                return true;                                  
+            }                                                  
+        }                                                      
+        return false;                                           
+    }
+
+    void display(std::ostream & out, clause_allocator const & ca, watch_list const & wlist) {
+        watch_list::const_iterator it  = wlist.begin();
+        watch_list::const_iterator end = wlist.end();
+        for (bool first = true; it != end; ++it) {
+            if (first)
+                first = false;
+            else
+                out << " ";
+            switch (it->get_kind()) {
+            case watched::BINARY:
+                out << it->get_literal();
+                if (it->is_learned())
+                    out << "*";
+                break;
+            case watched::TERNARY:
+                out << "(" << it->get_literal1() << " " << it->get_literal2() << ")";
+                break;
+            case watched::CLAUSE:
+                out << "(" << it->get_blocked_literal() << " " << *(ca.get_clause(it->get_clause_offset())) << ")";
+                break;
+            case watched::EXT_CONSTRAINT:
+                out << it->get_ext_constraint_idx();
+                break;
+            default: 
+                UNREACHABLE();
+            }
+        }
+    }
+
+};

src/sat/sat_watched.h

@@ -0,0 +1,136 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_watched.h
+
+Abstract:
+
+    Element of the SAT solver watchlist.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+Revision History:
+
+--*/
+#ifndef _SAT_WATCHED_H_
+#define _SAT_WATCHED_H_
+
+#include"sat_types.h"
+#include"vector.h"
+
+namespace sat {
+    /**
+       A watched element can be:
+       
+       1) A literal:               for watched binary clauses
+       2) A pair of literals:      for watched ternary clauses
+       3) A pair (literal, clause-offset): for watched clauses, where the first element of the pair is a literal of the clause.
+       4) A external constraint-idx: for external constraints.
+
+       For binary clauses: we use a bit to store whether the binary clause was learned or not.
+       
+       Remark: there is not Clause object for binary clauses.
+    */
+    class watched {
+    public:
+        enum kind {
+            BINARY = 0, TERNARY, CLAUSE, EXT_CONSTRAINT
+        };
+    private:
+        unsigned m_val1;
+        unsigned m_val2; 
+    public:
+        watched(literal l, bool learned):
+            m_val1(l.to_uint()),
+            m_val2(static_cast<unsigned>(BINARY) + (static_cast<unsigned>(learned) << 2)) {
+            SASSERT(is_binary_clause());
+            SASSERT(get_literal() == l);
+            SASSERT(is_learned() == learned);
+            SASSERT(learned || is_binary_non_learned_clause());
+        }
+
+        watched(literal l1, literal l2) {
+            SASSERT(l1 != l2);
+            if (l1.index() > l2.index())
+                std::swap(l1, l2);
+            m_val1 = l1.to_uint();
+            m_val2 = static_cast<unsigned>(TERNARY) + (l2.to_uint() << 2);
+            SASSERT(is_ternary_clause());
+            SASSERT(get_literal1() == l1);
+            SASSERT(get_literal2() == l2);
+        }
+
+        watched(literal blocked_lit, clause_offset cls_off):
+            m_val1(cls_off), 
+            m_val2(static_cast<unsigned>(CLAUSE) + (blocked_lit.to_uint() << 2)) {
+            SASSERT(is_clause());
+            SASSERT(get_blocked_literal() == blocked_lit);
+            SASSERT(get_clause_offset() == cls_off);
+        }
+
+        watched(ext_constraint_idx cnstr_idx):
+            m_val1(cnstr_idx),
+            m_val2(static_cast<unsigned>(EXT_CONSTRAINT)) {
+            SASSERT(is_ext_constraint());
+            SASSERT(get_ext_constraint_idx() == cnstr_idx);
+        }
+
+        kind get_kind() const { return static_cast<kind>(m_val2 & 3); }
+       
+        bool is_binary_clause() const { return get_kind() == BINARY; }
+        literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(m_val1); }
+        void set_literal(literal l) { SASSERT(is_binary_clause()); m_val1 = l.to_uint(); }
+        bool is_learned() const { SASSERT(is_binary_clause()); return (m_val2 >> 2) == 1; }
+        bool is_binary_non_learned_clause() const { return m_val2 == 0; }
+        void mark_not_learned() { SASSERT(is_learned()); m_val2 = static_cast<unsigned>(BINARY); SASSERT(!is_learned()); }
+        
+        bool is_ternary_clause() const { return get_kind() == TERNARY; }
+        literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(m_val1); }
+        literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 2); }
+
+        bool is_clause() const { return get_kind() == CLAUSE; }
+        clause_offset get_clause_offset() const { SASSERT(is_clause()); return m_val1; }
+        literal get_blocked_literal() const { SASSERT(is_clause()); return to_literal(m_val2 >> 2); }
+        void set_clause_offset(clause_offset c) { SASSERT(is_clause()); m_val1 = c; }
+        void set_blocked_literal(literal l) { SASSERT(is_clause()); m_val2 = static_cast<unsigned>(CLAUSE) + (l.to_uint() << 2); }
+        void set_clause(literal blocked_lit, clause_offset cls_off) {
+            m_val1 = cls_off;
+            m_val2 = static_cast<unsigned>(CLAUSE) + (blocked_lit.to_uint() << 2);
+        }
+
+        bool is_ext_constraint() const { return get_kind() == EXT_CONSTRAINT; }
+        ext_constraint_idx get_ext_constraint_idx() const { SASSERT(is_ext_constraint()); return m_val2; }
+        
+        bool operator==(watched const & w) const { return m_val1 == w.m_val1 && m_val2 == w.m_val2; }
+        bool operator!=(watched const & w) const { return !operator==(w); }
+    };
+
+    COMPILE_TIME_ASSERT(0 <= watched::BINARY && watched::BINARY <= 3);
+    COMPILE_TIME_ASSERT(0 <= watched::TERNARY && watched::TERNARY <= 3);
+    COMPILE_TIME_ASSERT(0 <= watched::CLAUSE && watched::CLAUSE <= 3);
+    COMPILE_TIME_ASSERT(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3);
+
+    struct watched_lt {
+        bool operator()(watched const & w1, watched const & w2) const {
+            if (w2.is_binary_clause()) return false;
+            if (w1.is_binary_clause()) return true;
+            if (w2.is_ternary_clause()) return false;
+            if (w1.is_ternary_clause()) return true;
+            return false;
+        }
+    };
+
+    typedef vector<watched> watch_list;
+
+    bool erase_clause_watch(watch_list & wlist, clause_offset c);
+    inline void erase_ternary_watch(watch_list & wlist, literal l1, literal l2) { wlist.erase(watched(l1, l2)); }
+
+    class clause_allocator;
+    void display(std::ostream & out, clause_allocator const & ca, watch_list const & wlist);
+};
+
+#endif