View Javadoc

1   /*******************************************************************************
2   * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3   *
4   * All rights reserved. This program and the accompanying materials
5   * are made available under the terms of the Eclipse Public License v1.0
6   * which accompanies this distribution, and is available at
7   * http://www.eclipse.org/legal/epl-v10.html
8   *
9   * Alternatively, the contents of this file may be used under the terms of
10  * either the GNU Lesser General Public License Version 2.1 or later (the
11  * "LGPL"), in which case the provisions of the LGPL are applicable instead
12  * of those above. If you wish to allow use of your version of this file only
13  * under the terms of the LGPL, and not to allow others to use your version of
14  * this file under the terms of the EPL, indicate your decision by deleting
15  * the provisions above and replace them with the notice and other provisions
16  * required by the LGPL. If you do not delete the provisions above, a recipient
17  * may use your version of this file under the terms of the EPL or the LGPL.
18  * 
19  * Based on the original MiniSat specification from:
20  * 
21  * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22  * Sixth International Conference on Theory and Applications of Satisfiability
23  * Testing, LNCS 2919, pp 502-518, 2003.
24  *
25  * See www.minisat.se for the original solver in C++.
26  * 
27  *******************************************************************************/
28  package org.sat4j.reader;
29  
30  import java.io.FileNotFoundException;
31  import java.io.IOException;
32  import java.io.PrintWriter;
33  import java.net.URL;
34  import java.util.Locale;
35  
36  import org.sat4j.specs.ContradictionException;
37  import org.sat4j.specs.IProblem;
38  import org.sat4j.specs.ISolver;
39  
40  /**
41   * An reader having the responsability to choose the right reader according to
42   * the input.
43   * 
44   * @author leberre
45   */
46  public class InstanceReader extends Reader {
47  
48      private AAGReader aag;
49  
50      private AIGReader aig;
51  
52      private DimacsReader ezdimacs;
53  
54      private LecteurDimacs dimacs;
55  
56      private ExtendedDimacsReader edimacs;
57  
58      private Reader reader = null;
59  
60      private final ISolver solver;
61  
62      public InstanceReader(ISolver solver) {
63          // dimacs = new DimacsReader(solver);
64          this.solver = solver;
65      }
66  
67      private Reader getDefaultSATReader() {
68          if (dimacs == null) {
69              dimacs = new LecteurDimacs(solver);// new LecteurDimacs(solver);
70          }
71          return dimacs;
72      }
73  
74      private Reader getEZSATReader() {
75          if (ezdimacs == null) {
76              ezdimacs = new DimacsReader(solver);// new LecteurDimacs(solver);
77          }
78          return ezdimacs;
79      }
80  
81      private Reader getDefaultExtendedDimacsReader() {
82          if (edimacs == null) {
83              edimacs = new ExtendedDimacsReader(solver);
84          }
85          return edimacs;
86      }
87  
88      private Reader getAIGReader() {
89          if (aig == null) {
90              aig = new AIGReader(solver);
91          }
92          return aig;
93      }
94  
95      private Reader getAAGReader() {
96          if (aag == null) {
97              aag = new AAGReader(solver);
98          }
99          return aag;
100     }
101 
102     @Override
103     public IProblem parseInstance(String filename)
104             throws FileNotFoundException, ParseFormatException, IOException,
105             ContradictionException {
106         String fname;
107         boolean isHttp = false;
108         String tempFileName = "";
109         String prefix = "";
110 
111         if (filename.startsWith("http://")) {
112             isHttp = true;
113             tempFileName = filename;
114             filename = filename.substring(filename.lastIndexOf('/'), filename
115                     .length() - 1);
116         }
117 
118         if (filename.indexOf(':') != -1) {
119 
120             String[] parts = filename.split(":");
121             filename = parts[1];
122             prefix = parts[0].toUpperCase(Locale.getDefault());
123 
124         }
125 
126         if (filename.endsWith(".gz")) {
127             fname = filename.substring(0, filename.lastIndexOf('.'));
128         } else {
129             fname = filename;
130         }
131         if ("EZCNF".equals(prefix)) {
132             reader = getEZSATReader();
133         } else if (fname.endsWith(".edimacs") || fname.endsWith(".ncnf")
134                 || "EDIMACS".equals(prefix)) {
135             reader = getDefaultExtendedDimacsReader();
136         } else if (fname.endsWith(".aag")) {
137             reader = getAAGReader();
138         } else if (fname.endsWith(".aig")) {
139             reader = getAIGReader();
140 
141         } else {
142             reader = getDefaultSATReader();
143         }
144 
145         if (isHttp) {
146             return reader.parseInstance((new URL(tempFileName)).openStream());
147         }
148         return reader.parseInstance(filename);
149     }
150 
151     @Override
152     @Deprecated
153     public String decode(int[] model) {
154         return reader.decode(model);
155     }
156 
157     @Override
158     public void decode(int[] model, PrintWriter out) {
159         reader.decode(model, out);
160     }
161 
162     @Override
163     public IProblem parseInstance(java.io.Reader in)
164             throws ParseFormatException, ContradictionException, IOException {
165         throw new UnsupportedOperationException();
166     }
167 }