View Javadoc

1   /*******************************************************************************
2   * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
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 pseudo boolean algorithms described in:
20  * A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
21  * Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
22  * Volume 24, Issue 3, March 2005 Page(s): 305 - 317
23  * 
24  * and 
25  * Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL 
26  * Framework. Ph.D. Dissertation, University of Oregon.
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   * @author anne
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  	// coefs.get(lit)
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  	//coefs.containsKey(nLitImplied)
88  	boolean containsKey(int lit){
89  		return allLits.get(lit) != -1;
90  	}
91  		
92  	int size(){
93  		return lits.size();
94  	}
95  	
96  	//coefs.put(lit, newValue)
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 	//void removeCoef(Integer lit) {
115         //coefs.remove(lit);     
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 }