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