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
20 package org.sat4j.pb.tools;
21
22 import java.util.Iterator;
23
24 import org.sat4j.core.Vec;
25 import org.sat4j.core.VecInt;
26 import org.sat4j.specs.ContradictionException;
27 import org.sat4j.specs.IConstr;
28 import org.sat4j.specs.IVec;
29 import org.sat4j.specs.IVecInt;
30
31 /**
32 * That class is used to represent a conjunction of literals in the RHS of an
33 * implication.
34 *
35 * @author daniel
36 *
37 * @param <T>
38 * @param <C>
39 */
40 public class ImplicationAnd<T, C> {
41 private final DependencyHelper<T, C> helper;
42 private final IVecInt clause;
43 private final IVec<IConstr> toName = new Vec<IConstr>();
44
45 public ImplicationAnd(DependencyHelper<T, C> helper, IVecInt clause) {
46 this.clause = clause;
47 this.helper = helper;
48 }
49
50 /**
51 * Add a new positive literal to the conjunction of literals.
52 *
53 * @param thing
54 * a domain object
55 * @return a RHS conjunction of literals.
56 * @throws ContradictionException
57 */
58 public ImplicationAnd<T, C> and(T thing) throws ContradictionException {
59 IVecInt tmpClause = new VecInt();
60 clause.copyTo(tmpClause);
61 tmpClause.push(helper.getIntValue(thing));
62 toName.push(helper.solver.addClause(tmpClause));
63 return this;
64 }
65
66 /**
67 * Add a new negative literal to the conjunction of literals.
68 *
69 * @param thing
70 * a domain object
71 * @return a RHS conjunction of literals.
72 * @throws ContradictionException
73 */
74 public ImplicationAnd<T, C> andNot(T thing) throws ContradictionException {
75 IVecInt tmpClause = new VecInt();
76 clause.copyTo(tmpClause);
77 tmpClause.push(-helper.getIntValue(thing));
78 toName.push(helper.solver.addClause(tmpClause));
79 return this;
80 }
81
82 /**
83 * "name" the constraint for the explanation.
84 *
85 * IT IS MANDATORY TO NAME ALL THE CONSTRAINTS!
86 *
87 * @param name
88 * an object to link to the constraint.
89 */
90 public void named(C name) {
91 for (Iterator<IConstr> it = toName.iterator(); it.hasNext();) {
92 helper.descs.put(it.next(), name);
93 }
94 }
95 }