Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
47   231   10   1,62
20   142   0,81   29
29     1,31  
1    
 
  DimacsOutputSolver       Line # 50 47 10 30,2% 0.30208334
 
No Tests
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le
3    * Berre
4    *
5    * Based on the original minisat specification from:
6    *
7    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
8    * Sixth International Conference on Theory and Applications of Satisfiability
9    * Testing, LNCS 2919, pp 502-518, 2003.
10    *
11    * This library is free software; you can redistribute it and/or modify it under
12    * the terms of the GNU Lesser General Public License as published by the Free
13    * Software Foundation; either version 2.1 of the License, or (at your option)
14    * any later version.
15    *
16    * This library is distributed in the hope that it will be useful, but WITHOUT
17    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
18    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
19    * details.
20    *
21    * You should have received a copy of the GNU Lesser General Public License
22    * along with this library; if not, write to the Free Software Foundation, Inc.,
23    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
24    *
25    */
26   
27    package org.sat4j.tools;
28   
29    import java.io.ObjectInputStream;
30    import java.io.PrintStream;
31    import java.io.PrintWriter;
32    import java.math.BigInteger;
33    import java.util.Map;
34   
35    import org.sat4j.specs.ContradictionException;
36    import org.sat4j.specs.IConstr;
37    import org.sat4j.specs.ISolver;
38    import org.sat4j.specs.IVec;
39    import org.sat4j.specs.IVecInt;
40    import org.sat4j.specs.TimeoutException;
41   
42    /**
43    * Solver used to display in a writer the CNF instance in Dimacs format.
44    *
45    * That solver is useful to produce CNF files to be used by third party solvers.
46    *
47    * @author leberre
48    *
49    */
 
50    public class DimacsOutputSolver implements ISolver {
51   
52    /**
53    *
54    */
55    private static final long serialVersionUID = 1L;
56   
57    private transient PrintWriter out;
58   
59    private int nbvars;
60   
61    private int nbclauses;
62   
63    private boolean fixedNbClauses = false;
64   
65    private boolean firstConstr = true;
66   
 
67  1 toggle public DimacsOutputSolver() {
68  1 this(new PrintWriter(System.out, true));
69    }
70   
 
71  1 toggle public DimacsOutputSolver(PrintWriter pw) {
72  1 out = pw;
73    }
74   
 
75  0 toggle private void readObject(ObjectInputStream stream) {
76  0 out = new PrintWriter(System.out, true);
77    }
78   
 
79  0 toggle public int newVar() {
80  0 return 0;
81    }
82   
 
83  1 toggle public int newVar(int howmany) {
84  1 out.print("p cnf " + howmany);
85  1 nbvars = howmany;
86  1 return 0;
87    }
88   
 
89  1 toggle public void setExpectedNumberOfClauses(int nb) {
90  1 out.println(" " + nb);
91  1 nbclauses = nb;
92  1 fixedNbClauses = true;
93    }
94   
 
95  415 toggle public IConstr addClause(IVecInt literals) throws ContradictionException {
96  415 if (firstConstr) {
97  1 if (!fixedNbClauses) {
98  0 out.println(" XXXXXX");
99    }
100  1 firstConstr = false;
101    }
102  415 for (int i : literals)
103  900 out.print(i + " ");
104  415 out.println("0");
105  415 return null;
106    }
107   
 
108  0 toggle public boolean removeConstr(IConstr c) {
109  0 throw new UnsupportedOperationException();
110    }
111   
 
112  0 toggle public void addAllClauses(IVec<IVecInt> clauses)
113    throws ContradictionException {
114  0 throw new UnsupportedOperationException();
115    }
116   
 
117  0 toggle public IConstr addAtMost(IVecInt literals, int degree)
118    throws ContradictionException {
119  0 if (degree > 1) {
120  0 throw new UnsupportedOperationException(
121    "Not a clausal problem! degree " + degree);
122    }
123  0 assert degree == 1;
124  0 if (firstConstr) {
125  0 if (!fixedNbClauses) {
126  0 out.println("XXXXXX");
127    }
128  0 firstConstr = false;
129    }
130  0 for (int i = 0; i <= literals.size(); i++) {
131  0 for (int j = i + 1; j < literals.size(); j++) {
132  0 out.println("" + (-literals.get(i)) + " " + (-literals.get(j))
133    + " 0");
134    }
135    }
136  0 return null;
137    }
138   
 
139  0 toggle public IConstr addAtLeast(IVecInt literals, int degree)
140    throws ContradictionException {
141  0 if (degree > 1) {
142  0 throw new UnsupportedOperationException(
143    "Not a clausal problem! degree " + degree);
144    }
145  0 assert degree == 1;
146  0 return addClause(literals);
147    }
148   
 
149  0 toggle public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
150    boolean moreThan, BigInteger d) throws ContradictionException {
151  0 throw new UnsupportedOperationException();
152    }
153   
 
154  1 toggle public void setTimeout(int t) {
155    // TODO Auto-generated method stub
156   
157    }
158   
 
159  0 toggle public void setTimeoutMs(long t) {
160    // TODO Auto-generated method stub
161    }
162   
 
163  0 toggle public int getTimeout() {
164    // TODO Auto-generated method stub
165  0 return 0;
166    }
167   
 
168  2 toggle public void reset() {
169  2 fixedNbClauses = false;
170  2 firstConstr = true;
171   
172    }
173   
 
174  0 toggle public void printStat(PrintStream out, String prefix) {
175    // TODO Auto-generated method stub
176   
177    }
178   
 
179  0 toggle public void printStat(PrintWriter out, String prefix) {
180    // TODO Auto-generated method stub
181   
182    }
183   
 
184  0 toggle public Map<String, Number> getStat() {
185    // TODO Auto-generated method stub
186  0 return null;
187    }
188   
 
189  0 toggle public String toString(String prefix) {
190  0 return "Dimacs output solver";
191    }
192   
 
193  0 toggle public void clearLearntClauses() {
194    // TODO Auto-generated method stub
195   
196    }
197   
 
198  0 toggle public int[] model() {
199  0 throw new UnsupportedOperationException();
200    }
201   
 
202  0 toggle public boolean model(int var) {
203  0 throw new UnsupportedOperationException();
204    }
205   
 
206  1 toggle public boolean isSatisfiable() throws TimeoutException {
207  1 throw new TimeoutException("There is no real solver behind!");
208    }
209   
 
210  0 toggle public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
211  0 throw new TimeoutException("There is no real solver behind!");
212    }
213   
 
214  0 toggle public int[] findModel() throws TimeoutException {
215  0 throw new UnsupportedOperationException();
216    }
217   
 
218  0 toggle public int[] findModel(IVecInt assumps) throws TimeoutException {
219  0 throw new UnsupportedOperationException();
220    }
221   
 
222  0 toggle public int nConstraints() {
223  0 return nbclauses;
224    }
225   
 
226  0 toggle public int nVars() {
227    // TODO Auto-generated method stub
228  0 return nbvars;
229    }
230   
231    }
 
CloverReport generated by Clover Code Coverage v2.0a5
mer. juin 27 2007 07:27:33 CEST.		   Beta Testers License registered to clover-support@cenqua.com. This license of Clover2 is provided for beta testing only. You have 5 day(s) before your Beta Tester License expires.