|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| LecteurDimacs | Line # 51 | 92 | 36 | 77,6% |
0.7755102
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
| (101) | |||
| Result | |||
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT12
org.sat4j.minisat.AbstractM2Test.testAim50SAT12
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH49
org.sat4j.minisat.AbstractM2Test.testJNH49
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT13
org.sat4j.minisat.AbstractM2Test.testAim50SAT13
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH50
org.sat4j.minisat.AbstractM2Test.testJNH50
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT14
org.sat4j.minisat.AbstractM2Test.testAim50SAT14
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testHole6
org.sat4j.minisat.AbstractM2Test.testHole6
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT15
org.sat4j.minisat.AbstractM2Test.testAim50SAT15
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testHole7
org.sat4j.minisat.AbstractM2Test.testHole7
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT8
org.sat4j.minisat.AbstractM2Test.testAim50SAT8
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testHole8
org.sat4j.minisat.AbstractM2Test.testHole8
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT9
org.sat4j.minisat.AbstractM2Test.testAim50SAT9
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testHole9
org.sat4j.minisat.AbstractM2Test.testHole9
|
3 FAIL | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT10
org.sat4j.minisat.AbstractM2Test.testAim50SAT10
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT11
org.sat4j.minisat.AbstractM2Test.testAim50SAT11
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH41
org.sat4j.minisat.AbstractM2Test.testJNH41
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT4
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT4
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH42
org.sat4j.minisat.AbstractM2Test.testJNH42
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT5
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT5
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH43
org.sat4j.minisat.AbstractM2Test.testJNH43
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT6
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT6
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH44
org.sat4j.minisat.AbstractM2Test.testJNH44
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT7
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT7
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH45
org.sat4j.minisat.AbstractM2Test.testJNH45
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT16
org.sat4j.minisat.AbstractM2Test.testAim50SAT16
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH46
org.sat4j.minisat.AbstractM2Test.testJNH46
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT1
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT1
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH47
org.sat4j.minisat.AbstractM2Test.testJNH47
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT2
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT2
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH48
org.sat4j.minisat.AbstractM2Test.testJNH48
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT3
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT3
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT5
org.sat4j.minisat.AbstractM2Test.testAim50SAT5
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT4
org.sat4j.minisat.AbstractM2Test.testAim50SAT4
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT7
org.sat4j.minisat.AbstractM2Test.testAim50SAT7
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT6
org.sat4j.minisat.AbstractM2Test.testAim50SAT6
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT1
org.sat4j.minisat.AbstractM2Test.testAim50SAT1
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT3
org.sat4j.minisat.AbstractM2Test.testAim50SAT3
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT2
org.sat4j.minisat.AbstractM2Test.testAim50SAT2
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH23
org.sat4j.minisat.AbstractM2Test.testJNH23
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH24
org.sat4j.minisat.AbstractM2Test.testJNH24
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH21
org.sat4j.minisat.AbstractM2Test.testJNH21
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH22
org.sat4j.minisat.AbstractM2Test.testJNH22
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH19
org.sat4j.minisat.AbstractM2Test.testJNH19
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH20
org.sat4j.minisat.AbstractM2Test.testJNH20
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH17
org.sat4j.minisat.AbstractM2Test.testJNH17
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH18
org.sat4j.minisat.AbstractM2Test.testJNH18
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH15
org.sat4j.minisat.AbstractM2Test.testJNH15
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH16
org.sat4j.minisat.AbstractM2Test.testJNH16
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH13
org.sat4j.minisat.AbstractM2Test.testJNH13
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH14
org.sat4j.minisat.AbstractM2Test.testJNH14
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH11
org.sat4j.minisat.AbstractM2Test.testJNH11
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH12
org.sat4j.minisat.AbstractM2Test.testJNH12
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH9
org.sat4j.minisat.AbstractM2Test.testJNH9
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH10
org.sat4j.minisat.AbstractM2Test.testJNH10
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH40
org.sat4j.minisat.AbstractM2Test.testJNH40
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH39
org.sat4j.minisat.AbstractM2Test.testJNH39
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH38
org.sat4j.minisat.AbstractM2Test.testJNH38
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH37
org.sat4j.minisat.AbstractM2Test.testJNH37
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH36
org.sat4j.minisat.AbstractM2Test.testJNH36
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH35
org.sat4j.minisat.AbstractM2Test.testJNH35
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH34
org.sat4j.minisat.AbstractM2Test.testJNH34
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH33
org.sat4j.minisat.AbstractM2Test.testJNH33
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH32
org.sat4j.minisat.AbstractM2Test.testJNH32
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH31
org.sat4j.minisat.AbstractM2Test.testJNH31
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH30
org.sat4j.minisat.AbstractM2Test.testJNH30
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH29
org.sat4j.minisat.AbstractM2Test.testJNH29
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH28
org.sat4j.minisat.AbstractM2Test.testJNH28
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH27
org.sat4j.minisat.AbstractM2Test.testJNH27
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH26
org.sat4j.minisat.AbstractM2Test.testJNH26
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH25
org.sat4j.minisat.AbstractM2Test.testJNH25
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi12
org.sat4j.minisat.AbstractM2Test.testIi12
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi13
org.sat4j.minisat.AbstractM2Test.testIi13
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi14
org.sat4j.minisat.AbstractM2Test.testIi14
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi15
org.sat4j.minisat.AbstractM2Test.testIi15
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi8
org.sat4j.minisat.AbstractM2Test.testIi8
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi9
org.sat4j.minisat.AbstractM2Test.testIi9
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi10
org.sat4j.minisat.AbstractM2Test.testIi10
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi11
org.sat4j.minisat.AbstractM2Test.testIi11
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi4
org.sat4j.minisat.AbstractM2Test.testIi4
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi5
org.sat4j.minisat.AbstractM2Test.testIi5
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi6
org.sat4j.minisat.AbstractM2Test.testIi6
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi7
org.sat4j.minisat.AbstractM2Test.testIi7
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT8
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT8
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi1
org.sat4j.minisat.AbstractM2Test.testIi1
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi2
org.sat4j.minisat.AbstractM2Test.testIi2
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi3
org.sat4j.minisat.AbstractM2Test.testIi3
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH6
org.sat4j.minisat.AbstractM2Test.testJNH6
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH5
org.sat4j.minisat.AbstractM2Test.testJNH5
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH8
org.sat4j.minisat.AbstractM2Test.testJNH8
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH7
org.sat4j.minisat.AbstractM2Test.testJNH7
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH2
org.sat4j.minisat.AbstractM2Test.testJNH2
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH1
org.sat4j.minisat.AbstractM2Test.testJNH1
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH4
org.sat4j.minisat.AbstractM2Test.testJNH4
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH3
org.sat4j.minisat.AbstractM2Test.testJNH3
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi22
org.sat4j.minisat.AbstractM2Test.testIi22
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi21
org.sat4j.minisat.AbstractM2Test.testIi21
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi24
org.sat4j.minisat.AbstractM2Test.testIi24
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi23
org.sat4j.minisat.AbstractM2Test.testIi23
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi17
org.sat4j.minisat.AbstractM2Test.testIi17
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi16
org.sat4j.minisat.AbstractM2Test.testIi16
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi20
org.sat4j.minisat.AbstractM2Test.testIi20
|
1 PASS | |
|
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi18
org.sat4j.minisat.AbstractM2Test.testIi18
|
1 PASS | |
| 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 | ||
| 26 | package org.sat4j.reader; | |
| 27 | ||
| 28 | import java.io.BufferedInputStream; | |
| 29 | import java.io.IOException; | |
| 30 | import java.io.InputStream; | |
| 31 | import java.io.PrintWriter; | |
| 32 | import java.io.Serializable; | |
| 33 | ||
| 34 | import org.sat4j.core.VecInt; | |
| 35 | import org.sat4j.specs.ContradictionException; | |
| 36 | import org.sat4j.specs.IProblem; | |
| 37 | import org.sat4j.specs.ISolver; | |
| 38 | import org.sat4j.specs.IVecInt; | |
| 39 | ||
| 40 | /** | |
| 41 | * Dimacs Reader written by Frederic Laihem. It is much faster than DimacsReader | |
| 42 | * because it does not split the input file into strings but reads and interpret | |
| 43 | * the input char by char. Hence, it is a bit more difficult to read and to | |
| 44 | * modify than DimacsReader. | |
| 45 | * | |
| 46 | * This reader is used during the SAT Competitions. | |
| 47 | * | |
| 48 | * @author laihem | |
| 49 | * @author leberre | |
| 50 | */ | |
| 51 | public class LecteurDimacs extends Reader implements Serializable { | |
| 52 | ||
| 53 | private static final long serialVersionUID = 1L; | |
| 54 | ||
| 55 | /* taille du buffer */ | |
| 56 | private final static int TAILLE_BUF = 16384; | |
| 57 | ||
| 58 | private final ISolver s; | |
| 59 | ||
| 60 | private transient BufferedInputStream in; | |
| 61 | ||
| 62 | /* nombre de literaux dans le fichier */ | |
| 63 | private int nbLit = 0; | |
| 64 | ||
| 65 | private int nbClauses = 0; | |
| 66 | ||
| 67 | private static final char EOF = (char) -1; | |
| 68 | ||
| 69 | /* | |
| 70 | * nomFichier repr?sente le nom du fichier ? lire | |
| 71 | */ | |
| 72 | 1673 |
public LecteurDimacs(ISolver s) { |
| 73 | 1673 | this.s = s; |
| 74 | } | |
| 75 | ||
| 76 | 1673 |
@Override |
| 77 | public final IProblem parseInstance(final InputStream in) | |
| 78 | throws ParseFormatException, ContradictionException, IOException { | |
| 79 | ||
| 80 | 1673 | this.in = new BufferedInputStream(in, LecteurDimacs.TAILLE_BUF); |
| 81 | 1673 | s.reset(); |
| 82 | 1673 | passerCommentaire(); |
| 83 | 1673 | if (nbLit == 0) |
| 84 | 0 | throw new IOException( |
| 85 | "DIMACS non valide (nombre de Literaux non valide)"); | |
| 86 | 1673 | s.newVar(nbLit); |
| 87 | 1673 | s.setExpectedNumberOfClauses(nbClauses); |
| 88 | 1673 | char car = passerEspaces(); |
| 89 | 1673 | if (car == EOF) |
| 90 | 0 | throw new IOException("DIMACS non valide (ou sont les clauses ?)"); |
| 91 | 1673 | ajouterClauses(car); |
| 92 | 1673 | in.close(); |
| 93 | 1673 | return s; |
| 94 | } | |
| 95 | ||
| 96 | 0 |
@Override |
| 97 | public IProblem parseInstance(java.io.Reader in) throws IOException, | |
| 98 | ContradictionException { | |
| 99 | 0 | throw new UnsupportedOperationException(); |
| 100 | } | |
| 101 | ||
| 102 | /** on passe les commentaires et on lit le nombre de literaux */ | |
| 103 | 1673 |
private char passerCommentaire() throws IOException { |
| 104 | 1673 | char car; |
| 105 | 1673 | for (;;) { |
| 106 | 22757 | car = passerEspaces(); |
| 107 | 22757 | if (car == 'p') { |
| 108 | 1673 | car = lectureNombreLiteraux(); |
| 109 | } | |
| 110 | 22757 | if (car != 'c' && car != 'p') |
| 111 | 1673 | break; /* fin des commentaires */ |
| 112 | 21084 | car = nextLine(); /* on passe la ligne de commentaire */ |
| 113 | 21084 | if (car == EOF) |
| 114 | 0 | break; |
| 115 | } | |
| 116 | 1673 | return car; |
| 117 | } | |
| 118 | ||
| 119 | /** lit le nombre repr?sentant le nombre de literaux */ | |
| 120 | 1673 |
private char lectureNombreLiteraux() throws IOException { |
| 121 | 1673 | char car = nextChiffre(); /* on lit le prchain chiffre */ |
| 122 | 1673 | if (car != EOF) { |
| 123 | 1673 | nbLit = car - '0'; |
| 124 | 1673 | for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */ |
| 125 | 4610 | car = (char) in.read(); |
| 126 | 4610 | if (car < '0' || car > '9') |
| 127 | 1673 | break; |
| 128 | 2937 | nbLit = 10 * nbLit + (car - '0'); |
| 129 | } | |
| 130 | 1673 | car = nextChiffre(); |
| 131 | 1673 | nbClauses = car - '0'; |
| 132 | 1673 | for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */ |
| 133 | 5355 | car = (char) in.read(); |
| 134 | 5355 | if (car < '0' || car > '9') |
| 135 | 1673 | break; |
| 136 | 3682 | nbClauses = 10 * nbClauses + (car - '0'); |
| 137 | } | |
| 138 | 1673 | if (car != '\n' && car != EOF) |
| 139 | 0 | nextLine(); /* on lit la fin de la ligne */ |
| 140 | } | |
| 141 | 1673 | return car; |
| 142 | } | |
| 143 | ||
| 144 | /** lit les clauses et les ajoute dans le vecteur donn? en param?tre | |
| 145 | * @throws ParseFormatException */ | |
| 146 | 1673 |
private void ajouterClauses(char car) throws IOException, |
| 147 | ContradictionException, ParseFormatException { | |
| 148 | 1673 | final IVecInt lit = new VecInt(); |
| 149 | 1673 | int val = 0; |
| 150 | 1673 | boolean neg = false; |
| 151 | 1673 | for (;;) { |
| 152 | /* on lit le signe du literal */ | |
| 153 | 16341595 | if (car == '-') { |
| 154 | 7229578 | neg = true; |
| 155 | 7229578 | car = (char) in.read(); |
| 156 | 9112017 | } else if (car == '+') |
| 157 | 0 | car = (char) in.read(); |
| 158 | else /* on le 1er chiffre du literal */ | |
| 159 | 9112017 | if (car >= '0' && car <= '9') { |
| 160 | 9112017 | val = car - '0'; |
| 161 | 9112017 | car = (char) in.read(); |
| 162 | } else | |
| 163 | 0 | throw new ParseFormatException("Unknown character "+car); |
| 164 | /* on lit la suite du literal */ | |
| 165 | 41747295 | while (car >= '0' && car <= '9') { |
| 166 | 25405700 | val = (val * 10) + car - '0'; |
| 167 | 25405700 | car = (char) in.read(); |
| 168 | } | |
| 169 | 16341595 | if (val == 0) { // on a lu toute la clause |
| 170 | 4011911 | s.addClause(lit); |
| 171 | 4011911 | lit.clear(); |
| 172 | } else { | |
| 173 | /* on ajoute le literal au vecteur */ | |
| 174 | // s.newVar(val-1); | |
| 175 | 12329684 | lit.push(neg ? -val : val); |
| 176 | 12329684 | neg = false; |
| 177 | 12329684 | val = 0; /* on reinitialise les variables */ |
| 178 | } | |
| 179 | 16341595 | if (car != EOF) |
| 180 | 16341211 | car = passerEspaces(); |
| 181 | 16341595 | if (car == EOF) |
| 182 | 1673 | break; /* on a lu tout le fichier */ |
| 183 | } | |
| 184 | } | |
| 185 | ||
| 186 | /** passe tout les caract?res d'espacement (espace ou \n) */ | |
| 187 | 16365641 |
private char passerEspaces() throws IOException { |
| 188 | 16365641 | char car; |
| 189 | ||
| 190 | 0 | while ((car = (char) in.read()) == ' ' || car == '\n') |
| 191 | 16239200 | ; |
| 192 | 16365641 | return car; |
| 193 | } | |
| 194 | ||
| 195 | /** passe tout les caract?res jusqu? rencontrer une fin de la ligne */ | |
| 196 | 21084 |
private char nextLine() throws IOException { |
| 197 | 21084 | char car; |
| 198 | 21084 | do { |
| 199 | 558511 | car = (char) in.read(); |
| 200 | 558511 | } while ((car != '\n') && (car != EOF)); |
| 201 | 21084 | return car; |
| 202 | } | |
| 203 | ||
| 204 | /** passe tout les caract?re jusqu'? rencontrer un chiffre */ | |
| 205 | 3346 |
private char nextChiffre() throws IOException { |
| 206 | 3346 | char car; |
| 207 | 3346 | do { |
| 208 | 11711 | car = (char) in.read(); |
| 209 | 11711 | } while ((car < '0') || (car > '9') && (car != EOF)); |
| 210 | 3346 | return car; |
| 211 | } | |
| 212 | ||
| 213 | 0 |
@Override |
| 214 | public String decode(int[] model) { | |
| 215 | 0 | StringBuffer stb = new StringBuffer(); |
| 216 | 0 | for (int i = 0; i < model.length; i++) { |
| 217 | 0 | stb.append(model[i]); |
| 218 | 0 | stb.append(" "); |
| 219 | } | |
| 220 | 0 | stb.append("0"); |
| 221 | 0 | return stb.toString(); |
| 222 | } | |
| 223 | ||
| 224 | 0 |
@Override |
| 225 | public void decode(int[] model, PrintWriter out) { | |
| 226 | 0 | for (int i = 0; i < model.length; i++) { |
| 227 | 0 | out.print(model[i]); |
| 228 | 0 | out.print(" "); |
| 229 | } | |
| 230 | 0 | out.print("0"); |
| 231 | } | |
| 232 | } | |
|
||||||||||