View Javadoc

1   /*******************************************************************************
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
3    *
4    * All rights reserved. This program and the accompanying materials
5    * are made available under the terms of the Eclipse Public License v1.0
6    * which accompanies this distribution, and is available at
7    *  http://www.eclipse.org/legal/epl-v10.html
8    *
9    * Alternatively, the contents of this file may be used under the terms of
10   * either the GNU Lesser General Public License Version 2.1 or later (the
11   * "LGPL"), in which case the provisions of the LGPL are applicable instead
12   * of those above. If you wish to allow use of your version of this file only
13   * under the terms of the LGPL, and not to allow others to use your version of
14   * this file under the terms of the EPL, indicate your decision by deleting
15   * the provisions above and replace them with the notice and other provisions
16   * required by the LGPL. If you do not delete the provisions above, a recipient
17   * may use your version of this file under the terms of the EPL or the LGPL.
18   *
19   * Based on the original MiniSat specification from:
20   *
21   * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22   * Sixth International Conference on Theory and Applications of Satisfiability
23   * Testing, LNCS 2919, pp 502-518, 2003.
24   *
25   * See www.minisat.se for the original solver in C++.
26   *
27   * Contributors:
28   *   CRIL - initial API and implementation
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   * @author anne
41   * 
42   */
43  public class InternalMapPBStructure {
44  
45      private final IVecInt lits;
46      private final IVec<BigInteger> coefs;
47      private IVecInt allLits;
48  
49      // temporarily : just for the case where an InternalMapPBStructure
50      // is used to embed in one object literals and coefs
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 }