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 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  *******************************************************************************/
28  package org.sat4j.minisat.constraints;
29  
30  import java.io.Serializable;
31  
32  import org.sat4j.core.Vec;
33  import org.sat4j.minisat.core.Constr;
34  import org.sat4j.minisat.core.DataStructureFactory;
35  import org.sat4j.minisat.core.ILits;
36  import org.sat4j.minisat.core.Learner;
37  import org.sat4j.minisat.core.Propagatable;
38  import org.sat4j.minisat.core.UnitPropagationListener;
39  import org.sat4j.specs.ContradictionException;
40  import org.sat4j.specs.IVec;
41  import org.sat4j.specs.IVecInt;
42  
43  /**
44   * @author leberre To change the template for this generated type comment go to
45   *         Window>Preferences>Java>Code Generation>Code and Comments
46   */
47  public abstract class AbstractDataStructureFactory implements
48          DataStructureFactory, Serializable {
49  
50      /**
51  	 * 
52  	 */
53  	private static final long serialVersionUID = 1L;
54  
55  	/*
56       * (non-Javadoc)
57       * 
58       * @see org.sat4j.minisat.core.DataStructureFactory#conflictDetectedInWatchesFor(int)
59       */
60      public void conflictDetectedInWatchesFor(int p, int i) {
61          for (int j = i + 1; j < tmp.size(); j++) {
62              lits.watch(p, tmp.get(j));
63          }
64      }
65  
66      /*
67       * (non-Javadoc)
68       * 
69       * @see org.sat4j.minisat.core.DataStructureFactory#getWatchesFor(int)
70       */
71      public IVec<Propagatable> getWatchesFor(int p) {
72          tmp.clear();
73          lits.watches(p).moveTo(tmp);
74          return tmp;
75      }
76  
77      protected ILits lits;
78      
79      protected AbstractDataStructureFactory() {
80          lits = createLits();
81      }
82  
83      protected abstract ILits createLits(); 
84      
85      private final IVec<Propagatable> tmp = new Vec<Propagatable>();
86  
87      /*
88       * (non-Javadoc)
89       * 
90       * @see org.sat4j.minisat.DataStructureFactory#createVocabulary()
91       */
92      public ILits getVocabulary() {
93          return lits;
94      }
95  
96      protected UnitPropagationListener solver;
97  
98      protected Learner learner;
99  
100     public void setUnitPropagationListener(UnitPropagationListener s) {
101         solver = s;
102     }
103 
104     public void setLearner(Learner learner) {
105         this.learner = learner;
106     }
107 
108     public void reset() {
109     }
110 
111     public void learnConstraint(Constr constr) {
112         learner.learn(constr);
113     }
114 
115     /*
116      * (non-Javadoc)
117      * 
118      * @see org.sat4j.minisat.core.DataStructureFactory#createCardinalityConstraint(org.sat4j.specs.VecInt,
119      *      int)
120      */
121     public Constr createCardinalityConstraint(IVecInt literals, int degree)
122             throws ContradictionException {
123         throw new UnsupportedOperationException();
124     }
125 }