org.sat4j.pb.tools
Class ImplicationAnd<T,C>

java.lang.Object
  org.sat4j.pb.tools.ImplicationAnd<T,C>

Type Parameters:

T -

C -

public class ImplicationAnd<T,C>
extends java.lang.Object

That class is used to represent a conjunction of literals in the RHS of an implication.

Author:

daniel

Constructor Summary

ImplicationAnd(DependencyHelper<T,C> helper, IVecInt clause)

Method Summary

ImplicationAnd<T,C>	and(T thing) Add a new positive literal to the conjunction of literals.
ImplicationAnd<T,C>	andNot(T thing) Add a new negative literal to the conjunction of literals.
void	named(C name) "name" the constraint for the explanation.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ImplicationAnd

public ImplicationAnd(DependencyHelper<T,C> helper,
                      IVecInt clause)

Method Detail

and

public ImplicationAnd<T,C> and(T thing)
                        throws ContradictionException

Add a new positive literal to the conjunction of literals.

Parameters:

thing - a domain object

Returns:

a RHS conjunction of literals.

Throws:

ContradictionException

andNot

public ImplicationAnd<T,C> andNot(T thing)
                           throws ContradictionException

Add a new negative literal to the conjunction of literals.

Parameters:

thing - a domain object

Returns:

a RHS conjunction of literals.

Throws:

ContradictionException

named

public void named(C name)

"name" the constraint for the explanation. IT IS MANDATORY TO NAME ALL THE CONSTRAINTS!

Parameters:

name - an object to link to the constraint.