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