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.tools;
29  
30  import java.io.FileNotFoundException;
31  import java.io.FileOutputStream;
32  import java.io.PrintStream;
33  
34  import org.sat4j.specs.IConstr;
35  import org.sat4j.specs.Lbool;
36  import org.sat4j.specs.SearchListener;
37  
38  /**
39   * @since 2.2
40   */
41  public class LearnedClauseSizeTracing implements SearchListener {
42  
43  	/**
44  	 * 
45  	 */
46  	private static final long serialVersionUID = 1L;
47  
48  	private final String filename;
49  	private PrintStream out;
50  
51  	public LearnedClauseSizeTracing(String filename) {
52  		this.filename = filename;
53  		updateWriter();
54  	}
55  
56  	private void updateWriter() {
57  		try {
58  			out = new PrintStream(new FileOutputStream(filename + ".dat"));
59  		} catch (FileNotFoundException e) {
60  			out = System.out;
61  		}
62  	}
63  
64  	public void adding(int p) {
65  		// TODO Auto-generated method stub
66  
67  	}
68  
69  	public void assuming(int p) {
70  
71  	}
72  
73  	public void backtracking(int p) {
74  		// TODO Auto-generated method stub
75  
76  	}
77  
78  	public void beginLoop() {
79  		// TODO Auto-generated method stub
80  
81  	}
82  
83  	public void conflictFound(IConstr confl, int dlevel, int trailLevel) {
84  		out.println(confl.size());
85  	}
86  
87  	public void conflictFound(int p) {
88  		// TODO Auto-generated method stub
89  
90  	}
91  
92  	public void delete(int[] clause) {
93  		// TODO Auto-generated method stub
94  
95  	}
96  
97  	public void end(Lbool result) {
98  		out.close();
99  	}
100 
101 	public void learn(IConstr c) {
102 		// TODO Auto-generated method stub
103 
104 	}
105 
106 	public void propagating(int p, IConstr reason) {
107 		// TODO Auto-generated method stub
108 
109 	}
110 
111 	public void solutionFound() {
112 		// TODO Auto-generated method stub
113 
114 	}
115 
116 	public void start() {
117 
118 	}
119 
120 	public void restarting() {
121 	}
122 
123 	public void backjump(int backjumpLevel) {
124 	}
125 
126 }