Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
20   125   4   3,33
6   62   0,45   6
6     1,5  
1    
 
  LanceurPseudo2005       Line # 48 20 4 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;
26   
27    import static java.lang.System.out;
28   
29    import org.sat4j.minisat.SolverFactory;
30    import org.sat4j.minisat.core.IOrder;
31    import org.sat4j.minisat.core.Solver;
32    import org.sat4j.minisat.orders.VarOrderHeapObjective;
33    import org.sat4j.opt.PseudoOptDecorator;
34    import org.sat4j.reader.OPBReader2005;
35    import org.sat4j.reader.OPBReader2006;
36    import org.sat4j.reader.ObjectiveFunction;
37    import org.sat4j.reader.Reader;
38    import org.sat4j.specs.IProblem;
39    import org.sat4j.specs.ISolver;
40    import org.sat4j.specs.TimeoutException;
41   
42    /**
43    * Launcher especially dedicated to the pseudo boolean 05 evaluation (@link
44    * http://www.cril.univ-artois.fr/PB05/).
45    *
46    * @author mederic
47    */
 
48    public class LanceurPseudo2005 extends AbstractOptimizationLauncher {
49   
50    /**
51    *
52    */
53    private static final long serialVersionUID = 1L;
54   
55    /**
56    * Lance le prouveur sur un fichier Dimacs
57    *
58    * @param args
59    * doit contenir le nom d'un fichier Dimacs, eventuellement
60    * compress?.
61    */
 
62  0 toggle public static void main(final String[] args) {
63  0 final AbstractLauncher lanceur = new LanceurPseudo2005();
64  0 lanceur.run(args);
65  0 System.exit(lanceur.getExitCode().value());
66    }
67   
68    protected ObjectiveFunction obfct;
69   
70    /*
71    * (non-Javadoc)
72    *
73    * @see org.sat4j.Lanceur#createReader(org.sat4j.specs.ISolver)
74    */
 
75  0 toggle @Override
76    protected Reader createReader(ISolver solver, String problemname) {
77  0 return new OPBReader2006(solver);
78    }
79   
 
80  0 toggle @Override
81    protected void solve(IProblem problem) throws TimeoutException {
82  0 ObjectiveFunction obj = ((OPBReader2005) getReader())
83    .getObjectiveFunction();
84  0 ((PseudoOptDecorator) problem).setObjectTiveFunction(obj);
85  0 IOrder<?> order = ((Solver) ((PseudoOptDecorator) problem).decorated())
86    .getOrder();
87  0 if (order instanceof VarOrderHeapObjective) {
88  0 ((VarOrderHeapObjective) order).setObjectiveFunction(obj);
89    }
90  0 super.solve(problem);
91    }
92   
93    /*
94    * (non-Javadoc)
95    *
96    * @see org.sat4j.Lanceur#configureSolver(java.lang.String[])
97    */
 
98  0 toggle @Override
99    protected ISolver configureSolver(String[] args) {
100  0 ISolver solver;
101  0 if (args.length > 1) {
102  0 solver = SolverFactory.instance().createSolverByName(args[0]);
103    } else {
104  0 solver = SolverFactory
105    .newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalMerging();
106    // solver = SolverFactory
107    // .newMinimalOPBClauseCardConstrMaxSpecificOrder();
108    }
109  0 solver = new PseudoOptDecorator(solver);
110  0 solver.setTimeout(Integer.MAX_VALUE);
111  0 out.println(solver.toString(COMMENT_PREFIX)); //$NON-NLS-1$
112  0 return solver;
113    }
114   
 
115  0 toggle @Override
116    protected void usage() {
117  0 out.println("java -jar sat4jPseudo instancename.opb"); //$NON-NLS-1$
118    }
119   
 
120  0 toggle @Override
121    protected String getInstanceName(String[] args) {
122  0 assert args.length == 1 || args.length == 2;
123  0 return args[args.length - 1];
124    }
125    }