1 package org.sat4j.tools;
2
3 import java.util.SortedSet;
4 import java.util.TreeSet;
5
6 import org.sat4j.core.VecInt;
7 import org.sat4j.specs.ISolver;
8 import org.sat4j.specs.IVecInt;
9 import org.sat4j.specs.IteratorInt;
10
11 public class AbstractMinimalModel extends SolverDecorator<ISolver> {
12
13
14
15
16 private static final long serialVersionUID = 1L;
17 protected final SortedSet<Integer> pLiterals;
18 protected final SolutionFoundListener modelListener;
19
20 public static IVecInt positiveLiterals(ISolver solver) {
21 IVecInt literals = new VecInt(solver.nVars());
22 for (int i = 1; i <= solver.nVars(); i++) {
23 literals.push(i);
24 }
25 return literals;
26 }
27
28 public static IVecInt negativeLiterals(ISolver solver) {
29 IVecInt literals = new VecInt(solver.nVars());
30 for (int i = 1; i <= solver.nVars(); i++) {
31 literals.push(-i);
32 }
33 return literals;
34 }
35
36 public AbstractMinimalModel(ISolver solver) {
37 this(solver, SolutionFoundListener.VOID);
38 }
39
40 public AbstractMinimalModel(ISolver solver, IVecInt p) {
41 this(solver, p, SolutionFoundListener.VOID);
42 }
43
44 public AbstractMinimalModel(ISolver solver,
45 SolutionFoundListener modelListener) {
46 this(solver, negativeLiterals(solver), modelListener);
47 }
48
49 public AbstractMinimalModel(ISolver solver, IVecInt p,
50 SolutionFoundListener modelListener) {
51 super(solver);
52 this.pLiterals = new TreeSet<Integer>();
53 for (IteratorInt it = p.iterator(); it.hasNext();) {
54 this.pLiterals.add(it.next());
55 }
56 this.modelListener = modelListener;
57
58 }
59
60 }