1 package org.sat4j.pb.tools;
2
3 import org.sat4j.core.Vec;
4 import org.sat4j.core.VecInt;
5 import org.sat4j.specs.ContradictionException;
6 import org.sat4j.specs.IConstr;
7 import org.sat4j.specs.IVec;
8 import org.sat4j.specs.IVecInt;
9 import org.sat4j.specs.IteratorInt;
10
11 public class DisjunctionRHS<T, C> {
12 private final IVecInt literals;
13 private final DependencyHelper<T, C> helper;
14
15 private final IVec<IConstr> toName = new Vec<IConstr>();
16
17 public DisjunctionRHS(DependencyHelper<T, C> helper, IVecInt literals) {
18 this.literals = literals;
19 this.helper = helper;
20 }
21
22 public ImplicationNamer<T, C> implies(T... things)
23 throws ContradictionException {
24 IVecInt clause = new VecInt();
25 for (T t : things) {
26 clause.push(helper.getIntValue(t));
27 }
28 int p;
29 IConstr constr;
30 for (IteratorInt it = literals.iterator(); it.hasNext();) {
31 p = it.next();
32 clause.push(p);
33 constr = helper.solver.addClause(clause);
34 if (constr == null) {
35 throw new IllegalStateException(
36 "Constraints are not supposed to be null when using the helper");
37 }
38 toName.push(constr);
39 clause.remove(p);
40 }
41 return new ImplicationNamer<T, C>(helper, toName);
42 }
43 }