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
29
30 package org.sat4j.pb.constraints.pb;
31
32 import java.math.BigInteger;
33
34 import org.sat4j.core.Vec;
35 import org.sat4j.core.VecInt;
36 import org.sat4j.specs.IVec;
37 import org.sat4j.specs.IVecInt;
38
39
40
41
42
43 public class InternalMapPBStructure {
44
45 IVecInt lits;
46 IVec<BigInteger> coefs;
47 IVecInt allLits;
48
49 InternalMapPBStructure(int size) {
50 assert size > 0;
51 this.allLits = new VecInt(size, -1);
52 this.coefs = new Vec<BigInteger>();
53 this.lits = new VecInt();
54 }
55
56 InternalMapPBStructure(PBConstr cpb) {
57 this.allLits = new VecInt(cpb.getVocabulary().nVars() * 2 + 2, -1);
58 this.coefs = new Vec<BigInteger>(cpb.size());
59 this.lits = new VecInt(cpb.size());
60 int lit;
61 for (int i = 0; i < cpb.size(); i++) {
62 assert cpb.get(i) != 0;
63 assert cpb.getCoef(i).signum() > 0;
64 lit = cpb.get(i);
65 this.lits.push(lit);
66 assert i + 1 == this.lits.size();
67 this.allLits.set(lit, i);
68 this.coefs.push(cpb.getCoef(i));
69 }
70 }
71
72
73 BigInteger get(int lit) {
74 assert this.allLits.get(lit) != -1;
75 return this.coefs.get(this.allLits.get(lit));
76 }
77
78 int getLit(int indLit) {
79 assert indLit < this.lits.size();
80 return this.lits.get(indLit);
81 }
82
83 BigInteger getCoef(int indLit) {
84 assert indLit < this.coefs.size();
85 return this.coefs.get(indLit);
86 }
87
88
89 boolean containsKey(int lit) {
90 return this.allLits.get(lit) != -1;
91 }
92
93 int size() {
94 return this.lits.size();
95 }
96
97
98 void put(int lit, BigInteger newValue) {
99 int indLit = this.allLits.get(lit);
100 if (indLit != -1) {
101 this.coefs.set(indLit, newValue);
102 } else {
103 this.lits.push(lit);
104 this.coefs.push(newValue);
105 this.allLits.set(lit, this.lits.size() - 1);
106 }
107 }
108
109 void changeCoef(int indLit, BigInteger newValue) {
110 assert indLit <= this.coefs.size();
111 this.coefs.set(indLit, newValue);
112 }
113
114
115
116 void remove(int lit) {
117 int indLit = this.allLits.get(lit);
118 if (indLit != -1) {
119 int tmp = this.lits.last();
120 this.coefs.delete(indLit);
121 this.lits.delete(indLit);
122 this.allLits.set(tmp, indLit);
123 this.allLits.set(lit, -1);
124 }
125 }
126
127 void copyCoefs(IVec<BigInteger> dest) {
128 this.coefs.copyTo(dest);
129 }
130
131 void copyCoefs(BigInteger[] dest) {
132 this.coefs.copyTo(dest);
133 }
134
135 void copyLits(IVecInt dest) {
136 this.lits.copyTo(dest);
137 }
138
139 void copyLits(int[] dest) {
140 this.lits.copyTo(dest);
141 }
142 }