/*
    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
    * 
    * Based on the original minisat specification from:
    * 
    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
    * Sixth International Conference on Theory and Applications of Satisfiability
    * Testing, LNCS 2919, pp 502-518, 2003.
    * 
   * This library is free software; you can redistribute it and/or modify it under
   * the terms of the GNU Lesser General Public License as published by the Free
   * Software Foundation; either version 2.1 of the License, or (at your option)
   * any later version.
   * 
   * This library is distributed in the hope that it will be useful, but WITHOUT
   * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
   * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
   * details.
   * 
   * You should have received a copy of the GNU Lesser General Public License
   * along with this library; if not, write to the Free Software Foundation, Inc.,
   * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
   * 
   */
  
  package org.sat4j.minisat.core;
  
  import static org.sat4j.minisat.core.LiteralsUtils.neg;
  import static org.sat4j.minisat.core.LiteralsUtils.var;
  
  import java.io.PrintStream;
  import java.io.PrintWriter;
  import java.io.Serializable;
  import java.lang.reflect.Field;
  import java.math.BigInteger;
  import java.util.Comparator;
  import java.util.Map;
  import java.util.Timer;
  import java.util.TimerTask;
  
  import org.sat4j.core.Vec;
  import org.sat4j.core.VecInt;
  import org.sat4j.specs.ContradictionException;
  import org.sat4j.specs.IConstr;
  import org.sat4j.specs.ISolver;
  import org.sat4j.specs.IVec;
  import org.sat4j.specs.IVecInt;
  import org.sat4j.specs.TimeoutException;
  
  /**
   * The backbone of the library providing the modular implementation of a MiniSAT
   * (Chaff) like solver.
   * 
   * @author leberre
   */
  public class Solver<L extends ILits> implements ISolver, UnitPropagationListener,
          ActivityListener, Learner {
  
      private static final long serialVersionUID = 1L;
  
      private static final double CLAUSE_RESCALE_FACTOR = 1e-20;
  
      private static final double CLAUSE_RESCALE_BOUND = 1 / CLAUSE_RESCALE_FACTOR;
  
      /**
       * List des contraintes du probl?me.
       */
      private final IVec<Constr> constrs = new Vec<Constr>(); // Constr
  
      /**
       * Liste des clauses apprises.
       */
      private final IVec<Constr> learnts = new Vec<Constr>(); // Clause
  
      /**
       * incr?ment pour l'activit? des clauses.
       */
      private double claInc = 1.0;
  
      /**
       * decay factor pour l'activit? des clauses.
       */
      private double claDecay = 1.0;
  
      /**
       * Queue de propagation
       */
      // private final IntQueue propQ = new IntQueue(); // Lit
      // head of the queue in trail ... (taken from MiniSAT 1.14)
      private int qhead = 0;
  
      // queue
  
      /**
       * affectation en ordre chronologique
       */
      protected final IVecInt trail = new VecInt(); // lit
  
      // vector
 
     /**
      * indice des s?parateurs des diff?rents niveau de d?cision dans trail
      */
     protected final IVecInt trailLim = new VecInt(); // int
 
     // vector
 
     /**
      * S?pare les hypoth?ses incr?mentale et recherche
      */
     protected int rootLevel;
 
     private int[] model = null;
 
     protected L voc;
 
     private IOrder<L> order;
 
     private final ActivityComparator comparator = new ActivityComparator();
 
     private final SolverStats stats = new SolverStats();
 
     private final LearningStrategy<L> learner;
 
     protected final AssertingClauseGenerator analyzer;
 
     private boolean undertimeout;
 
     private long timeout = Integer.MAX_VALUE;
 
     protected DataStructureFactory<L> dsfactory;
 
     private SearchParams params;
 
     private final IVecInt __dimacs_out = new VecInt();
 
     private SearchListener slistener = new NullSearchListener();
 
     private RestartStrategy restarter;
     
     protected IVecInt dimacs2internal(IVecInt in) {
         if (voc.nVars() == 0) {
             throw new RuntimeException(
                     "Please set the number of variables (solver.newVar() or solver.newVar(maxvar)) before adding constraints!");
         }
         __dimacs_out.clear();
         __dimacs_out.ensure(in.size());
         for (int i = 0; i < in.size(); i++) {
             assert (in.get(i) != 0) && (Math.abs(in.get(i)) <= voc.nVars());
             __dimacs_out.unsafePush(voc.getFromPool(in.get(i)));
         }
         return __dimacs_out;
     }
 
     /**
      * creates a Solver without LearningListener. A learningListener must be
      * added to the solver, else it won't backtrack!!! A data structure factory
      * must be provided, else it won't work either.
      * 
      * @param acg
      *            an asserting clause generator
      */
 
     public Solver(AssertingClauseGenerator acg, LearningStrategy<L> learner,
             DataStructureFactory<L> dsf, IOrder<L> order, RestartStrategy restarter) {
         this(acg, learner, dsf, new SearchParams(), order,restarter);
     }
     
     public Solver(AssertingClauseGenerator acg, LearningStrategy<L> learner,
             DataStructureFactory<L> dsf, SearchParams params, IOrder<L> order, RestartStrategy restarter) {
         analyzer = acg;
         this.learner = learner;
         this.order = order;
         this.params = params;
         setDataStructureFactory(dsf);
         this.restarter = restarter;
     }
 
     /**
      * Change the internal representation of the contraints. Note that the
      * heuristics must be changed prior to calling that method.
      * 
      * @param dsf
      *            the internal factory
      */
     public final void setDataStructureFactory(DataStructureFactory<L> dsf) {
         dsfactory = dsf;
         dsfactory.setUnitPropagationListener(this);
         dsfactory.setLearner(this);
         voc = dsf.getVocabulary();
         order.setLits(voc);
     }
 
     public void setSearchListener(SearchListener sl) {
         slistener = sl;
     }
 
     public void setTimeout(int t) {
         timeout = t*1000L;
     }
 
     public void setTimeoutMs(long t) {
         timeout = t;
     }
     
     public void setSearchParams(SearchParams sp) {
         params = sp;
     }
 
     public void setRestartStrategy(RestartStrategy restarter) {
         this.restarter = restarter;
     }
     
     protected int nAssigns() {
         return trail.size();
     }
 
     public int nConstraints() {
         return constrs.size();
     }
 
     public void learn(Constr c) {
         learnts.push(c);
         c.setLearnt();
         c.register();
         stats.learnedclauses++;
         switch (c.size()) {
         case 2:
             stats.learnedbinaryclauses++;
             break;
         case 3:
             stats.learnedternaryclauses++;
             break;
         default:
             // do nothing
         }
     }
 
     public int decisionLevel() {
         return trailLim.size();
     }
 
     public int newVar() {
         int index = voc.nVars() + 1;
         voc.ensurePool(index);
         mseen = new boolean[index + 1];
         trail.ensure(index);
         trailLim.ensure(index);
         order.newVar();
         return index;
     }
 
     public int newVar(int howmany) {
         voc.ensurePool(howmany);
         order.newVar(howmany);
         mseen = new boolean[howmany + 1];
         trail.ensure(howmany);
         trailLim.ensure(howmany);
         return voc.nVars();
     }
 
     public IConstr addClause(IVecInt literals) throws ContradictionException {
         IVecInt vlits = dimacs2internal(literals);
         return addConstr(dsfactory.createClause(vlits));
     }
 
     public boolean removeConstr(IConstr co) {
         if (co == null) {
             throw new UnsupportedOperationException(
                     "Reference to the constraint to remove needed!"); //$NON-NLS-1$
         }
         Constr c = (Constr) co;
         c.remove();
         constrs.remove(c);
         clearLearntClauses();
         cancelLearntLiterals();
         return true;
     }
 
     public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs,
             boolean moreThan, BigInteger degree) throws ContradictionException {
         IVecInt vlits = dimacs2internal(literals);
         assert vlits.size() == literals.size();
         assert literals.size() == coeffs.size();
         return addConstr(dsfactory.createPseudoBooleanConstraint(vlits, coeffs,
                 moreThan, degree));
     }
 
     public void addAllClauses(IVec<IVecInt> clauses)
             throws ContradictionException {
         for (IVecInt clause : clauses) {
             addClause(clause);
         }
     }
 
     public IConstr addAtMost(IVecInt literals, int degree)
             throws ContradictionException {
         int n = literals.size();
         IVecInt opliterals = new VecInt(n);
         for (int p : literals) {
             opliterals.push(-p);
         }
         return addAtLeast(opliterals, n - degree);
     }
 
     public IConstr addAtLeast(IVecInt literals, int degree)
             throws ContradictionException {
         IVecInt vlits = dimacs2internal(literals);
         return addConstr(dsfactory.createCardinalityConstraint(vlits, degree));
     }
 
     @SuppressWarnings("unchecked")
     public boolean simplifyDB() {
         // aucune raison de recommencer un propagate?
         // if (propagate() != null) {
         // // Un conflit est d?couvert, la base est inconsistante
         // return false;
         // }
 
         // Simplifie la base de clauses apres la premiere propagation des
         // clauses unitaires
         IVec<Constr>[] cs = new IVec[] { constrs, learnts };
         for (int type = 0; type < 2; type++) {
             int j = 0;
             for (int i = 0; i < cs[type].size(); i++) {
                 if (cs[type].get(i).simplify()) {
                     // enleve les contraintes satisfaites de la base
                     cs[type].get(i).remove();
                 } else {
                     cs[type].moveTo(j++, i);
                 }
             }
             cs[type].shrinkTo(j);
         }
         return true;
     }
 
     /**
      * Si un mod?le est trouv?, ce vecteur contient le mod?le.
      * 
      * @return un mod?le de la formule.
      */
     public int[] model() {
         if (model == null) {
             throw new UnsupportedOperationException(
                     "Call the solve method first!!!"); //$NON-NLS-1$
         }
         int[] nmodel = new int[model.length];
         System.arraycopy(model, 0, nmodel, 0, model.length);
         return nmodel;
     }
 
     /**
      * Satisfait un litt?ral
      * 
      * @param p
      *            le litt?ral
      * @return true si tout se passe bien, false si un conflit appara?t.
      */
     public boolean enqueue(int p) {
         return enqueue(p, null);
     }
 
     /**
      * Put the literal on the queue of assignments to be done.
      * 
      * @param p
      *            the literal.
      * @param from
      *            the reason to propagate that literal, else null
      * @return true if the asignment can be made, false if a conflict is
      *         detected.
      */
     public boolean enqueue(int p, Constr from) {
         assert p > 1;
         if (voc.isSatisfied(p)) {
             // literal is already satisfied. Skipping.
             return true;
         }
         if (voc.isFalsified(p)) {
             // conflicting enqueued assignment
             return false;
         }
         // new fact, store it
         voc.satisfies(p);
         voc.setLevel(p, decisionLevel());
         voc.setReason(p, from);
         trail.push(p);
         return true;
     }
 
     private boolean[] mseen = new boolean[0];
 
     private final IVecInt preason = new VecInt();
 
     private final IVecInt outLearnt = new VecInt();
 
     public int analyze(Constr confl, Handle<Constr> outLearntRef) {
         assert confl != null;
         outLearnt.clear();
 
         final boolean[] seen = mseen;
 
         assert outLearnt.size() == 0;
         for (int i = 0; i < seen.length; i++) {
             seen[i] = false;
         }
 
         analyzer.initAnalyze();
         int p = ILits.UNDEFINED;
 
         outLearnt.push(ILits.UNDEFINED);
         // reserve de la place pour le litteral falsifie
         int outBtlevel = 0;
 
         do {
             preason.clear();
             assert confl != null;
             confl.calcReason(p, preason);
             if (confl.learnt())
                 claBumpActivity(confl);
             // Trace reason for p
             for (int j = 0; j < preason.size(); j++) {
                 int q = preason.get(j);
                 order.updateVar(q);
                 if (!seen[q >> 1]) {
                     // order.updateVar(q); // MINISAT
                     seen[q >> 1] = true;
                     if (voc.getLevel(q) == decisionLevel()) {
                         analyzer.onCurrentDecisionLevelLiteral(q);
                     } else if (voc.getLevel(q) > 0) {
                         // ajoute les variables depuis le niveau de d?cision 0
                         outLearnt.push(q ^ 1);
                         outBtlevel = Math.max(outBtlevel, voc.getLevel(q));
                     }
                 }
             }
 
             // select next reason to look at
             do {
                 p = trail.last();
                 // System.err.print((Clause.lastid()+1)+"
                 // "+((Clause)confl).getId()+" ");
                 confl = voc.getReason(p);
                 // System.err.println(((Clause)confl).getId());
                 // assert(confl != null) || counter == 1;
                 undoOne();
             } while (!seen[p >> 1]);
             // seen[p.var] indique que p se trouve dans outLearnt ou dans
             // le dernier niveau de d?cision
         } while (analyzer.clauseNonAssertive(confl));
 
         outLearnt.set(0, p ^ 1);
         simplifier.simplify(outLearnt);
 
         Constr c = dsfactory.createUnregisteredClause(outLearnt);
         slistener.learn(c);
 
         outLearntRef.obj = c;
 
         assert outBtlevel > -1;
         return outBtlevel;
     }
 
     interface ISimplifier extends Serializable {
         void simplify(IVecInt outLearnt);
     }
 
     public static final ISimplifier NO_SIMPLIFICATION = new ISimplifier() {
         /**
          * 
          */
         private static final long serialVersionUID = 1L;
 
         public void simplify(IVecInt outLearnt) {
         }
 
         @Override
         public String toString() {
             return "No reason simplification"; //$NON-NLS-1$
         }
     };
 
     public final ISimplifier SIMPLE_SIMPLIFICATION = new ISimplifier() {
         /**
          * 
          */
         private static final long serialVersionUID = 1L;
 
         public void simplify(IVecInt outLearnt) {
             simpleSimplification(outLearnt);
         }
 
         @Override
         public String toString() {
             return "Simple reason simplification"; //$NON-NLS-1$
         }
     };
 
     public final ISimplifier EXPENSIVE_SIMPLIFICATION = new ISimplifier() {
 
         /**
          * 
          */
         private static final long serialVersionUID = 1L;
 
         public void simplify(IVecInt outLearnt) {
             expensiveSimplification(outLearnt);
         }
 
         @Override
         public String toString() {
             return "Expensive reason simplification"; //$NON-NLS-1$
         }
     };
 
     private ISimplifier simplifier = NO_SIMPLIFICATION;
 
     /**
      * Setup the reason simplification strategy.
      * By default, there is no reason simplification.
      * NOTE THAT REASON SIMPLIFICATION IS ONLY ALLOWED FOR WL 
      * CLAUSAL data structures. USING REASON SIMPLIFICATION
      * ON CB CLAUSES, CARDINALITY CONSTRAINTS OR PB CONSTRAINTS
      * MIGHT RESULT IN INCORRECT RESULTS. 
      * 
      * @param simp the name of the simplifier (one of NO_SIMPLIFICATION, SIMPLE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION).
      */
     public void setSimplifier(String simp) {
         Field f;
         try {
             f = Solver.class.getDeclaredField(simp);
             simplifier = (ISimplifier) f.get(this);
         } catch (Exception e) {
             e.printStackTrace();
             simplifier = NO_SIMPLIFICATION;
         }
     }
 
     /**
      * Setup the reason simplification strategy.
      * By default, there is no reason simplification.
      * NOTE THAT REASON SIMPLIFICATION IS ONLY ALLOWED FOR WL 
      * CLAUSAL data structures. USING REASON SIMPLIFICATION
      * ON CB CLAUSES, CARDINALITY CONSTRAINTS OR PB CONSTRAINTS
      * MIGHT RESULT IN INCORRECT RESULTS. 
      * 
      * @param simp
      */
     public void setSimplifier(ISimplifier simp) {
         simplifier = simp;
     }
 
     // Taken from MiniSAT 1.14: Simplify conflict clause (a little):
     private void simpleSimplification(IVecInt outLearnt) {
         int i, j;
         final boolean[] seen = mseen;
         for (i = j = 1; i < outLearnt.size(); i++) {
             IConstr r = voc.getReason(outLearnt.get(i));
             if (r == null) {
                 outLearnt.moveTo(j++, i);
             } else {
                 assert r.get(0) == neg(outLearnt.get(i));
                 for (int k = 1; k < r.size(); k++)
                     if (!seen[r.get(k) >> 1] && (voc.getLevel(r.get(k)) != 0)) {
                         outLearnt.moveTo(j++, i);
                         break;
                     }
             }
         }
         outLearnt.shrink(i - j);
         stats.reducedliterals += (i - j);
     }
 
     private final IVecInt analyzetoclear = new VecInt();
 
     private final IVecInt analyzestack = new VecInt();
 
     // Taken from MiniSAT 1.14
     private void expensiveSimplification(IVecInt outLearnt) {
         // Simplify conflict clause (a lot):
         //
         int i, j;
         // (maintain an abstraction of levels involved in conflict)
         analyzetoclear.clear();
         outLearnt.copyTo(analyzetoclear);
         for (i = 1, j = 1; i < outLearnt.size(); i++)
             if (voc.getReason(outLearnt.get(i)) == null
                     || !analyzeRemovable(outLearnt.get(i)))
                 outLearnt.moveTo(j++, i);
         outLearnt.shrink(i - j);
         stats.reducedliterals += (i - j);
     }
 
     // Check if 'p' can be removed. 'min_level' is used to abort early if
     // visiting literals at a level that cannot be removed.
     //
     private boolean analyzeRemovable(int p) {
         assert voc.getReason(p) != null;
         analyzestack.clear();
         analyzestack.push(p);
         final boolean[] seen = mseen;
         int top = analyzetoclear.size();
         while (analyzestack.size() > 0) {
             int q = analyzestack.last();
             assert voc.getReason(q) != null;
             Constr c = voc.getReason(q);
             analyzestack.pop();
             assert c.get(0) == neg(q);
             for (int i = 1; i < c.size(); i++) {
                 int l = c.get(i);
                 if (!seen[var(l)] && voc.getLevel(l) != 0) {
                     if (voc.getReason(l) == null) {
                         for (int j = top; j < analyzetoclear.size(); j++)
                             seen[analyzetoclear.get(j) >> 1] = false;
                         analyzetoclear.shrink(analyzetoclear.size() - top);
                         return false;
                     }
                     seen[l >> 1] = true;
                     analyzestack.push(l);
                     analyzetoclear.push(l);
                 }
             }
         }
 
         return true;
     }
 
     /**
      * decode the internal representation of a literal into Dimacs format.
      * 
      * @param p
      *            the literal in internal representation
      * @return the literal in dimacs representation
      */
     public static int decode2dimacs(int p) {
         return ((p & 1) == 0 ? 1 : -1) * (p >> 1);
     }
 
     /**
      * 
      */
     protected void undoOne() {
         // recupere le dernier litteral affecte
         int p = trail.last();
         assert p > 1;
         assert voc.getLevel(p) >= 0;
         int x = p >> 1;
         // desaffecte la variable
         voc.unassign(p);
         voc.setReason(p, null);
         voc.setLevel(p, -1);
         // met a jour l'heuristique
         order.undo(x);
         // depile le litteral des affectations
         trail.pop();
         // met a jour les contraintes apres desaffectation du litteral :
         // normalement, il n'y a rien a faire ici pour les prouveurs de type
         // Chaff??
         IVec<Undoable> undos = voc.undos(p);
         assert undos != null;
         while (undos.size() > 0) {
             undos.last().undo(p);
             undos.pop();
         }
     }
 
     /**
      * Propagate activity to a constraint
      * 
      * @param confl
      *            a constraint
      */
     public void claBumpActivity(Constr confl) {
         confl.incActivity(claInc);
         if (confl.getActivity() > CLAUSE_RESCALE_BOUND)
             claRescalActivity();
         // for (int i = 0; i < confl.size(); i++) {
         // varBumpActivity(confl.get(i));
         // }
     }
 
     public void varBumpActivity(int p) {
         order.updateVar(p);
     }
 
     private void claRescalActivity() {
         for (int i = 0; i < learnts.size(); i++) {
             learnts.get(i).rescaleBy(CLAUSE_RESCALE_FACTOR);
         }
         claInc *= CLAUSE_RESCALE_FACTOR;
     }
 
     /**
      * @return null if not conflict is found, else a conflicting constraint.
      */
     public Constr propagate() {
         while (qhead < trail.size()) {
             stats.propagations++;
             int p = trail.get(qhead++);
             slistener.propagating(decode2dimacs(p));
             order.assignLiteral(p);
             // p is the literal to propagate
             // Moved original MiniSAT code to dsfactory to avoid
             // watches manipulation in counter Based clauses for instance.
             assert p > 1;
             IVec<Propagatable> constrs = dsfactory.getWatchesFor(p);
 
             final int size = constrs.size();
             for (int i = 0; i < size; i++) {
                 stats.inspects++;
                 if (!constrs.get(i).propagate(this, p)) {
                     // Constraint is conflicting: copy remaining watches to
                     // watches[p]
                     // and return constraint
                     dsfactory.conflictDetectedInWatchesFor(p, i);
                     qhead = trail.size(); // propQ.clear();
                     // FIXME enlever le transtypage
                     return (Constr) constrs.get(i);
                 }
             }
         }
         return null;
     }
 
     void record(Constr constr) {
         constr.assertConstraint(this);
         slistener.adding(decode2dimacs(constr.get(0)));
         if (constr.size() == 1) {
             stats.learnedliterals++;
         } else {
             learner.learns(constr);
         }
     }
 
     /**
      * @return false ssi conflit imm?diat.
      */
     public boolean assume(int p) {
         // Precondition: assume propagation queue is empty
         assert trail.size() == qhead;
         trailLim.push(trail.size());
         return enqueue(p);
     }
 
     /**
      * Revert to the state before the last push()
      */
     private void cancel() {
         // assert trail.size() == qhead || !undertimeout;
         int decisionvar = trail.unsafeGet(trailLim.last());
         slistener.backtracking(decode2dimacs(decisionvar));
         for (int c = trail.size() - trailLim.last(); c > 0; c--) {
             undoOne();
         }
         trailLim.pop();
     }
 
     /**
      * Restore literals
      */
     private void cancelLearntLiterals() {
         // assert trail.size() == qhead || !undertimeout;
 
         for (int c = trail.size() - rootLevel; c > 0; c--) {
             undoOne();
         }
         qhead = trail.size();
     }
 
     /**
      * Cancel several levels of assumptions
      * 
      * @param level
      */
     protected void cancelUntil(int level) {
         while (decisionLevel() > level) {
             cancel();
         }
         qhead = trail.size();
     }
 
     private final Handle<Constr> learntConstraint = new Handle<Constr>();
 
     private boolean[] fullmodel;
 
     Lbool search(long nofConflicts) {
         assert rootLevel == decisionLevel();
         stats.starts++;
         int conflictC = 0;
 
         // varDecay = 1 / params.varDecay;
         order.setVarDecay(1 / params.getVarDecay());
         claDecay = 1 / params.getClaDecay();
 
         do {
             slistener.beginLoop();
             // propage les clauses unitaires
             Constr confl = propagate();
             assert trail.size() == qhead;
 
             if (confl == null) {
                 // No conflict found
                 // simpliFYDB() prevents a correct use of
                 // constraints removal.
                 // if (decisionLevel() == 0) {
                 // // Simplify the set of problem clause
                 // // iff rootLevel==0
                 // stats.rootSimplifications++;
                 // boolean ret = simplifyDB();
                 // assert ret;
                 // }
                 // was learnts.size() - nAssigns() > nofLearnts
                 // if (nofLearnts.obj >= 0 && learnts.size() > nofLearnts.obj) {
                 assert nAssigns() <= voc.realnVars();
                 if (nAssigns() == voc.realnVars()) {
                     slistener.solutionFound();
                     modelFound();
                     return Lbool.TRUE;
                 }
                 if (conflictC >= nofConflicts) {
                     // Reached bound on number of conflicts
                     // Force a restart
                     cancelUntil(rootLevel);
                     return Lbool.UNDEFINED;
                 }
                 if (needToReduceDB) {
                     reduceDB();
                     needToReduceDB = false;
                     // Runtime.getRuntime().gc();
                 }
                 // New variable decision
                 stats.decisions++;
                 int p = order.select();
                 assert p > 1;
                 slistener.assuming(decode2dimacs(p));
                 boolean ret = assume(p);
                 assert ret;
             } else {
                 // un conflit apparait
                 stats.conflicts++;
                 conflictC++;
                 slistener.conflictFound();
                 freeMem.newConflict();
                 if (decisionLevel() == rootLevel) {
                     // on est a la racine, la formule est inconsistante
                     return Lbool.FALSE;
                 }
                 // analyze conflict
                 int backtrackLevel = analyze(confl, learntConstraint);
                 assert backtrackLevel < decisionLevel();
                 cancelUntil(Math.max(backtrackLevel, rootLevel));
                 assert (decisionLevel() >= rootLevel)
                         && (decisionLevel() >= backtrackLevel);
                 if (learntConstraint.obj == null) {
                     return Lbool.FALSE;
                 }
                 record(learntConstraint.obj);
                 learntConstraint.obj = null;
                 decayActivities();
             }
         } while (undertimeout);
         return Lbool.UNDEFINED; // timeout occured
     }
 
     /**
      * 
      */
     void modelFound() {
         model = new int[trail.size()];
         fullmodel = new boolean[nVars()];
         int index = 0;
         for (int i = 1; i <= voc.nVars(); i++) {
             if (voc.belongsToPool(i)) {
                 int p = voc.getFromPool(i);
                 if (!voc.isUnassigned(p)) {
                     model[index++] = voc.isSatisfied(p) ? i : -i;
                     fullmodel[i - 1] = voc.isSatisfied(p);
                 }
             }
         }
         assert index == model.length;
         cancelUntil(rootLevel);
     }
 
     public boolean model(int var) {
         if (var <= 0 || var > nVars()) {
             throw new IllegalArgumentException(
                     "Use a valid Dimacs var id as argument!"); //$NON-NLS-1$
         }
         if (fullmodel == null) {
             throw new UnsupportedOperationException(
                     "Call the solve method first!!!"); //$NON-NLS-1$
         }
         return fullmodel[var - 1];
     }
 
     /**
      * 
      */
     protected void reduceDB() {
         reduceDB(claInc / learnts.size());
     }
 
     public void clearLearntClauses() {
         for (Constr c : learnts)
             c.remove();
         learnts.clear();
     }
 
     protected void reduceDB(double lim) {
         int i, j;
         sortOnActivity();
         stats.reduceddb++;
         for (i = j = 0; i < learnts.size() / 2; i++) {
             Constr c = learnts.get(i);
             if (c.locked()) {
                 learnts.set(j++, learnts.get(i));
             } else {
                 c.remove();
             }
         }
         for (; i < learnts.size(); i++) {
             // Constr c = learnts.get(i);
             // if (!c.locked() && (c.getActivity() < lim)) {
             // c.remove();
             // } else {
             learnts.set(j++, learnts.get(i));
             // }
         }
         System.out.println("c cleaning " + (learnts.size() - j) //$NON-NLS-1$
                 + " clauses out of " + learnts.size() + " for limit " + lim); //$NON-NLS-1$ //$NON-NLS-2$
         learnts.shrinkTo(j);
     }
 
     /**
      * @param learnts
      */
     private void sortOnActivity() {
         learnts.sort(comparator);
     }
 
     /**
      * 
      */
     protected void decayActivities() {
         order.varDecayActivity();
         claDecayActivity();
     }
 
     /**
      * 
      */
     private void claDecayActivity() {
         claInc *= claDecay;
     }
 
     /**
      * @return true iff the set of constraints is satisfiable, else false.
      */
     public boolean isSatisfiable() throws TimeoutException {
         return isSatisfiable(VecInt.EMPTY);
     }
 
     private double timebegin = 0;
 
     private boolean needToReduceDB;
 
     private ConflictTimer freeMem;
     
     public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
         Lbool status = Lbool.UNDEFINED;
         
         order.init();
         learner.init();
         restarter.init(params);
         timebegin = System.currentTimeMillis();
         slistener.start();
         model = null; // forget about previous model
         fullmodel = null;
 
         // propagate constraints
         if (propagate() != null) {
             slistener.end(Lbool.FALSE);
             cancelUntil(0);
             return false;
         }
 
         // push incremental assumptions
         for (int q : assumps) {
             if (!assume(voc.getFromPool(q)) || (propagate() != null)) {
                 slistener.end(Lbool.FALSE);
                 cancelUntil(0);
                 return false;
             }
         }
         rootLevel = decisionLevel();
 
         TimerTask stopMe = new TimerTask() {
             @Override
             public void run() {
                 undertimeout = false;
             }
         };
         undertimeout = true;
         Timer timer = new Timer(true);
         timer.schedule(stopMe, timeout);
         needToReduceDB = false;
 
         final long memorybound = Runtime.getRuntime().freeMemory() / 10;
         freeMem = new ConflictTimer(500) {
             private static final long serialVersionUID = 1L;
                     @Override
                     void run() {
                         long freemem = Runtime.getRuntime().freeMemory();
                         // System.out.println("c Free memory "+freemem);
                         if (freemem < memorybound) {
                             // Reduce the set of learnt clauses
                             needToReduceDB = true;
                         }
                     }
                 };
         // Solve
         while ((status == Lbool.UNDEFINED) && undertimeout) {
             status = search(restarter.nextRestartNumberOfConflict());
             // System.out.println("c speed "+(stats.decisions/((System.currentTimeMillis()-timebegin)/1000))+" dec/s, "+stats.starts+"/"+stats.conflicts);
             restarter.onRestart();
         }
 
         cancelUntil(0);
         timer.cancel();
         slistener.end(status);
         if (!undertimeout) {
             throw new TimeoutException(" Timeout (" + timeout + "s) exceeded"); //$NON-NLS-1$//$NON-NLS-2$
         }
         return status == Lbool.TRUE;
     }
 
     public SolverStats getStats() {
         return stats;
     }
 
     public IOrder<L> getOrder() {
         return order;
     }
 
     public void setOrder(IOrder<L> h) {
         order = h;
         order.setLits(voc);
     }
 
     public L getVocabulary() {
         return voc;
     }
 
     public void reset() {
         // FIXME verify that cleanup is OK
         voc.resetPool();
         dsfactory.reset();
         constrs.clear();
         learnts.clear();
         stats.reset();
     }
 
     public int nVars() {
         return voc.nVars();
     }
 
     /**
      * @param constr
      *            a constraint implementing the Constr interface.
      * @return a reference to the constraint for external use.
      */
     protected IConstr addConstr(Constr constr) {
         if (constr != null) {
             constrs.push(constr);
         }
         return constr;
     }
 
     public DataStructureFactory<L> getDSFactory() {
         return dsfactory;
     }
 
     public IVecInt getOutLearnt() {
         return outLearnt;
     }
 
     /**
      * returns the ith constraint in the solver.
      * 
      * @param i
      *            the constraint number (begins at 0)
      * @return the ith constraint
      */
     public IConstr getIthConstr(int i) {
         return constrs.get(i);
     }
 
     /*
      * (non-Javadoc)
      * 
      * @see org.sat4j.specs.ISolver#printStat(java.io.PrintStream,
      *      java.lang.String)
      */
     public void printStat(PrintStream out, String prefix) {
         printStat(new PrintWriter(out), prefix);
     }
 
     public void printStat(PrintWriter out, String prefix) {
         stats.printStat(out, prefix);
         double cputime = (System.currentTimeMillis() - timebegin) / 1000;
         out.println(prefix + "speed (decisions/second)\t: " + stats.decisions //$NON-NLS-1$
                 / cputime);
         order.printStat(out, prefix);
     }
 
     /*
      * (non-Javadoc)
      * 
      * @see java.lang.Object#toString()
      */
     public String toString(String prefix) {
         StringBuilder stb = new StringBuilder();
         Object[] objs = { analyzer, dsfactory, learner, params, order,
                 simplifier, restarter };
         // stb.append(prefix);
         stb.append("--- Begin Solver configuration ---"); //$NON-NLS-1$
         stb.append("\n"); //$NON-NLS-1$
         for (Object o : objs) {
             stb.append(prefix);
             stb.append(o.toString());
             stb.append("\n"); //$NON-NLS-1$
         }
         stb.append(prefix);
         stb.append("--- End Solver configuration ---"); //$NON-NLS-1$
         return stb.toString();
     }
 
     /*
      * (non-Javadoc)
      * 
      * @see java.lang.Object#toString()
      */
     @Override
     public String toString() {
         return toString(""); //$NON-NLS-1$
     }
 
     public int getTimeout() {
         return (int)(timeout/1000);
     }
 
     public void setExpectedNumberOfClauses(int nb) {
         constrs.ensure(nb);
     }
 
     public Map<String, Number> getStat() {
         return stats.toMap();
     }
 
     public int[] findModel() throws TimeoutException {
         if (isSatisfiable()) {
             return model();
         }
         // DLB findbugs ok
         // A zero length array would mean that the formula is a tautology.
         return null;
     }
 
     public int[] findModel(IVecInt assumps) throws TimeoutException {
         if (isSatisfiable(assumps)) {
             return model();
         }
         // DLB findbugs ok
         // A zero length array would mean that the formula is a tautology.
         return null;
     }
 
 }
 
 class ActivityComparator implements Comparator<Constr>, Serializable {
 
     private static final long serialVersionUID = 1L;
 
     /*
      * (non-Javadoc)
      * 
      * @see java.util.Comparator#compare(java.lang.Object, java.lang.Object)
      */
     public int compare(Constr c1, Constr c2) {
         return (int) Math.round(c1.getActivity() - c2.getActivity());
     }
 }
 
 abstract class ConflictTimer implements Serializable {
     
     private int counter;
     private final int bound;
     
     ConflictTimer(final int bound)  {
         this.bound = bound;
         counter = 0;
     }
     
     void reset() {
         counter = 0;
     }
     
     void newConflict() {
         counter++;
         if (counter==bound) {
             run();
             counter = 0;
         }
     }
     
     abstract void run();
 }