|
|||||||||||||||||||
Source file | Conditionals | Statements | Methods | TOTAL | |||||||||||||||
MiniSATLearning.java | - | 100% | 100% | 100% |
|
1 | /* | |
2 | * SAT4J: a SATisfiability library for Java Copyright (C) 2004 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 | |
7 | * the Sixth International Conference on Theory and Applications of | |
8 | * Satisfiability 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.minisat.learning; | |
26 | ||
27 | import java.io.Serializable; | |
28 | ||
29 | import org.sat4j.minisat.core.Constr; | |
30 | import org.sat4j.minisat.core.DataStructureFactory; | |
31 | ||
32 | /** | |
33 | * MiniSAT learning scheme. | |
34 | * | |
35 | * @author leberre | |
36 | */ | |
37 | public class MiniSATLearning extends AbstractLearning implements Serializable { | |
38 | private static final long serialVersionUID = 1L; | |
39 | ||
40 | private DataStructureFactory dsf; | |
41 | ||
42 | 1929 | public void setDataStructureFactory(DataStructureFactory dsf) { |
43 | 1929 | this.dsf = dsf; |
44 | } | |
45 | ||
46 | 1782 | public void init() { |
47 | ||
48 | } | |
49 | ||
50 | /* | |
51 | * (non-Javadoc) | |
52 | * | |
53 | * @see org.sat4j.minisat.LearningScheme#learns(org.sat4j.minisat.Solver, | |
54 | * org.sat4j.minisat.datatype.Vec) | |
55 | */ | |
56 | 18354401 | public void learns(Constr constr) { |
57 | // va contenir une nouvelle clause ou null si la clause est unitaire | |
58 | 18354401 | claBumpActivity(constr); |
59 | 18354401 | dsf.learnConstraint(constr); |
60 | } | |
61 | } |
|