1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3 *
4 * All rights reserved. This program and the accompanying materials
5 * are made available under the terms of the Eclipse Public License v1.0
6 * which accompanies this distribution, and is available at
7 * http://www.eclipse.org/legal/epl-v10.html
8 *
9 * Alternatively, the contents of this file may be used under the terms of
10 * either the GNU Lesser General Public License Version 2.1 or later (the
11 * "LGPL"), in which case the provisions of the LGPL are applicable instead
12 * of those above. If you wish to allow use of your version of this file only
13 * under the terms of the LGPL, and not to allow others to use your version of
14 * this file under the terms of the EPL, indicate your decision by deleting
15 * the provisions above and replace them with the notice and other provisions
16 * required by the LGPL. If you do not delete the provisions above, a recipient
17 * may use your version of this file under the terms of the EPL or the LGPL.
18 *
19 * Based on the original MiniSat specification from:
20 *
21 * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22 * Sixth International Conference on Theory and Applications of Satisfiability
23 * Testing, LNCS 2919, pp 502-518, 2003.
24 *
25 * See www.minisat.se for the original solver in C++.
26 *
27 *******************************************************************************/
28 package org.sat4j.minisat.core;
29
30 import java.util.Set;
31
32 import org.sat4j.specs.IVecInt;
33
34 /**
35 * Vocabulary in which literals can be marked.
36 *
37 * @author daniel
38 *
39 */
40 public interface IMarkableLits extends ILits {
41 int MARKLESS = 0;
42
43 /**
44 * Mark a given literal with a given mark.
45 *
46 * @param p
47 * the literal
48 * @param mark
49 * an integer used to mark the literal. The specific mark
50 * MARKLESS is used to denote that the literal is not marked. The
51 * marks are supposed to be positive in the most common cases.
52 */
53 void setMark(int p, int mark);
54
55 /**
56 * Mark a given literal.
57 *
58 * @param p
59 * a literal
60 */
61 void setMark(int p);
62
63 /**
64 * To get the mark for a given literal.
65 *
66 * @param p
67 * a literal
68 * @return the mark associated with that literal, or MARKLESS if the literal
69 * is not marked.
70 */
71 int getMark(int p);
72
73 /**
74 * To know if a given literal is marked, i.e. has a mark different from
75 * MARKLESS.
76 *
77 * @param p
78 * a literal
79 * @return true iif the literal is marked.
80 */
81 boolean isMarked(int p);
82
83 /**
84 * Set the mark of a given literal to MARKLESS.
85 *
86 * @param p
87 * a literal
88 */
89 void resetMark(int p);
90
91 /**
92 * Set all the literal marks to MARKLESS
93 *
94 */
95 void resetAllMarks();
96
97 /**
98 * Returns the set of all marked literals.
99 *
100 * @return a set of literals whose mark is different from MARKLESS.
101 */
102 IVecInt getMarkedLiterals();
103
104 /**
105 * Returns that set of all the literals having a specific mark.
106 *
107 * @param mark
108 * a mark
109 * @return a set of literals whose mark is mark
110 */
111 IVecInt getMarkedLiterals(int mark);
112
113 /**
114 * Returns the set of all marked variables. A variable is marked iff at
115 * least one of its literal is marked.
116 *
117 * @return a set of variables whose mark is different from MARKLESS.
118 */
119 IVecInt getMarkedVariables();
120
121 /**
122 * Returns the set of all variables having a specific mark. A variable is
123 * marked iff at least one of its literal is marked.
124 *
125 * @param mark
126 * a mark.
127 * @return a set of variables whose mark is mark.
128 */
129 IVecInt getMarkedVariables(int mark);
130
131 /**
132 *
133 * @return a list of marks used to mark the literals.
134 */
135 Set<Integer> getMarks();
136 }