View Javadoc

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.reader;
26  
27  import java.io.IOException;
28  import java.io.LineNumberReader;
29  import java.util.Scanner;
30  import java.util.StringTokenizer;
31  
32  import org.sat4j.specs.ContradictionException;
33  import org.sat4j.specs.ISolver;
34  import org.sat4j.specs.IVecInt;
35  import org.sat4j.tools.GateTranslator;
36  
37  /**
38   * Reader for the Extended Dimacs format proposed by Fahiem Bacchus and Toby
39   * Walsh.
40   * 
41   * @author leberre
42   * 
43   */
44  public class ExtendedDimacsReader extends DimacsReader {
45  
46      public static final int FALSE = 1;
47  
48      public static final int TRUE = 2;
49  
50      public static final int NOT = 3;
51  
52      public static final int AND = 4;
53  
54      public static final int NAND = 5;
55  
56      public static final int OR = 6;
57  
58      public static final int NOR = 7;
59  
60      public static final int XOR = 8;
61  
62      public static final int XNOR = 9;
63  
64      public static final int IMPLIES = 10;
65  
66      public static final int IFF = 11;
67  
68      public static final int IFTHENELSE = 12;
69  
70      public static final int ATLEAST = 13;
71  
72      public static final int ATMOST = 14;
73  
74      public static final int COUNT = 15;
75  
76      /**
77       * 
78       * 
79       */
80      private static final long serialVersionUID = 1L;
81  
82      public ExtendedDimacsReader(ISolver solver) {
83          super(new GateTranslator(solver));
84      }
85  
86      /**
87       * @param in
88       *            the input stream
89       * @throws IOException
90       *             iff an IO occurs
91       * @throws ParseFormatException
92       *             if the input stream does not comply with the DIMACS format.
93       */
94      @Override
95      protected void readProblemLine(LineNumberReader in) throws IOException,
96              ParseFormatException {
97  
98          String line = in.readLine();
99  
100         if (line == null) {
101             throw new ParseFormatException(
102                     "premature end of file: <p noncnf ...> expected  on line "
103                             + in.getLineNumber());
104         }
105         StringTokenizer stk = new StringTokenizer(line);
106 
107         if (!(stk.hasMoreTokens() && stk.nextToken().equals("p")
108                 && stk.hasMoreTokens() && stk.nextToken().equals("noncnf"))) {
109             throw new ParseFormatException(
110                     "problem line expected (p noncnf ...) on line "
111                             + in.getLineNumber());
112         }
113 
114         int vars;
115 
116         // reads the max var id
117         vars = Integer.parseInt(stk.nextToken());
118         assert vars > 0;
119         solver.newVar(vars);
120         try {
121             ((GateTranslator)solver).gateTrue(vars);
122         } catch (ContradictionException e) {
123             assert false;
124             System.err.println("Contradiction when asserting root variable?");
125         }
126         disableNumberOfConstraintCheck();
127     }
128 
129     /*
130      * (non-Javadoc)
131      * 
132      * @see org.sat4j.reader.DimacsReader#handleConstr(java.lang.String,
133      *      org.sat4j.specs.IVecInt)
134      */
135     @Override
136     protected boolean handleConstr(String line, IVecInt literals)
137             throws ContradictionException {
138         boolean added = true;
139         assert literals.size() == 0;
140         Scanner scan = new Scanner(line);
141         GateTranslator gater = (GateTranslator)solver;
142         while (scan.hasNext()) {
143             int gateType = scan.nextInt();
144             assert gateType > 0;
145             int nbparam = scan.nextInt();
146             assert nbparam != 0;
147             assert nbparam == -1 || gateType >= ATLEAST;
148             for (int i = 0; i < nbparam; i++) {
149                 scan.nextInt();
150             }
151             // readI/O until reaching ending 0
152             int y = scan.nextInt();
153             int x;
154             while ((x = scan.nextInt()) != 0) {
155                 literals.push(x);
156             }
157             switch (gateType) {
158             case FALSE:
159                 assert literals.size()==0;
160                 gater.gateFalse(y);
161                 break;
162             case TRUE:
163                 assert literals.size()==0;
164                 gater.gateTrue(y);
165                 break;
166             case OR:
167                 gater.or(y, literals);
168                 break;
169             case NOT:
170                 assert literals.size()==1;
171                 gater.not(y, literals.get(0));
172                 break;
173             case AND:
174                 gater.and(y, literals);
175                 break;
176             case XOR:
177                 gater.xor(y, literals);
178                 break;
179             case IFF:
180                 gater.iff(y, literals);
181                 break;
182             case IFTHENELSE:
183                 assert literals.size()==3;
184                 gater.ite(y, literals.get(0),literals.get(1),literals.get(2));
185                 break;
186             default:
187                 throw new UnsupportedOperationException("Gate type " + gateType
188                         + " not handled yet");
189             }
190         }
191         literals.clear();
192         return added;
193     }
194 
195 
196 }