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 Reader reader = null;
57  
58  	private final ISolver solver;
59  
60  	public InstanceReader(ISolver solver) {
61  		// dimacs = new DimacsReader(solver);
62  		this.solver = solver;
63  	}
64  
65  	private Reader getDefaultSATReader() {
66  		if (dimacs == null) {
67  			dimacs = new LecteurDimacs(solver);// new LecteurDimacs(solver);
68  		}
69  		return dimacs;
70  	}
71  
72  	private Reader getEZSATReader() {
73  		if (ezdimacs == null) {
74  			ezdimacs = new DimacsReader(solver);// new LecteurDimacs(solver);
75  		}
76  		return ezdimacs;
77  	}
78  
79  	private Reader getAIGReader() {
80  		if (aig == null) {
81  			aig = new AIGReader(solver);
82  		}
83  		return aig;
84  	}
85  
86  	private Reader getAAGReader() {
87  		if (aag == null) {
88  			aag = new AAGReader(solver);
89  		}
90  		return aag;
91  	}
92  
93  	@Override
94  	public IProblem parseInstance(String filename)
95  			throws FileNotFoundException, ParseFormatException, IOException,
96  			ContradictionException {
97  		String fname;
98  		boolean isHttp = false;
99  		String tempFileName = "";
100 		String prefix = "";
101 
102 		if (filename.startsWith("http://")) {
103 			isHttp = true;
104 			tempFileName = filename;
105 			filename = filename.substring(filename.lastIndexOf('/'), filename
106 					.length() - 1);
107 		}
108 
109 		if (filename.indexOf(':') != -1) {
110 
111 			String[] parts = filename.split(":");
112 			filename = parts[1];
113 			prefix = parts[0].toUpperCase(Locale.getDefault());
114 
115 		}
116 
117 		if (filename.endsWith(".gz")) {
118 			fname = filename.substring(0, filename.lastIndexOf('.'));
119 		} else {
120 			fname = filename;
121 		}
122 		if ("EZCNF".equals(prefix)) {
123 			reader = getEZSATReader();
124 		} else if (fname.endsWith(".aag")) {
125 			reader = getAAGReader();
126 		} else if (fname.endsWith(".aig")) {
127 			reader = getAIGReader();
128 
129 		} else {
130 			reader = getDefaultSATReader();
131 		}
132 
133 		if (isHttp) {
134 			return reader.parseInstance((new URL(tempFileName)).openStream());
135 		}
136 		return reader.parseInstance(filename);
137 	}
138 
139 	@Override
140 	@Deprecated
141 	public String decode(int[] model) {
142 		return reader.decode(model);
143 	}
144 
145 	@Override
146 	public void decode(int[] model, PrintWriter out) {
147 		reader.decode(model, out);
148 	}
149 
150 	@Override
151 	public IProblem parseInstance(java.io.Reader in)
152 			throws ParseFormatException, ContradictionException, IOException {
153 		throw new UnsupportedOperationException();
154 	}
155 }