Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 1 057   Methods: 66
NCLOC: 603   Classes: 3
 
 Source file Conditionals Statements Methods TOTAL
Solver.java 93,4% 88,2% 78,8% 88%
coverage coverage
 1    /*
 2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004 Daniel Le Berre
 3    *
 4    * Based on the original minisat specification from:
 5    *
 6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of
 7    * the Sixth International Conference on Theory and Applications of
 8    * Satisfiability Testing, LNCS 2919, pp 502-518, 2003.
 9    *
 10    * This library is free software; you can redistribute it and/or modify it
 11    * under the terms of the GNU Lesser General Public License as published by the
 12    * Free Software Foundation; either version 2.1 of the License, or (at your
 13    * option) any later version.
 14    *
 15    * This library is distributed in the hope that it will be useful, but WITHOUT
 16    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
 17    * FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License
 18    * for more details.
 19    *
 20    * You should have received a copy of the GNU Lesser General Public License
 21    * along with this library; if not, write to the Free Software Foundation,
 22    * Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 23    *
 24    */
 25   
 26    package org.sat4j.minisat.core;
 27   
 28    import java.io.PrintStream;
 29    import java.io.Serializable;
 30    import java.math.BigInteger;
 31    import java.util.Comparator;
 32    import java.util.Timer;
 33    import java.util.TimerTask;
 34   
 35    import org.sat4j.core.Vec;
 36    import org.sat4j.core.VecInt;
 37    import org.sat4j.specs.ContradictionException;
 38    import org.sat4j.specs.IConstr;
 39    import org.sat4j.specs.ISolver;
 40    import org.sat4j.specs.IVec;
 41    import org.sat4j.specs.IVecInt;
 42    import org.sat4j.specs.TimeoutException;
 43   
 44    /**
 45    * @author leberre
 46    */
 47    public class Solver implements ISolver, UnitPropagationListener,
 48    ActivityListener, Learner, Serializable {
 49   
 50    private static final long serialVersionUID = 1L;
 51   
 52    private static final double CLAUSE_RESCALE_FACTOR = 1e-20;
 53   
 54    private static final double CLAUSE_RESCALE_BOUND = 1 / CLAUSE_RESCALE_FACTOR;
 55   
 56    /**
 57    * List des contraintes du probl?me.
 58    */
 59    private final IVec<Constr> constrs = new Vec<Constr>(); // Constr
 60   
 61    // vector
 62   
 63    /**
 64    * Liste des clauses apprises.
 65    */
 66    private final IVec<Constr> learnts = new Vec<Constr>(); // Clause
 67   
 68    // vector
 69   
 70    /**
 71    * incr?ment pour l'activit? des clauses.
 72    */
 73    private double claInc = 1.0;
 74   
 75    /**
 76    * decay factor pour l'activit? des clauses.
 77    */
 78    private double claDecay = 1.0;
 79   
 80    /**
 81    * Queue de propagation
 82    */
 83    // private final IntQueue propQ = new IntQueue(); // Lit
 84    // head of the queue in trail ... (taken from MiniSAT 1.14)
 85    private int qhead = 0;
 86   
 87    // queue
 88   
 89    /**
 90    * affectation en ordre chronologique
 91    */
 92    protected final IVecInt trail = new VecInt(); // lit
 93   
 94    // vector
 95   
 96    /**
 97    * indice des s?parateurs des diff?rents niveau de d?cision dans trail
 98    */
 99    protected final IVecInt trailLim = new VecInt(); // int
 100   
 101    // vector
 102   
 103    /**
 104    * S?pare les hypoth?ses incr?mentale et recherche
 105    */
 106    protected int rootLevel;
 107   
 108    private int[] model = null;
 109   
 110    protected final ILits voc;
 111   
 112    private IOrder order;
 113   
 114    private final Comparator<Constr> comparator = new ActivityComparator();
 115   
 116    private final SolverStats stats = new SolverStats();
 117   
 118    private final LearningStrategy learner;
 119   
 120    protected final AssertingClauseGenerator analyzer;
 121   
 122    private boolean undertimeout;
 123   
 124    private int timeout = Integer.MAX_VALUE;
 125   
 126    protected final DataStructureFactory dsfactory;
 127   
 128    private final SearchParams params;
 129   
 130    private final IVecInt __dimacs_out = new VecInt();
 131   
 132    private SearchListener slistener = new NullSearchListener();
 133   
 134  4564607 private IVecInt dimacs2internal(IVecInt in) {
 135  4564607 if (voc.nVars() == 0) {
 136  0 throw new RuntimeException(
 137    "Please set the number of variables (solver.newVar() or solver.newVar(maxvar)) before adding constraints!");
 138    }
 139  4564607 __dimacs_out.clear();
 140  4564607 __dimacs_out.ensure(in.size());
 141  4564607 for (int i = 0; i < in.size(); i++) {
 142    assert (in.get(i) != 0) && (Math.abs(in.get(i)) <= voc.nVars());
 143  16393476 __dimacs_out.unsafePush(voc.getFromPool(in.get(i)));
 144    }
 145  4564607 return __dimacs_out;
 146    }
 147   
 148   
 149    /**
 150    * creates a Solver without LearningListener. A learningListener must be
 151    * added to the solver, else it won't backtrack!!! A data structure factory
 152    * must be provided, else it won't work either.
 153    *
 154    * @param acg
 155    * an asserting clause generator
 156    */
 157   
 158  1926 public Solver(AssertingClauseGenerator acg, LearningStrategy learner,
 159    DataStructureFactory dsf, IOrder order) {
 160  1926 this(acg, learner, dsf, new SearchParams(), order);
 161    }
 162   
 163  2031 public Solver(AssertingClauseGenerator acg, LearningStrategy learner,
 164    DataStructureFactory dsf, SearchParams params, IOrder order) {
 165  2031 analyzer = acg;
 166  2031 this.learner = learner;
 167  2031 dsfactory = dsf;
 168  2031 dsfactory.setUnitPropagationListener(this);
 169  2031 dsfactory.setLearner(this);
 170  2031 this.order = order;
 171  2031 voc = dsf.getVocabulary();
 172  2031 order.setLits(voc);
 173  2031 this.params = params;
 174    }
 175   
 176  0 public void setSearchListener(SearchListener sl) {
 177  0 slistener = sl;
 178    }
 179   
 180  1944 public void setTimeout(int t) {
 181  1944 timeout = t;
 182    }
 183   
 184  293667668 protected int nAssigns() {
 185  293667668 return trail.size();
 186    }
 187   
 188  1986 public int nConstraints() {
 189  1986 return constrs.size();
 190    }
 191   
 192  0 private int nLearnts() {
 193  0 return learnts.size();
 194    }
 195   
 196  18353541 public void learn(Constr c) {
 197    // slistener.learn(c);
 198  18353541 learnts.push(c);
 199  18353541 c.setLearnt();
 200  18353541 c.register();
 201  18353541 stats.learnedclauses++;
 202  18353541 switch (c.size()) {
 203  3105 case 2:
 204  3105 stats.learnedbinaryclauses++;
 205  3105 break;
 206  3560 case 3:
 207  3560 stats.learnedternaryclauses++;
 208  3560 break;
 209    }
 210    }
 211   
 212    public int decisionLevel() {
 213    return trailLim.size();
 214    }
 215   
 216  250626 public int newVar() {
 217  250626 int index = voc.nVars() + 1;
 218  250626 voc.ensurePool(index);
 219  250626 seen = new boolean[index + 1];
 220  250626 trail.ensure(index);
 221  250626 trailLim.ensure(index);
 222    // propQ.ensure(index);
 223  250626 order.newVar();
 224  250626 return index;
 225    }
 226   
 227  1658 public int newVar(int howmany) {
 228  1658 voc.ensurePool(howmany);
 229  1658 order.newVar(howmany);
 230  1658 seen = new boolean[howmany + 1];
 231  1658 trail.ensure(howmany);
 232  1658 trailLim.ensure(howmany);
 233    // propQ.ensure(howmany);
 234  1658 return voc.nVars();
 235    }
 236   
 237  4000735 public IConstr addClause(IVecInt literals) throws ContradictionException {
 238  4000735 IVecInt vlits = dimacs2internal(literals);
 239  4000735 return addConstr(dsfactory.createClause(vlits));
 240    }
 241   
 242  0 public boolean removeConstr(IConstr co) {
 243  0 Constr c = (Constr) co;
 244  0 c.remove();
 245  0 constrs.remove(c);
 246  0 clearLearntClauses();
 247  0 cancelLearntLiterals();
 248  0 return true;
 249    }
 250   
 251    // public IConstr addPseudoBoolean(IVecInt literals, IVecInt coeffs,
 252    // boolean moreThan, int degree) throws ContradictionException {
 253    // IVecInt vlits = dimacs2internal(literals);
 254    // assert vlits.size() == literals.size();
 255    // assert literals.size() == coeffs.size();
 256    // return addConstr(dsfactory.createPseudoBooleanConstraint(vlits, coeffs,
 257    // moreThan, degree));
 258    // }
 259   
 260  563859 public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs,
 261    boolean moreThan, BigInteger degree) throws ContradictionException {
 262  563859 IVecInt vlits = dimacs2internal(literals);
 263    assert vlits.size() == literals.size();
 264    assert literals.size() == coeffs.size();
 265  563859 return addConstr(dsfactory.createPseudoBooleanConstraint(vlits, coeffs,
 266    moreThan, degree));
 267    }
 268   
 269  0 public void addAllClauses(IVec<IVecInt> clauses)
 270    throws ContradictionException {
 271  0 for (int i = 0; i < clauses.size(); i++) {
 272  0 addClause(clauses.get(i));
 273    }
 274    }
 275   
 276  13 public IConstr addAtMost(IVecInt literals, int degree)
 277    throws ContradictionException {
 278  13 for (int i = 0; i < literals.size(); i++) {
 279  39 literals.set(i, -literals.get(i));
 280    }
 281  13 return addAtLeast(literals, literals.size() - degree);
 282    }
 283   
 284  13 public IConstr addAtLeast(IVecInt literals, int degree)
 285    throws ContradictionException {
 286  13 IVecInt vlits = dimacs2internal(literals);
 287  13 return addConstr(dsfactory.createCardinalityConstraint(vlits, degree));
 288    }
 289   
 290  8319 @SuppressWarnings("unchecked")
 291    public boolean simplifyDB() {
 292    // aucune raison de recommencer un propagate?
 293    // if (propagate() != null) {
 294    // // Un conflit est d?couvert, la base est inconsistante
 295    // return false;
 296    // }
 297   
 298    // Simplifie la base de clauses apres la premiere propagation des
 299    // clauses unitaires
 300  8319 IVec<Constr>[] cs = new IVec[] { constrs, learnts };
 301  8319 for (int type = 0; type < 2; type++) {
 302  16638 int j = 0;
 303  16638 for (int i = 0; i < cs[type].size(); i++) {
 304  9134027 if (cs[type].get(i).simplify()) {
 305    // enleve les contraintes satisfaites de la base
 306  226828 cs[type].get(i).remove();
 307    } else {
 308  8907199 cs[type].set(j++, cs[type].get(i));
 309    }
 310    }
 311  16638 cs[type].shrinkTo(j);
 312    }
 313  8319 return true;
 314    }
 315   
 316    /**
 317    * Si un mod?le est trouv?, ce vecteur contient le mod?le.
 318    *
 319    * @return un mod?le de la formule.
 320    */
 321  37 public int[] model() {
 322  37 if (model == null) {
 323  0 throw new UnsupportedOperationException(
 324    "Call the solve method first!!!");
 325    }
 326  37 int[] nmodel = new int[model.length];
 327  37 System.arraycopy(model, 0, nmodel, 0, model.length);
 328  37 return nmodel;
 329    }
 330   
 331    /**
 332    * Satisfait un litt?ral
 333    *
 334    * @param p
 335    * le litt?ral
 336    * @return true si tout se passe bien, false si un conflit appara?t.
 337    */
 338  146830808 public boolean enqueue(int p) {
 339  146830808 return enqueue(p, null);
 340    }
 341   
 342    /**
 343    * Put the literal on the queue of assignments to be done.
 344    *
 345    * @param p
 346    * the literal.
 347    * @param from
 348    * the reason to propagate that literal, else null
 349    * @return true if the asignment can be made, false if a conflict is
 350    * detected.
 351    */
 352    public boolean enqueue(int p, Constr from) {
 353    // System.err.println("prop "+Lits.toString(p)+" thanks to "+from);
 354    assert p > 1;
 355    if (voc.isSatisfied(p)) {
 356    // Constr old = voc.getReason(p);
 357    // if
 358    // (from!=null&&old!=null&&voc.getLevel(p)==decisionLevel()&&from.size()<old.size())
 359    // {
 360    // assert from.get(0)==p;
 361    // voc.setReason(p,from);
 362    // stats.changedreason++;
 363    // }
 364    return true;
 365    }
 366    if (voc.isFalsified(p)) {
 367    // conflicting enqueued assignment
 368  63340452 return false;
 369    }
 370    // new fact, store it
 371    voc.satisfies(p);
 372    voc.setLevel(p, decisionLevel());
 373    voc.setReason(p, from);
 374    trail.push(p);
 375    // propQ.insert(p);
 376    return true;
 377    }
 378   
 379    private boolean[] seen = new boolean[0];
 380   
 381    private final IVecInt preason = new VecInt();
 382   
 383    private final IVecInt outLearnt = new VecInt();
 384   
 385  93469633 public int analyze(Constr confl, Handle<Constr> outLearntRef) {
 386    assert confl != null;
 387  93469633 outLearnt.clear();
 388   
 389    assert outLearnt.size() == 0;
 390  93469633 for (int i = 0; i < seen.length; i++) {
 391  1124508873 seen[i] = false;
 392    }
 393   
 394  93469633 analyzer.initAnalyze();
 395  93469633 int p = ILits.UNDEFINED;
 396   
 397  93469633 outLearnt.push(ILits.UNDEFINED);
 398    // reserve de la place pour le litteral falsifie
 399  93469633 int outBtlevel = 0;
 400   
 401  93469633 do {
 402  975635365 preason.clear();
 403    assert confl != null;
 404  975635365 confl.calcReason(p, preason);
 405  975635365 if (confl.learnt())
 406  101597304 claBumpActivity(confl);
 407    // Trace reason for p
 408  975635365 for (int j = 0; j < preason.size(); j++) {
 409  1644854262 int q = preason.get(j);
 410  1644854262 order.updateVar(q);
 411  1644854262 if (!seen[q >> 1]) {
 412    // order.updateVar(q); // MINISAT
 413    seen[q >> 1] = true;
 414    if (voc.getLevel(q) == decisionLevel()) {
 415  975635365 analyzer.onCurrentDecisionLevelLiteral(q);
 416    } else if (voc.getLevel(q) > 0) {
 417    // ajoute les variables depuis le niveau de d?cision 0
 418    outLearnt.push(q ^ 1);
 419    outBtlevel = Math.max(outBtlevel, voc.getLevel(q));
 420    }
 421    }
 422    }
 423   
 424    // select next reason to look at
 425  975635365 do {
 426    p = trail.last();
 427    // System.err.print((Clause.lastid()+1)+"
 428    // "+((Clause)confl).getId()+" ");
 429    confl = voc.getReason(p);
 430    // System.err.println(((Clause)confl).getId());
 431    // assert(confl != null) || counter == 1;
 432    undoOne();
 433    } while (!seen[p >> 1]);
 434    // seen[p.var] indique que p se trouve dans outLearnt ou dans
 435    // le dernier niveau de d?cision
 436  975635365 } while (analyzer.clauseNonAssertive(confl));
 437   
 438  93469633 simplifier.simplify(outLearnt);
 439   
 440  93469633 outLearnt.set(0, p ^ 1);
 441   
 442  93469633 Constr c = dsfactory.createUnregisteredClause(outLearnt);
 443  93469633 slistener.learn(c);
 444   
 445  93469633 outLearntRef.obj = c;
 446   
 447    assert outBtlevel > -1;
 448  93469633 return outBtlevel;
 449    }
 450   
 451    interface ISimplifier extends Serializable {
 452    void simplify(IVecInt outLearnt);
 453    }
 454   
 455    public static final ISimplifier NO_SIMPLIFICATION = new ISimplifier() {
 456    /**
 457    *
 458    */
 459    private static final long serialVersionUID = 1L;
 460   
 461  89223259 public void simplify(IVecInt outLearnt) {
 462    }
 463   
 464  0 @Override
 465    public String toString() {
 466  0 return "No reason simplification";
 467    }
 468    };
 469   
 470    public final ISimplifier SIMPLE_SIMPLIFICATION = new ISimplifier() {
 471    /**
 472    *
 473    */
 474    private static final long serialVersionUID = 1L;
 475   
 476  4246374 public void simplify(IVecInt outLearnt) {
 477  4246374 simpleSimplification(outLearnt);
 478    }
 479   
 480  0 @Override
 481    public String toString() {
 482  0 return "Simple reason simplification";
 483    }
 484    };
 485   
 486    private ISimplifier simplifier = NO_SIMPLIFICATION;
 487   
 488  2 public void setSimplifier(ISimplifier simp) {
 489  2 simplifier = simp;
 490    }
 491   
 492    // Simplify conflict clause (a little):
 493  4246374 private void simpleSimplification(IVecInt outLearnt) {
 494  4246374 int i, j;
 495   
 496  4246374 for (i = j = 1; i < outLearnt.size(); i++) {
 497  95912168 IConstr r = voc.getReason(outLearnt.get(i));
 498  95912168 if (r == null) {
 499  41802539 outLearnt.moveTo(j++, i);
 500    } else {
 501  54109629 for (int k = 1; k < r.size(); k++)
 502  114632631 if (!seen[r.get(k) >> 1] && (voc.getLevel(r.get(k)) != 0)) {
 503  53264643 outLearnt.moveTo(j++, i);
 504  53264643 break;
 505    }
 506    }
 507    }
 508  4246374 outLearnt.shrink(i - j);
 509  4246374 stats.reducedliterals += (i - j);
 510    }
 511   
 512    // private void expensiveSimplification(IVecInt outLearn) {
 513    // // Simplify conflict clause (a lot):
 514    // //
 515    // int min_level = 0;
 516    // for (i = 1; i < outLearnt.size(); i++)
 517    // min_level |= 1 << (level[var(out_learnt[i])] & 31); // (maintain an
 518    // abstraction of levels involved in conflict)
 519    //
 520    // out_learnt.copyTo(analyze_toclear);
 521    // for (i = j = 1; i < out_learnt.size(); i++)
 522    // if (reason[var(out_learnt[i])] == GClause_NULL ||
 523    // !analyze_removable(out_learnt[i], min_level))
 524    // out_learnt[j++] = out_learnt[i];
 525    // }
 526    //
 527    // // Check if 'p' can be removed. 'min_level' is used to abort early if
 528    // visiting literals at a level that cannot be removed.
 529    // //
 530    // private boolean analyze_removable(int p, int min_level)
 531    // {
 532    // assert(reason[var(p)] != GClause_NULL);
 533    // analyze_stack.clear(); analyze_stack.push(p);
 534    // int top = analyze_toclear.size();
 535    // while (analyze_stack.size() > 0){
 536    // assert(reason[var(analyze_stack.last())] != GClause_NULL);
 537    // GClause r = reason[var(analyze_stack.last())]; analyze_stack.pop();
 538    // Clause& c = r.isLit() ? ((*analyze_tmpbin)[1] = r.lit(), *analyze_tmpbin)
 539    // : *r.clause();
 540    // for (int i = 1; i < c.size(); i++){
 541    // Lit p = c[i];
 542    // if (!analyze_seen[var(p)] && level[var(p)] != 0){
 543    // if (reason[var(p)] != GClause_NULL && ((1 << (level[var(p)] & 31)) &
 544    // min_level) != 0){
 545    // analyze_seen[var(p)] = 1;
 546    // analyze_stack.push(p);
 547    // analyze_toclear.push(p);
 548    // }else{
 549    // for (int j = top; j < analyze_toclear.size(); j++)
 550    // analyze_seen[var(analyze_toclear[j])] = 0;
 551    // analyze_toclear.shrink(analyze_toclear.size() - top);
 552    // return false;
 553    // }
 554    // }
 555    // }
 556    // }
 557    //
 558    // return true;
 559    // }
 560   
 561    /**
 562    * decode the internal representation of a literal into Dimacs format.
 563    *
 564    * @param p
 565    * the literal in internal representation
 566    * @return the literal in dimacs representation
 567    */
 568    public static int decode2dimacs(int p) {
 569    return ((p & 1) == 0 ? 1 : -1) * (p >> 1);
 570    }
 571   
 572    /**
 573    *
 574    */
 575    protected void undoOne() {
 576    // recupere le dernier litteral affecte
 577    int p = trail.last();
 578    assert p > 1;
 579    assert voc.getLevel(p) > 0;
 580    int x = p >> 1;
 581    // desaffecte la variable
 582    voc.unassign(p);
 583    voc.setReason(p, null);
 584    voc.setLevel(p, -1);
 585    // met a jour l'heuristique
 586    order.undo(x);
 587    // depile le litteral des affectations
 588    trail.pop();
 589    // met a jour les contraintes apres desaffectation du litteral :
 590    // normalement, il n'y a rien a faire ici pour les prouveurs de type
 591    // Chaff??
 592    IVec<Undoable> undos = voc.undos(p);
 593    assert undos != null;
 594    while (undos.size() > 0) {
 595  1290630367 undos.last().undo(p);
 596  1290630367 undos.pop();
 597    }
 598    }
 599   
 600    /**
 601    * Propagate activity to a constraint
 602    * @param confl a constraint
 603    */
 604  101597304 public void claBumpActivity(Constr confl) {
 605  101597304 confl.incActivity(claInc);
 606  101597304 if (confl.getActivity() > CLAUSE_RESCALE_BOUND)
 607  1969 claRescalActivity();
 608    // for (int i = 0; i < confl.size(); i++) {
 609    // varBumpActivity(confl.get(i));
 610    // }
 611    }
 612   
 613    public void varBumpActivity(int p) {
 614    order.updateVar(p);
 615    }
 616   
 617  1969 private void claRescalActivity() {
 618  1969 for (int i = 0; i < learnts.size(); i++) {
 619  84231 learnts.get(i).rescaleBy(CLAUSE_RESCALE_FACTOR);
 620    }
 621  1969 claInc *= CLAUSE_RESCALE_FACTOR;
 622    }
 623   
 624    /**
 625    * @return null if not conflict is found, else a conflicting constraint.
 626    */
 627  240368785 public Constr propagate() {
 628  240368785 while (qhead < trail.size()) {
 629  2038839501 stats.propagations++;
 630  2038839501 int p = trail.get(qhead++); // propQ.dequeue();
 631  2038839501 slistener.propagating(decode2dimacs(p));
 632    // p est maintenant le litt?ral a propager
 633    // Moved original MiniSAT code to dsfactory to avoid
 634    // watches manipulation in counter Based clauses for instance.
 635    assert p > 1;
 636  2038839501 IVec<Propagatable> constrs = dsfactory.getWatchesFor(p);
 637   
 638  2038839501 for (int i = 0; i < constrs.size(); i++) {
 639  54702070 stats.inspects++;
 640  54702070 if (!constrs.get(i).propagate(this, p)) {
 641    // Constraint is conflicting: copy remaining watches to
 642    // watches[p]
 643    // and return constraint
 644  93532944 dsfactory.conflictDetectedInWatchesFor(p, i);
 645  93532944 qhead = trail.size(); // propQ.clear();
 646    // FIXME enlever le transtypage
 647  93532944 return (Constr) constrs.get(i);
 648    }
 649    }
 650    }
 651  146835841 return null;
 652    }
 653   
 654  93532095 void record(Constr constr) {
 655  93532095 constr.setLearnt();
 656  93532095 constr.assertConstraint(this);
 657  93532095 slistener.adding(decode2dimacs(constr.get(0)));
 658  93532095 if (constr.size() == 1) {
 659  4319 stats.learnedliterals++;
 660    } else {
 661  93527776 learner.learns(constr);
 662    }
 663    }
 664   
 665    /**
 666    * @return false ssi conflit imm?diat.
 667    */
 668  146830419 public boolean assume(int p) {
 669    // Precondition: assume propagation queue is empty
 670    assert trail.size() == qhead;
 671  146830419 trailLim.push(trail.size());
 672  146830419 return enqueue(p);
 673    }
 674   
 675    /**
 676    * Revert to the state before the last push()
 677    */
 678  146803591 private void cancel() {
 679    // assert trail.size() == qhead || !undertimeout;
 680  146803591 int decisionvar = trail.unsafeGet(trailLim.last());
 681  146803591 slistener.backtracking(decode2dimacs(decisionvar));
 682  146803591 for (int c = trail.size() - trailLim.last(); c > 0; c--) {
 683  205617936 undoOne();
 684    }
 685  146803591 trailLim.pop();
 686    }
 687   
 688    /**
 689    * Restore literals
 690    */
 691  0 private void cancelLearntLiterals() {
 692    // assert trail.size() == qhead || !undertimeout;
 693   
 694  0 for (int c = trail.size() - rootLevel; c > 0; c--) {
 695  0 undoOne();
 696    }
 697    }
 698   
 699    /**
 700    * Cancel several levels of assumptions
 701    *
 702    * @param level
 703    */
 704  93537547 protected void cancelUntil(int level) {
 705  93537547 while (decisionLevel() > level) {
 706  146803591 cancel();
 707    }
 708  93537547 qhead = trail.size();
 709    }
 710   
 711    private final Handle<Constr> learntConstraint = new Handle<Constr>();
 712   
 713  4378 Lbool search(long nofConflicts, long nofLearnts) {
 714    assert rootLevel == decisionLevel();
 715  4378 stats.starts++;
 716  4378 int conflictC = 0;
 717   
 718    // varDecay = 1 / params.varDecay;
 719  4378 order.setVarDecay(1 / params.getVarDecay());
 720  4378 claDecay = 1 / params.getClaDecay();
 721   
 722  4378 do {
 723  240366777 slistener.beginLoop();
 724    // propage les clauses unitaires
 725  240366777 Constr confl = propagate();
 726    assert trail.size() == qhead;
 727   
 728  240366777 if (confl != null) {
 729    // un conflit apparait
 730  93532943 stats.conflicts++;
 731  93532943 conflictC++;
 732  93532943 slistener.conflictFound();
 733  93532943 if (decisionLevel() == rootLevel) {
 734    // on est a la racine, la formule est inconsistante
 735  820 return Lbool.FALSE;
 736    }
 737   
 738    // analyse la cause du conflit
 739    assert confl != null;
 740  93532123 int backtrackLevel = analyze(confl, learntConstraint);
 741    assert backtrackLevel < decisionLevel();
 742  93532123 cancelUntil(Math.max(backtrackLevel, rootLevel));
 743    assert (decisionLevel() >= rootLevel)
 744    && (decisionLevel() >= backtrackLevel);
 745  93532123 if (learntConstraint.obj == null) {
 746  28 return Lbool.FALSE;
 747    }
 748  93532095 record(learntConstraint.obj);
 749  93532095 learntConstraint.obj = null;
 750  93532095 decayActivities();
 751    } else {
 752    // No conflict found
 753  146833834 if (decisionLevel() == 0) {
 754    // Simplify the set of problem clause
 755    // iff rootLevel==0
 756  8319 stats.rootSimplifications++;
 757  8319 boolean ret = simplifyDB();
 758    assert ret;
 759    }
 760    // was learnts.size() - nAssigns() > nofLearnts
 761  146833834 if (nofLearnts >= 0 && learnts.size() > nofLearnts) {
 762    // Reduce the set of learnt clauses
 763  1966715 reduceDB();
 764    }
 765    assert nAssigns() <= voc.realnVars();
 766  146833834 if (nAssigns() == voc.realnVars()) {
 767  1044 modelFound();
 768  1044 slistener.solutionFound();
 769  1044 return Lbool.TRUE;
 770    }
 771  146832790 if (conflictC >= nofConflicts) {
 772    // Reached bound on number of conflicts
 773    // Force a restart
 774  2394 cancelUntil(rootLevel);
 775  2394 return Lbool.UNDEFINED;
 776    }
 777    // New variable decision
 778  146830396 stats.decisions++;
 779  146830396 int p = order.select();
 780    assert p > 1;
 781  146830396 slistener.assuming(decode2dimacs(p));
 782  146830396 boolean ret = assume(p);
 783    assert ret;
 784    }
 785  240362491 } while (undertimeout);
 786  92 return Lbool.UNDEFINED; // timeout occured
 787    }
 788   
 789    /**
 790    *
 791    */
 792  1044 void modelFound() {
 793    // Model found
 794  1044 model = new int[trail.size()];
 795  1044 int index = 0;
 796  1044 for (int i = 1; i <= voc.nVars(); i++) {
 797  375461 if (voc.belongsToPool(i) && !voc.isUnassigned(i)) {
 798  375461 model[index++] = voc.isSatisfied(voc.getFromPool(i)) ? i : -i;
 799    }
 800    }
 801    assert index == model.length;
 802  1044 cancelUntil(rootLevel);
 803    }
 804   
 805    /**
 806    *
 807    */
 808  1966715 protected void reduceDB() {
 809  1966715 reduceDB(claInc / learnts.size());
 810    }
 811   
 812  0 protected void clearLearntClauses() {
 813  0 reduceDB(Double.MAX_VALUE);
 814    }
 815   
 816  1966715 protected void reduceDB(double lim) {
 817  1966715 int i, j;
 818  1966715 sortOnActivity();
 819  1966715 stats.reduceddb++;
 820  1966715 for (i = j = 0; i < learnts.size() / 2; i++) {
 821  93825403 Constr c = learnts.get(i);
 822  93825403 if (!c.locked()) {
 823  18080903 c.remove();
 824    } else {
 825  75744500 learnts.set(j++, learnts.get(i));
 826    }
 827    }
 828  1966715 for (; i < learnts.size(); i++) {
 829  94872438 Constr c = learnts.get(i);
 830  94872438 if (!c.locked() && (c.getActivity() < lim)) {
 831  144890 c.remove();
 832    } else {
 833  94727548 learnts.set(j++, learnts.get(i));
 834    }
 835    }
 836  1966715 learnts.shrinkTo(j);
 837    }
 838   
 839    /**
 840    * @param learnts
 841    */
 842  1966715 private void sortOnActivity() {
 843  1966715 learnts.sort(comparator);
 844    }
 845   
 846    /**
 847    *
 848    */
 849  93532095 protected void decayActivities() {
 850  93532095 order.varDecayActivity();
 851  93532095 claDecayActivity();
 852    }
 853   
 854    /**
 855    *
 856    */
 857  93532095 private void claDecayActivity() {
 858  93532095 claInc *= claDecay;
 859    }
 860   
 861    /**
 862    * @return true iff the set of constraints is satisfiable, else false.
 863    */
 864  1977 public boolean isSatisfiable() throws TimeoutException {
 865  1977 return isSatisfiable(VecInt.EMPTY);
 866    }
 867   
 868    private double timebegin = 0;
 869   
 870  1986 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
 871  1986 Lbool status = Lbool.UNDEFINED;
 872  1986 double nofConflicts = params.initConflictBound;
 873  1986 double nofLearnts = nConstraints()
 874    * params.initLearntBoundConstraintFactor;
 875   
 876  1986 order.init();
 877  1986 learner.init();
 878  1986 timebegin = System.currentTimeMillis();
 879   
 880  1986 model = null; // forget about previous model
 881   
 882    // propagate constraints
 883  1986 if (propagate() != null) {
 884  1 cancelUntil(0);
 885  1 return false;
 886    }
 887   
 888    // push incremental assumptions
 889  1985 for (int l : assumps) {
 890  15 if (!assume(voc.getFromPool(l))
 891    || (propagate() != null)) {
 892  1 cancelUntil(0);
 893  1 return false;
 894    }
 895    }
 896    // StringBuffer stb = new StringBuffer();
 897    // stb.append("%RESA ");
 898    // stb.append(nVars());
 899    // stb.append(" ");
 900    // stb.append(nConstraints());
 901    // while(stb.length()<255) {
 902    // stb.append(' ');
 903    // }
 904    // System.err.println(stb);
 905  1984 rootLevel = decisionLevel();
 906   
 907  1984 TimerTask stopMe = new TimerTask() {
 908  92 @Override
 909    public void run() {
 910  92 undertimeout = false;
 911    }
 912    };
 913  1984 undertimeout = true;
 914  1984 Timer timer = new Timer(true);
 915  1984 timer.schedule(stopMe, timeout * 1000L);
 916   
 917    // Solve
 918  1984 while ((status == Lbool.UNDEFINED) && undertimeout) {
 919  4378 status = search(Math.round(nofConflicts), Math.round(nofLearnts));
 920  4378 nofConflicts *= params.conflictBoundIncFactor;
 921  4378 nofLearnts *= params.learntBoundIncFactor;
 922    // order.mirror(stats.starts);
 923    }
 924   
 925  1984 cancelUntil(0);
 926  1984 timer.cancel();
 927  1984 if (!undertimeout) {
 928  92 throw new TimeoutException(" Timeout (" + timeout + "s) exceeded");
 929    }
 930  1892 return status == Lbool.TRUE;
 931    }
 932   
 933  0 public SolverStats getStats() {
 934  0 return stats;
 935    }
 936   
 937  102 public IOrder getOrder() {
 938  102 return order;
 939    }
 940   
 941  103 public void setOrder(IOrder h) {
 942  103 order = h;
 943  103 order.setLits(voc);
 944    }
 945   
 946  1101 public ILits getVocabulary() {
 947  1101 return voc;
 948    }
 949   
 950  2018 public void reset() {
 951    // FIXME verify that cleanup is OK
 952  2018 voc.resetPool();
 953  2018 dsfactory.reset();
 954  2018 constrs.clear();
 955  2018 learnts.clear();
 956  2018 stats.reset();
 957    }
 958   
 959  52 public int nVars() {
 960  52 return voc.nVars();
 961    }
 962   
 963    /**
 964    * @param constr
 965    * a constraint implementing the Constr interface.
 966    * @return a reference to the constraint for external use.
 967    */
 968  4564509 IConstr addConstr(Constr constr) {
 969  4564509 if (constr != null) {
 970  3965472 constrs.push(constr);
 971    }
 972  4564509 return constr;
 973    }
 974   
 975  1929 public DataStructureFactory getDSFactory() {
 976  1929 return dsfactory;
 977    }
 978   
 979  0 public IVecInt getOutLearnt() {
 980  0 return outLearnt;
 981    }
 982   
 983    /**
 984    * returns the ith constraint in the solver.
 985    *
 986    * @param i
 987    * the constraint number (begins at 0)
 988    * @return the ith constraint
 989    */
 990  1 public IConstr getIthConstr(int i) {
 991  1 return constrs.get(i);
 992    }
 993   
 994    /*
 995    * (non-Javadoc)
 996    *
 997    * @see org.sat4j.specs.ISolver#printStat(java.io.PrintStream,
 998    * java.lang.String)
 999    */
 1000  0 public void printStat(PrintStream out, String prefix) {
 1001  0 stats.printStat(out, prefix);
 1002  0 double cputime = (System.currentTimeMillis() - timebegin) / 1000;
 1003  0 out.println(prefix + "speed (decisions/second)\t: " + stats.decisions
 1004    / cputime);
 1005  0 order.printStat(out, prefix);
 1006    }
 1007   
 1008    /*
 1009    * (non-Javadoc)
 1010    *
 1011    * @see java.lang.Object#toString()
 1012    */
 1013  0 public String toString(String prefix) {
 1014  0 StringBuilder stb = new StringBuilder();
 1015  0 Object[] objs = { analyzer, dsfactory, learner, params, order,
 1016    simplifier };
 1017  0 stb.append(prefix);
 1018  0 stb.append("--- Begin Solver configuration ---");
 1019  0 stb.append("\n");
 1020  0 for (Object o : objs) {
 1021  0 stb.append(prefix);
 1022  0 stb.append(o.toString());
 1023  0 stb.append("\n");
 1024    }
 1025  0 stb.append(prefix);
 1026  0 stb.append("--- End Solver configuration ---");
 1027  0 return stb.toString();
 1028    }
 1029   
 1030    /*
 1031    * (non-Javadoc)
 1032    *
 1033    * @see java.lang.Object#toString()
 1034    */
 1035  0 @Override
 1036    public String toString() {
 1037  0 return toString("");
 1038    }
 1039   
 1040  0 public int getTimeout() {
 1041  0 return timeout;
 1042    }
 1043    }
 1044   
 1045    class ActivityComparator implements Comparator<Constr>, Serializable {
 1046   
 1047    private static final long serialVersionUID = 1L;
 1048   
 1049    /*
 1050    * (non-Javadoc)
 1051    *
 1052    * @see java.util.Comparator#compare(java.lang.Object, java.lang.Object)
 1053    */
 1054    public int compare(Constr c1, Constr c2) {
 1055    return (int) Math.round(c1.getActivity() - c2.getActivity());
 1056    }
 1057    }
 
CloverReport generated by Clover Code Coverage v1.3.9
jeu. sept. 29 2005 23:57:47 CEST.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.