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 IConstr constr = helper.solver.addClause(tmpClause);
63 if (constr != null) {
64 toName.push(constr);
65 }
66 return this;
67 }
68
69 /**
70 * Add a new negative literal to the conjunction of literals.
71 *
72 * @param thing
73 * a domain object
74 * @return a RHS conjunction of literals.
75 * @throws ContradictionException
76 */
77 public ImplicationAnd<T, C> andNot(T thing) throws ContradictionException {
78 IVecInt tmpClause = new VecInt();
79 clause.copyTo(tmpClause);
80 tmpClause.push(-helper.getIntValue(thing));
81 IConstr constr = helper.solver.addClause(tmpClause);
82 if (constr != null) {
83 toName.push(constr);
84 }
85 return this;
86 }
87
88 /**
89 * "name" the constraint for the explanation.
90 *
91 * IT IS MANDATORY TO NAME ALL THE CONSTRAINTS!
92 *
93 * @param name
94 * an object to link to the constraint.
95 */
96 public void named(C name) {
97 for (Iterator<IConstr> it = toName.iterator(); it.hasNext();) {
98 helper.descs.put(it.next(), name);
99 }
100 }
101 }