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.core;
26
27 import java.util.Set;
28
29 import org.sat4j.specs.IVecInt;
30
31 /**
32 * Vocabulary in which literals can be marked.
33 *
34 * @author daniel
35 *
36 */
37 public interface IMarkableLits extends ILits {
38 int MARKLESS = 0;
39
40 /**
41 * Mark a given literal with a given mark.
42 *
43 * @param p
44 * the literal
45 * @param mark
46 * an integer used to mark the literal. The specific mark
47 * MARKLESS is used to denote that the literal is not marked. The
48 * marks are supposed to be positive in the most common cases.
49 */
50 void setMark(int p, int mark);
51
52 /**
53 * Mark a given literal.
54 *
55 * @param p
56 * a literal
57 */
58 void setMark(int p);
59
60 /**
61 * To get the mark for a given literal.
62 *
63 * @param p
64 * a literal
65 * @return the mark associated with that literal, or MARKLESS if the literal
66 * is not marked.
67 */
68 int getMark(int p);
69
70 /**
71 * To know if a given literal is marked, i.e. has a mark different from
72 * MARKLESS.
73 *
74 * @param p
75 * a literal
76 * @return true iif the literal is marked.
77 */
78 boolean isMarked(int p);
79
80 /**
81 * Set the mark of a given literal to MARKLESS.
82 *
83 * @param p
84 * a literal
85 */
86 void resetMark(int p);
87
88 /**
89 * Set all the literal marks to MARKLESS
90 *
91 */
92 void resetAllMarks();
93
94 /**
95 * Returns the set of all marked literals.
96 *
97 * @return a set of literals whose mark is different from MARKLESS.
98 */
99 IVecInt getMarkedLiterals();
100
101 /**
102 * Returns that set of all the literals having a specific mark.
103 *
104 * @param mark
105 * a mark
106 * @return a set of literals whose mark is mark
107 */
108 IVecInt getMarkedLiterals(int mark);
109
110 /**
111 * Returns the set of all marked variables. A variable is marked iff at
112 * least one of its literal is marked.
113 *
114 * @return a set of variables whose mark is different from MARKLESS.
115 */
116 IVecInt getMarkedVariables();
117
118 /**
119 * Returns the set of all variables having a specific mark. A variable is
120 * marked iff at least one of its literal is marked.
121 *
122 * @param mark
123 * a mark.
124 * @return a set of variables whose mark is mark.
125 */
126 IVecInt getMarkedVariables(int mark);
127
128 /**
129 *
130 * @return a list of marks used to mark the literals.
131 */
132 Set<Integer> getMarks();
133 }