Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
16   103   3   3,2
4   41   0,44   5
5     1,4  
1    
 
  DimacsArrayReader       Line # 46 16 3 0% 0.0
 
No Tests
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 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 the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    *
10    * This library is free software; you can redistribute it and/or modify it under
11    * the terms of the GNU Lesser General Public License as published by the Free
12    * Software Foundation; either version 2.1 of the License, or (at your option)
13    * 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 FITNESS
17    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18    * 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, Inc.,
22    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23    *
24    */
25    package org.sat4j.tools;
26   
27    import java.io.Serializable;
28   
29    import org.sat4j.core.VecInt;
30    import org.sat4j.specs.ContradictionException;
31    import org.sat4j.specs.IProblem;
32    import org.sat4j.specs.ISolver;
33    import org.sat4j.specs.IVecInt;
34   
35    /**
36    * Very simple Dimacs array reader. Allow solvers to read the constraints from
37    * arrays that effectively contain Dimacs formatted lines (without the
38    * terminating 0).
39    *
40    * Adaptation of org.sat4j.reader.DimacsReader.
41    *
42    * @author dlb
43    * @author or
44    * @author fuhs
45    */
 
46    public class DimacsArrayReader implements Serializable {
47   
48    private static final long serialVersionUID = 1L;
49   
50    protected final ISolver solver;
51   
 
52  0 toggle public DimacsArrayReader(ISolver solver) {
53  0 this.solver = solver;
54    }
55   
 
56  0 toggle protected boolean handleConstr(int gateType, int output, int[] inputs)
57    throws ContradictionException {
58  0 IVecInt literals = new VecInt(inputs);
59  0 solver.addClause(literals);
60  0 return true;
61    }
62   
63    /**
64    * @param gateType
65    * gateType[i] is the type of gate i according to the Extended
66    * Dimacs specs; ignored in DimacsArrayReader, but important for
67    * inheriting classes
68    * @param outputs
69    * outputs[i] is the number of the output; ignored in
70    * DimacsArrayReader
71    * @param inputs
72    * inputs[i] contains the clauses in DimacsArrayReader; an
73    * overriding class might have it contain the inputs of the
74    * current gate
75    * @param maxVar
76    * the maximum number of assigned ids
77    * @throws ContradictionException
78    * si le probleme est trivialement inconsitant
79    */
 
80  0 toggle public IProblem parseInstance(int[] gateType, int[] outputs,
81    int[][] inputs, int maxVar) throws ContradictionException {
82  0 solver.reset();
83  0 solver.newVar(maxVar);
84  0 for (int i = 0; i < outputs.length; ++i) {
85  0 handleConstr(gateType[i], outputs[i], inputs[i]);
86    }
87  0 return solver;
88    }
89   
 
90  0 toggle public String decode(int[] model) {
91  0 StringBuilder stb = new StringBuilder(4 * model.length);
92  0 for (int i = 0; i < model.length; i++) {
93  0 stb.append(model[i]);
94  0 stb.append(" ");
95    }
96  0 stb.append("0");
97  0 return stb.toString();
98    }
99   
 
100  0 toggle protected ISolver getSolver() {
101  0 return solver;
102    }
103    }