Initial KLEE checkin.

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


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

1 files changed, 811 insertions, 0 deletions

diff --git a/stp/sat/Solver.C b/stp/sat/Solver.C
new file mode 100644
index 00000000..0fcb6149
--- /dev/null
+++ b/stp/sat/Solver.C
@@ -0,0 +1,811 @@
+/****************************************************************************************[Solver.C]
+MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#include "Solver.h"
+#include "Sort.h"
+#include <cmath>
+
+namespace MINISAT {
+//=================================================================================================
+// Operations on clauses:
+
+
+/*_________________________________________________________________________________________________
+|
+|  newClause : (ps : const vec<Lit>&) (learnt : bool)  ->  [void]
+|  
+|  Description:
+|    Allocate and add a new clause to the SAT solvers clause database. 
+|  
+|  Input:
+|    ps     - The new clause as a vector of literals.
+|    learnt - Is the clause a learnt clause? For learnt clauses, 'ps[0]' is assumed to be the
+|             asserting literal. An appropriate 'enqueue()' operation will be performed on this
+|             literal. One of the watches will always be on this literal, the other will be set to
+|             the literal with the highest decision level.
+|  
+|  Effect:
+|    Activity heuristics are updated.
+|________________________________________________________________________________________________@*/
+bool Solver::newClause(const vec<Lit>& ps_, bool learnt, bool normalized)
+{
+    vec<Lit>    qs;
+    if (!learnt && !normalized){
+        assert(decisionLevel() == 0);
+        ps_.copyTo(qs);             // Make a copy of the input vector.
+
+        // Remove duplicates:
+        sortUnique(qs);
+
+        // Check if clause is satisfied:
+        for (int i = 0; i < qs.size()-1; i++){
+            if (qs[i] == ~qs[i+1])
+                return true; }
+        for (int i = 0; i < qs.size(); i++){
+            if (value(qs[i]) == l_True)
+                return true; }
+
+        // Remove false literals:
+        int     i, j;
+        for (i = j = 0; i < qs.size(); i++)
+            if (value(qs[i]) != l_False)
+                qs[j++] = qs[i];
+        qs.shrink(i - j);
+    }
+    const vec<Lit>& ps = learnt || normalized ? ps_ : qs;     // 'ps' is now the (possibly) reduced vector of literals.
+
+    if (ps.size() == 0)
+        return false;
+    else if (ps.size() == 1){
+        assert(decisionLevel() == 0);
+        return enqueue(ps[0]);
+    }else{
+        // Allocate clause:
+        Clause* c   = Clause_new(ps, learnt);
+
+        if (learnt){
+            // Put the second watch on the first literal with highest decision level:
+            // (requires that this method is called at the level where the clause is asserting!)
+            int i;
+            for (i = 1; i < ps.size() && position(trailpos[var(ps[i])]) < trail_lim.last(); i++)
+                ;
+            (*c)[1] = ps[i];
+            (*c)[i] = ps[1];
+
+            // Bump, enqueue, store clause:
+            claBumpActivity(*c);        // (newly learnt clauses should be considered active)
+            check(enqueue((*c)[0], c));
+            learnts.push(c);
+            stats.learnts_literals += c->size();
+        }else{
+            // Store clause:
+            clauses.push(c);
+            stats.clauses_literals += c->size();
+
+            if (subsumption){
+                c->calcAbstraction();
+                for (int i = 0; i < c->size(); i++){
+                    assert(!find(occurs[var((*c)[i])], c));
+                    occurs[var((*c)[i])].push(c);
+                    n_occ[toInt((*c)[i])]++;
+                    touched[var((*c)[i])] = 1;
+
+                    if (heap.inHeap(var((*c)[i])))
+		      updateHeap(var((*c)[i]));
+                }
+            }
+
+        }
+        // Watch clause:
+        watches[toInt(~(*c)[0])].push(c);
+        watches[toInt(~(*c)[1])].push(c);
+    }
+
+    return true;
+}
+
+
+// Disposes a clauses and removes it from watcher lists. NOTE!
+// Low-level; does NOT change the 'clauses' and 'learnts' vector.
+//
+void Solver::removeClause(Clause& c, bool dealloc)
+{
+    //fprintf(stderr, "delete %d: ", _c); printClause(c); fprintf(stderr, "\n");
+    assert(c.mark() == 0);
+
+    if (c.size() > 1){
+        assert(find(watches[toInt(~c[0])], &c));
+        assert(find(watches[toInt(~c[1])], &c));
+        remove(watches[toInt(~c[0])], &c);
+        remove(watches[toInt(~c[1])], &c); }
+
+    if (c.learnt()) stats.learnts_literals -= c.size();
+    else            stats.clauses_literals -= c.size();
+
+    if (subsumption && !c.learnt()){
+        for (int i = 0; i < c.size(); i++){
+            if (dealloc){
+                assert(find(occurs[var(c[i])], &c));
+                remove(occurs[var(c[i])], &c); 
+            }
+            n_occ[toInt(c[i])]--;
+            updateHeap(var(c[i]));
+        }
+    }
+
+    if (dealloc)
+        xfree(&c);
+    else
+        c.mark(1);
+}
+
+
+bool Solver::satisfied(Clause& c) const
+{
+    for (int i = 0; i < c.size(); i++)
+        if (value(c[i]) == l_True)
+            return true;
+    return false; }
+
+
+bool Solver::strengthen(Clause& c, Lit l)
+{
+    assert(decisionLevel() == 0);
+    assert(c.size() > 1);
+    assert(c.mark() == 0);
+
+    assert(toInt(~c[0]) < watches.size());
+    assert(toInt(~c[1]) < watches.size());
+    
+    assert(find(watches[toInt(~c[0])], &c));
+    assert(find(watches[toInt(~c[1])], &c));
+    assert(find(c,l));
+
+    if (c.learnt()) stats.learnts_literals -= 1;
+    else            stats.clauses_literals -= 1;
+
+    if (c[0] == l || c[1] == l){
+        assert(find(watches[toInt(~l)], &c));
+        remove(c,l);
+        remove(watches[toInt(~l)], &c);
+        if (c.size() > 1){
+            assert(!find(watches[toInt(~c[1])], &c));
+            watches[toInt(~c[1])].push(&c); }
+        else {
+            assert(find(watches[toInt(~c[0])], &c));
+            remove(watches[toInt(~c[0])], &c);
+            removeClause(c, false);
+        }
+    }
+    else
+        remove(c,l);
+        
+    assert(c.size() == 1 || find(watches[toInt(~c[0])], &c));
+    assert(c.size() == 1 || find(watches[toInt(~c[1])], &c));
+
+    if (subsumption){
+        assert(find(occurs[var(l)], &c));
+        remove(occurs[var(l)], &c);
+        assert(!find(occurs[var(l)], &c));
+
+        c.calcAbstraction();
+
+        n_occ[toInt(l)]--;
+        updateHeap(var(l));
+    }
+
+    return c.size() == 1 ? enqueue(c[0]) : true;
+}
+
+
+//=================================================================================================
+// Minor methods:
+
+
+// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be
+// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
+//
+Var Solver::newVar(bool polarity, bool dvar) {
+    int     index;
+    index = nVars();
+    watches     .push();          // (list for positive literal)
+    watches     .push();          // (list for negative literal)
+    reason      .push(NULL);
+    assigns     .push(toInt(l_Undef));
+    trailpos    .push(TrailPos(0,0));
+    activity    .push(0);
+    order       .newVar(polarity,dvar);
+    seen        .push(0);
+    touched     .push(0);
+    if (subsumption){
+        occurs  .push();
+        n_occ   .push(0);
+        n_occ   .push(0);
+        heap    .setBounds(index+1);
+    }
+    return index; }
+
+
+// Returns FALSE if immediate conflict.
+bool Solver::assume(Lit p) {
+    trail_lim.push(trail.size());
+    return enqueue(p); }
+
+
+// Revert to the state at given level.
+void Solver::cancelUntil(int level) {
+    if (decisionLevel() > level){
+        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
+            Var     x  = var(trail[c]);
+            assigns[x] = toInt(l_Undef);
+            reason [x] = NULL; 
+            order.undo(x); }
+        qhead = trail_lim[level];
+        trail.shrink(trail.size() - trail_lim[level]);
+        trail_lim.shrink(trail_lim.size() - level);
+    }
+}
+
+
+//=================================================================================================
+// Major methods:
+
+
+/*_________________________________________________________________________________________________
+|
+|  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->  [void]
+|  
+|  Description:
+|    Analyze conflict and produce a reason clause.
+|  
+|    Pre-conditions:
+|      * 'out_learnt' is assumed to be cleared.
+|      * Current decision level must be greater than root level.
+|  
+|    Post-conditions:
+|      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
+|  
+|  Effect:
+|    Will undo part of the trail, upto but not beyond the assumption of the current decision level.
+|________________________________________________________________________________________________@*/
+void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
+{
+    int            pathC = 0;
+    int            btpos = -1;
+    Lit            p     = lit_Undef;
+
+    // Generate conflict clause:
+    //
+    out_learnt.push();      // (leave room for the asserting literal)
+    int index = trail.size()-1;
+    do{
+        assert(confl != NULL);          // (otherwise should be UIP)
+        Clause& c = *confl;
+
+        if (c.learnt())
+            claBumpActivity(c);
+
+        for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
+            Lit q = c[j];
+            if (!seen[var(q)] && position(trailpos[var(q)]) >= trail_lim[0]){
+	      varBumpActivity(q);
+                seen[var(q)] = 1;
+                if (position(trailpos[var(q)]) >= trail_lim.last())
+                    pathC++;
+                else{
+                    out_learnt.push(q);
+                    btpos = max(btpos, position(trailpos[var(q)]));
+                }
+            }
+        }
+
+        // Select next clause to look at:
+        while (!seen[var(trail[index--])]);
+        p     = trail[index+1];
+        confl = reason[var(p)];
+        seen[var(p)] = 0;
+        pathC--;
+
+    }while (pathC > 0);
+    out_learnt[0] = ~p;
+
+    // Find correct backtrack level
+    for (out_btlevel = trail_lim.size()-1; out_btlevel > 0 && trail_lim[out_btlevel-1] > btpos; out_btlevel--)
+        ;
+
+    int     i, j;
+    if (expensive_ccmin){
+        // Simplify conflict clause (a lot):
+        //
+        uint    min_level = 0;
+        for (i = 1; i < out_learnt.size(); i++)
+            min_level |= abstractLevel(trailpos[var(out_learnt[i])]);     // (maintain an abstraction of levels involved in conflict)
+
+        out_learnt.copyTo(analyze_toclear);
+        for (i = j = 1; i < out_learnt.size(); i++)
+            if (reason[var(out_learnt[i])] == NULL || !analyze_removable(out_learnt[i], min_level))
+                out_learnt[j++] = out_learnt[i];
+    }else{
+        // Simplify conflict clause (a little):
+        //
+        out_learnt.copyTo(analyze_toclear);
+        for (i = j = 1; i < out_learnt.size(); i++){
+            Clause& c = *reason[var(out_learnt[i])];
+            for (int k = 1; k < c.size(); k++)
+                if (!seen[var(c[k])] && position(trailpos[var(c[k])]) >= trail_lim[0]){
+                    out_learnt[j++] = out_learnt[i];
+                    break; }
+        }
+    }
+
+    stats.max_literals += out_learnt.size();
+    out_learnt.shrink(i - j);
+    stats.tot_literals += out_learnt.size();
+
+    for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
+}
+
+
+// Check if 'p' can be removed. 'min_level' is used to abort early if visiting literals at a level that cannot be removed.
+//
+bool Solver::analyze_removable(Lit p, uint min_level)
+{
+    analyze_stack.clear(); analyze_stack.push(p);
+    int top = analyze_toclear.size();
+    while (analyze_stack.size() > 0){
+        assert(reason[var(analyze_stack.last())] != NULL);
+        Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop();
+
+        for (int i = 1; i < c.size(); i++){
+            Lit      p   = c[i];
+            TrailPos tp = trailpos[var(p)];
+            if (!seen[var(p)] && position(tp) >= trail_lim[0]){
+                if (reason[var(p)] != NULL && (abstractLevel(tp) & min_level) != 0){
+                    seen[var(p)] = 1;
+                    analyze_stack.push(p);
+                    analyze_toclear.push(p);
+                }else{
+                    for (int j = top; j < analyze_toclear.size(); j++)
+                        seen[var(analyze_toclear[j])] = 0;
+                    analyze_toclear.shrink(analyze_toclear.size() - top);
+                    return false;
+                }
+            }
+        }
+    }
+
+    return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  analyzeFinal : (p : Lit) ->  [void]
+|  
+|  Description:
+|    Specialized analysis procedure to express the final conflict in terms of assumptions.
+|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
+|    stores the result in 'out_conflict'.
+|________________________________________________________________________________________________@*/
+void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
+{
+    out_conflict.clear();
+    out_conflict.push(p);
+
+    if (decisionLevel() == 0)
+        return;
+
+    seen[var(p)] = 1;
+
+    int start = position(trailpos[var(p)]);
+    for (int i = start; i >= trail_lim[0]; i--){
+        Var     x = var(trail[i]);
+        if (seen[x]){
+            if (reason[x] == NULL){
+                assert(position(trailpos[x]) >= trail_lim[0]);
+                out_conflict.push(~trail[i]);
+            }else{
+                Clause& c = *reason[x];
+                for (int j = 1; j < c.size(); j++)
+                    if (position(trailpos[var(c[j])]) >= trail_lim[0])
+                        seen[var(c[j])] = 1;
+            }
+            seen[x] = 0;
+        }
+    }
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  enqueue : (p : Lit) (from : Clause*)  ->  [bool]
+|  
+|  Description:
+|    Puts a new fact on the propagation queue as well as immediately updating the variable's value.
+|    Should a conflict arise, FALSE is returned.
+|  
+|  Input:
+|    p    - The fact to enqueue
+|    from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'.
+|           Default value is NULL (no reason).
+|  
+|  Output:
+|    TRUE if fact was enqueued without conflict, FALSE otherwise.
+|________________________________________________________________________________________________@*/
+bool Solver::enqueue(Lit p, Clause* from)
+{
+
+    if (value(p) != l_Undef)
+        return value(p) != l_False;
+    else{
+        assigns [var(p)] = toInt(lbool(!sign(p)));
+        trailpos[var(p)] = TrailPos(trail.size(),decisionLevel());
+        reason  [var(p)] = from;
+        trail.push(p);
+        return true;
+    }
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  propagate : [void]  ->  [Clause*]
+|  
+|  Description:
+|    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
+|    otherwise NULL.
+|  
+|    Post-conditions:
+|      * the propagation queue is empty, even if there was a conflict.
+|________________________________________________________________________________________________@*/
+Clause* Solver::propagate()
+{
+    if (decisionLevel() == 0 && subsumption)
+        return backwardSubsumptionCheck() ? NULL : propagate_tmpempty;
+
+    Clause* confl = NULL;
+    //fprintf(stderr, "propagate, qhead = %d, qtail = %d\n", qhead, qtail);
+    while (qhead < trail.size()){
+        stats.propagations++;
+        simpDB_props--;
+
+        Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
+        vec<Clause*>&  ws  = watches[toInt(p)];
+        Clause         **i, **j, **end;
+
+        for (i = j = (Clause**)ws, end = i + ws.size();  i != end;){
+            Clause& c = **i++;
+            
+            // Make sure the false literal is data[1]:
+            Lit false_lit = ~p;
+            if (c[0] == false_lit)
+                c[0] = c[1], c[1] = false_lit;
+
+            assert(c[1] == false_lit);
+
+            // If 0th watch is true, then clause is already satisfied.
+            Lit first = c[0];
+            if (value(first) == l_True){
+                *j++ = &c;
+            }else{
+                // Look for new watch:
+                for (int k = 2; k < c.size(); k++)
+                    if (value(c[k]) != l_False){
+                        c[1] = c[k]; c[k] = false_lit;
+                        watches[toInt(~c[1])].push(&c);
+                        goto FoundWatch; }
+
+                // Did not find watch -- clause is unit under assignment:
+                *j++ = &c;
+                if (!enqueue(first, &c)){
+                    confl = &c;
+                    qhead = trail.size();
+                    // Copy the remaining watches:
+                    while (i < end)
+                        *j++ = *i++;
+                }
+            FoundWatch:;
+            }
+        }
+        ws.shrink(i - j);
+    }
+
+    return confl;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  reduceDB : ()  ->  [void]
+|  
+|  Description:
+|    Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
+|    clauses are clauses that are reason to some assignment. Binary clauses are never removed.
+|________________________________________________________________________________________________@*/
+struct reduceDB_lt { bool operator () (Clause* x, Clause* y) { return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity()); } };
+void Solver::reduceDB()
+{
+    int     i, j;
+    double  extra_lim = cla_inc / learnts.size();    // Remove any clause below this activity
+
+    sort(learnts, reduceDB_lt());
+    for (i = j = 0; i < learnts.size() / 2; i++){
+        if (learnts[i]->size() > 2 && !locked(*learnts[i]))
+            removeClause(*learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    for (; i < learnts.size(); i++){
+        if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() < extra_lim)
+            removeClause(*learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    learnts.shrink(i - j);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  simplifyDB : [void]  ->  [bool]
+|  
+|  Description:
+|    Simplify the clause database according to the current top-level assigment. Currently, the only
+|    thing done here is the removal of satisfied clauses, but more things can be put here.
+|________________________________________________________________________________________________@*/
+bool Solver::simplifyDB(bool expensive)
+{
+    assert(decisionLevel() == 0);
+    if (!ok || propagate() != NULL)
+        return ok = false;
+
+    if (nAssigns() == simpDB_assigns || 
+        (!subsumption && simpDB_props > 0)) // (nothing has changed or preformed a simplification too recently)
+        return true;
+
+    if (subsumption){
+        if (expensive && !eliminate())
+            return ok = false;
+
+        // Move this cleanup code to its own method ?
+        int      i , j;
+        vec<Var> dirty;
+        for (i = 0; i < clauses.size(); i++)
+            if (clauses[i]->mark() == 1){
+                Clause& c = *clauses[i];
+                for (int k = 0; k < c.size(); k++)
+                    if (!seen[var(c[k])]){
+                        seen[var(c[k])] = 1;
+                        dirty.push(var(c[k]));
+                    }
+            }
+        
+        for (i = 0; i < dirty.size(); i++){
+            cleanOcc(dirty[i]);
+            seen[dirty[i]] = 0;
+        }
+
+        for (i = j = 0; i < clauses.size(); i++)
+            if (clauses[i]->mark() == 1)
+                xfree(clauses[i]);
+            else
+                clauses[j++] = clauses[i];
+        clauses.shrink(i - j);
+    }
+
+    // Remove satisfied clauses:
+    for (int type = 0; type < (subsumption ? 1 : 2); type++){  // (only scan learnt clauses if subsumption is on)
+        vec<Clause*>& cs = type ? learnts : clauses;
+        int     j  = 0;
+        for (int i = 0; i < cs.size(); i++){
+            assert(cs[i]->mark() == 0);
+            if (satisfied(*cs[i]))
+                removeClause(*cs[i]);
+            else
+                cs[j++] = cs[i];
+        }
+        cs.shrink(cs.size()-j);
+    }
+    order.cleanup();
+
+    simpDB_assigns = nAssigns();
+    simpDB_props   = stats.clauses_literals + stats.learnts_literals;   // (shouldn't depend on 'stats' really, but it will do for now)
+
+    return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&)  ->  [lbool]
+|  
+|  Description:
+|    Search for a model the specified number of conflicts, keeping the number of learnt clauses
+|    below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to
+|    indicate infinity.
+|  
+|  Output:
+|    'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
+|    all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
+|    if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
+|________________________________________________________________________________________________@*/
+lbool Solver::search(int nof_conflicts, int nof_learnts)
+{
+    assert(ok);
+    int         backtrack_level;
+    int         conflictC = 0;
+    vec<Lit>    learnt_clause;
+
+    stats.starts++;
+    var_decay = 1 / params.var_decay;
+    cla_decay = 1 / params.clause_decay;
+
+    for (;;){
+        Clause* confl = propagate();
+        if (confl != NULL){
+            // CONFLICT
+            stats.conflicts++; conflictC++;
+            if (decisionLevel() == 0) return l_False;
+
+            learnt_clause.clear();
+            analyze(confl, learnt_clause, backtrack_level);
+            cancelUntil(backtrack_level);
+            newClause(learnt_clause, true);
+            varDecayActivity();
+            claDecayActivity();
+
+        }else{
+            // NO CONFLICT
+
+            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+                // Reached bound on number of conflicts:
+                progress_estimate = progressEstimate();
+                cancelUntil(0);
+                return l_Undef; }
+
+            // Simplify the set of problem clauses:
+            if (decisionLevel() == 0 && !simplifyDB())
+                return l_False;
+
+            if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts)
+                // Reduce the set of learnt clauses:
+                reduceDB();
+
+            Lit next = lit_Undef;
+
+            if (decisionLevel() < assumptions.size()){
+                // Perform user provided assumption:
+                next = assumptions[decisionLevel()]; 
+                if (value(next) == l_False){
+                    analyzeFinal(~next, conflict);
+                    return l_False; }
+            }else{
+                // New variable decision:
+                stats.decisions++;
+                next = order.select(params.random_var_freq, decisionLevel());		
+	    }
+            if (next == lit_Undef)
+                // Model found:
+                return l_True;
+
+            check(assume(next));
+        }
+    }
+}
+
+
+// Return search-space coverage. Not extremely reliable.
+//
+double Solver::progressEstimate()
+{
+    double  progress = 0;
+    double  F = 1.0 / nVars();
+
+    for (int i = 0; i <= decisionLevel(); i++){
+        int beg = i == 0 ? 0 : trail_lim[i - 1];
+        int end = i == decisionLevel() ? trail.size() : trail_lim[i];
+        progress += pow(F, i) * (end - beg);
+    }
+
+    return progress / nVars();
+}
+
+
+// Divide all variable activities by 1e100.
+//
+void Solver::varRescaleActivity()
+{
+    for (int i = 0; i < nVars(); i++)
+        activity[i] *= 1e-100;
+    var_inc *= 1e-100;
+}
+
+
+// Divide all constraint activities by 1e100.
+//
+void Solver::claRescaleActivity()
+{
+    for (int i = 0; i < learnts.size(); i++)
+        learnts[i]->activity() *= 1e-20;
+    cla_inc *= 1e-20;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  solve : (assumps : const vec<Lit>&)  ->  [bool]
+|  
+|  Description:
+|    Top-level solve.
+|________________________________________________________________________________________________@*/
+bool Solver::solve(const vec<Lit>& assumps)
+{
+    model.clear();
+    conflict.clear();
+
+    if (!simplifyDB(true)) return false;
+
+
+    double  nof_conflicts = params.restart_first;
+    double  nof_learnts   = nClauses() * params.learntsize_factor;
+    lbool   status        = l_Undef;
+    assumps.copyTo(assumptions);
+
+    if (verbosity >= 1){
+        reportf("==================================[MINISAT]====================================\n");
+        reportf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
+        reportf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
+        reportf("===============================================================================\n");
+    }
+
+    // Search:
+    while (status == l_Undef){
+        if (verbosity >= 1)
+            //reportf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100);
+            reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)stats.conflicts, order.size(), nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (double)stats.learnts_literals/nLearnts(), progress_estimate*100);
+        status = search((int)nof_conflicts, (int)nof_learnts);
+        nof_conflicts *= params.restart_inc;
+        nof_learnts   *= params.learntsize_inc;
+    }
+
+    if (verbosity >= 1)
+        reportf("==============================================================================\n");
+
+    if (status == l_True){
+        // Copy model:
+        extendModel();
+#if 1
+        //fprintf(stderr, "Verifying model.\n");
+        for (int i = 0; i < clauses.size(); i++)
+            assert(satisfied(*clauses[i]));
+        for (int i = 0; i < eliminated.size(); i++)
+            assert(satisfied(*eliminated[i]));
+#endif
+        model.growTo(nVars());
+        for (int i = 0; i < nVars(); i++) model[i] = value(i);
+    }else{
+        assert(status == l_False);
+        if (conflict.size() == 0)
+            ok = false;
+    }
+
+    cancelUntil(0);
+    return status == l_True;
+}
+};//end of MINISAT namespace