1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28 package org.sat4j.minisat.constraints.cnf;
29
30 import static org.sat4j.core.LiteralsUtils.neg;
31
32 import java.io.Serializable;
33
34 import org.sat4j.minisat.core.Constr;
35 import org.sat4j.minisat.core.ILits;
36 import org.sat4j.minisat.core.UnitPropagationListener;
37 import org.sat4j.specs.IVecInt;
38
39
40
41
42
43
44
45 public abstract class BinaryClause implements Constr, Serializable {
46
47 private static final long serialVersionUID = 1L;
48
49 protected double activity;
50
51 private final ILits voc;
52
53 protected int head;
54
55 protected int tail;
56
57
58
59
60
61
62
63
64
65 public BinaryClause(IVecInt ps, ILits voc) {
66 assert ps.size() == 2;
67 head = ps.get(0);
68 tail = ps.get(1);
69 this.voc = voc;
70 activity = 0;
71 }
72
73
74
75
76
77
78 public void calcReason(int p, IVecInt outReason) {
79 if (voc.isFalsified(head)) {
80 outReason.push(neg(head));
81 }
82 if (voc.isFalsified(tail)) {
83 outReason.push(neg(tail));
84 }
85 }
86
87
88
89
90
91
92 public void remove(UnitPropagationListener upl) {
93 voc.watches(neg(head)).remove(this);
94 voc.watches(neg(tail)).remove(this);
95 }
96
97
98
99
100
101
102 public boolean simplify() {
103 if (voc.isSatisfied(head) || voc.isSatisfied(tail)) {
104 return true;
105 }
106 return false;
107 }
108
109 public boolean propagate(UnitPropagationListener s, int p) {
110 voc.watch(p, this);
111 if (head == neg(p)) {
112 return s.enqueue(tail, this);
113 }
114 assert tail == neg(p);
115 return s.enqueue(head, this);
116 }
117
118
119
120
121 public boolean locked() {
122 return voc.getReason(head) == this || voc.getReason(tail) == this;
123 }
124
125
126
127
128 public double getActivity() {
129 return activity;
130 }
131
132 @Override
133 public String toString() {
134 StringBuffer stb = new StringBuffer();
135 stb.append(Lits.toString(head));
136 stb.append("[");
137 stb.append(voc.valueToString(head));
138 stb.append("]");
139 stb.append(" ");
140 stb.append(Lits.toString(tail));
141 stb.append("[");
142 stb.append(voc.valueToString(tail));
143 stb.append("]");
144 return stb.toString();
145 }
146
147
148
149
150
151
152
153
154
155 public int get(int i) {
156 if (i == 0)
157 return head;
158 assert i == 1;
159 return tail;
160 }
161
162
163
164
165 public void rescaleBy(double d) {
166 activity *= d;
167 }
168
169 public int size() {
170 return 2;
171 }
172
173 public void assertConstraint(UnitPropagationListener s) {
174 assert voc.isUnassigned(head);
175 boolean ret = s.enqueue(head, this);
176 assert ret;
177 }
178
179 public ILits getVocabulary() {
180 return voc;
181 }
182
183 public int[] getLits() {
184 int[] tmp = new int[2];
185 tmp[0] = head;
186 tmp[1] = tail;
187 return tmp;
188 }
189
190 @Override
191 public boolean equals(Object obj) {
192 if (obj == null)
193 return false;
194 try {
195 BinaryClause wcl = (BinaryClause) obj;
196 if (wcl.head != head || wcl.tail != tail) {
197 return false;
198 }
199 return true;
200 } catch (ClassCastException e) {
201 return false;
202 }
203 }
204
205 @Override
206 public int hashCode() {
207 long sum = head + tail;
208 return (int) sum / 2;
209 }
210
211 public void register() {
212 voc.watch(neg(head), this);
213 voc.watch(neg(tail), this);
214 }
215 }