Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
file stats: LOC: 49   Methods: 2
NCLOC: 27   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
RemiUtils.java 0% 0% 0% 0%
coverage
 1    package org.sat4j.tools;
 2   
 3    import org.sat4j.core.VecInt;
 4    import org.sat4j.specs.ISolver;
 5    import org.sat4j.specs.IVecInt;
 6    import org.sat4j.specs.TimeoutException;
 7   
 8    /**
 9    * Class dedicated to RŽmi Coletta utility methods :-)
 10    *
 11    * @author leberre
 12    */
 13    public class RemiUtils {
 14   
 15  0 private RemiUtils() {
 16    // no instanceof that class are expected to be used.
 17    }
 18   
 19    /**
 20    * Compute the set of literals common to all models of the formula.
 21    *
 22    * @param s
 23    * a solver already feeded
 24    * @return the set of literals common to all models of the formula contained
 25    * in the solver, in dimacs format.
 26    * @throws TimeoutException
 27    */
 28  0 public static IVecInt backbone(ISolver s) throws TimeoutException {
 29  0 IVecInt backbone = new VecInt();
 30  0 int nvars = s.nVars();
 31  0 for (int i = 1; i <= nvars; i++) {
 32  0 backbone.push(i);
 33  0 if (s.isSatisfiable(backbone)) {
 34  0 backbone.pop().push(-i);
 35  0 if (s.isSatisfiable(backbone)) {
 36  0 backbone.pop();
 37    } else {
 38    // -i is in the backbone
 39  0 backbone.pop().push(i);
 40    }
 41    } else {
 42    // -i is in the backbone
 43  0 backbone.pop().push(-i);
 44    }
 45    }
 46  0 return backbone;
 47    }
 48   
 49    }