View Javadoc

1   /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 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 the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * 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.constraints.cnf;
26  
27  import java.util.HashSet;
28  import java.util.Set;
29  
30  import org.sat4j.core.VecInt;
31  import org.sat4j.minisat.core.IMarkableLits;
32  import org.sat4j.specs.IVecInt;
33  
34  public class MarkableLits extends Lits implements IMarkableLits {
35  
36      /**
37       * 
38       */
39      private static final long serialVersionUID = 1L;
40  
41      private int[] marks;
42  
43      private static final int DEFAULTMARK = 1;
44  
45      @Override
46      public void init(int nvar) {
47          super.init(nvar);
48          marks = new int[(nvar << 1) + 2];
49      }
50  
51      public void setMark(int p, int mark) {
52          assert marks != null;
53          assert p > 1;
54          assert p < marks.length;
55          marks[p] = mark;
56      }
57  
58      public void setMark(int p) {
59          setMark(p, DEFAULTMARK);
60      }
61  
62      public int getMark(int p) {
63          return marks[p];
64      }
65  
66      public boolean isMarked(int p) {
67          return marks[p] != MARKLESS;
68      }
69  
70      public void resetMark(int p) {
71          marks[p] = MARKLESS;
72      }
73  
74      public void resetAllMarks() {
75          for (int i = 2; i < marks.length; i++)
76              resetMark(i);
77      }
78  
79      public IVecInt getMarkedLiterals() {
80          IVecInt marked = new VecInt();
81          for (int i = 2; i < marks.length; i++) {
82              if (isMarked(i))
83                  marked.push(i);
84          }
85          return marked;
86      }
87  
88      public IVecInt getMarkedLiterals(int mark) {
89          IVecInt marked = new VecInt();
90          for (int i = 2; i < marks.length; i++) {
91              if (getMark(i) == mark)
92                  marked.push(i);
93          }
94          return marked;
95      }
96  
97      public IVecInt getMarkedVariables() {
98          IVecInt marked = new VecInt();
99          for (int i = 2; i < marks.length; i += 2) {
100             if (isMarked(i) || isMarked(i + 1))
101                 marked.push(i >> 1);
102         }
103         return marked;
104     }
105 
106     public IVecInt getMarkedVariables(int mark) {
107         IVecInt marked = new VecInt();
108         for (int i = 2; i < marks.length; i += 2) {
109             if (getMark(i) == mark || getMark(i + 1) == mark)
110                 marked.push(i >> 1);
111         }
112         return marked;
113     }
114 
115     public Set<Integer> getMarks() {
116         Set<Integer> markers = new HashSet<Integer>();
117         for (int m : marks)
118             if (m != MARKLESS)
119                 markers.add(m);
120         return markers;
121     }
122 }