|
|||||||||||||||||||
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 org.sat4j.minisat.core.Constr; | |
28 | import org.sat4j.minisat.core.DataStructureFactory; | |
29 | ||
30 | /** | |
31 | * MiniSAT learning scheme. | |
32 | * | |
33 | * @author leberre | |
34 | */ | |
35 | public class MiniSATLearning extends AbstractLearning { | |
36 | private static final long serialVersionUID = 1L; | |
37 | ||
38 | private DataStructureFactory dsf; | |
39 | ||
40 | 2404 | public void setDataStructureFactory(DataStructureFactory dsf) { |
41 | 2404 | this.dsf = dsf; |
42 | } | |
43 | ||
44 | 3686059 | public void learns(Constr constr) { |
45 | // va contenir une nouvelle clause ou null si la clause est unitaire | |
46 | 3686059 | claBumpActivity(constr); |
47 | 3686059 | dsf.learnConstraint(constr); |
48 | } | |
49 | } |
|