1 |
| |
2 |
| |
3 |
| |
4 |
| |
5 |
| |
6 |
| |
7 |
| package org.sat4j.minisat.constraints.cnf; |
8 |
| |
9 |
| import org.sat4j.minisat.core.ILits23; |
10 |
| |
11 |
| |
12 |
| |
13 |
| |
14 |
| |
15 |
| public class Lits23 extends Lits2 implements ILits23 { |
16 |
| |
17 |
| private static final long serialVersionUID = 1L; |
18 |
| |
19 |
| private TernaryClauses[] ternclauses = null; |
20 |
| |
21 |
| |
22 |
| |
23 |
| |
24 |
106
| public Lits23() {
|
25 |
106
| super();
|
26 |
| } |
27 |
| |
28 |
33972
| private void register(int p, int q, int r) {
|
29 |
| assert p > 1; |
30 |
| assert q > 1; |
31 |
| assert r > 1; |
32 |
| |
33 |
33972
| if (ternclauses == null) {
|
34 |
84
| ternclauses = new TernaryClauses[2 * nVars() + 2];
|
35 |
| } |
36 |
33972
| if (ternclauses[p] == null) {
|
37 |
11574
| ternclauses[p] = new TernaryClauses(this, p);
|
38 |
11574
| watches[p ^ 1].push(ternclauses[p]);
|
39 |
| } |
40 |
33972
| ternclauses[p].addTernaryClause(q, r);
|
41 |
| } |
42 |
| |
43 |
11324
| public void ternaryClauses(int lit1, int lit2, int lit3) {
|
44 |
11324
| register(lit1, lit2, lit3);
|
45 |
11324
| register(lit2, lit1, lit3);
|
46 |
11324
| register(lit3, lit1, lit2);
|
47 |
| } |
48 |
| |
49 |
951557146
| public int nTernaryClauses(int p) {
|
50 |
951557146
| if (ternclauses == null) {
|
51 |
951310152
| return 0;
|
52 |
| } |
53 |
246994
| if (ternclauses[p] == null) {
|
54 |
12923
| return 0;
|
55 |
| } |
56 |
234071
| return ternclauses[p].size();
|
57 |
| } |
58 |
| } |