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 for (IteratorInt it = literals.iterator(); it.hasNext();) {
30 p = it.next();
31 clause.push(p);
32 toName.push(helper.solver.addClause(clause));
33 clause.remove(p);
34 }
35 return new ImplicationNamer<T, C>(helper, toName);
36 }
37 }