Commit 4a2113a7 authored by leberre's avatar leberre

Updated javadoc of the dependency manager.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@288 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 2aa707de
......@@ -59,6 +59,12 @@ public class DependencyHelper<T,C> {
final XplainPB xplain;
/**
*
* @param solver the solver to be used to solve the problem.
* @param maxvarid an upper bound of the expected number of objects to be used
* in the constraints.
*/
public DependencyHelper(IPBSolver solver, int maxvarid) {
this.xplain = new XplainPB(solver);
xplain.newVar(maxvarid);
......@@ -66,6 +72,11 @@ public class DependencyHelper<T,C> {
mapToDomain.push(null);
}
/**
* Translate a domain object into a dimacs variable.
* @param thing a domain object
* @return the dimacs variable (an integer) representing that domain object.
*/
int getIntValue(T thing) {
Integer intValue = mapToDimacs.get(thing);
if (intValue == null) {
......@@ -76,6 +87,15 @@ public class DependencyHelper<T,C> {
return intValue;
}
/**
* Retrieve the solution found.
*
* THAT METHOD IS EXPECTED TO BE CALLED IF hasASolution() RETURNS TRUE.
*
* @return the domain object that must be satisfied to satisfy the constraints
* entered in the solver.
* @see {@link #hasASolution()}
*/
public IVec<T> getSolution() {
int[] model = xplain.model();
IVec<T> toInstall = new Vec<T>();
......@@ -87,10 +107,24 @@ public class DependencyHelper<T,C> {
return toInstall;
}
/**
*
* @return true if the set of constraints entered inside the solver can be satisfied.
* @throws TimeoutException
*/
public boolean hasASolution() throws TimeoutException {
return xplain.isSatisfiable();
}
/**
* Explain the reason of the inconsistency of the set of constraints.
*
* THAT METHOD IS EXPECTED TO BE CALLED IF hasASolution() RETURNS FALSE.
*
* @return a set of objects used to "name" each constraint entered in the solver.
* @throws TimeoutException
* @see {@link #hasASolution()}
*/
public Set<C> why() throws TimeoutException {
IVecInt explanation = xplain.explain();
Set<C> ezexplain = new TreeSet<C>();
......@@ -100,12 +134,26 @@ public class DependencyHelper<T,C> {
return ezexplain;
}
/**
* Explain a domain object has been set to true in a solution.
*
* @return a set of objects used to "name" each constraint entered in the solver.
* @throws TimeoutException
* @see {@link #hasASolution()}
*/
public Set<C> why(T thing) throws TimeoutException {
IVecInt assumps = new VecInt();
assumps.push(-getIntValue(thing));
return why(assumps);
}
/**
* Explain a domain object has been set to false in a solution.
*
* @return a set of objects used to "name" each constraint entered in the solver.
* @throws TimeoutException
* @see {@link #hasASolution()}
*/
public Set<C> whyNot(T thing) throws TimeoutException {
IVecInt assumps = new VecInt();
assumps.push(getIntValue(thing));
......@@ -124,6 +172,13 @@ public class DependencyHelper<T,C> {
return ezexplain;
}
/**
* Add a constraint to set the value of a domain object to true.
*
* @param thing the domain object
* @param name the name of the constraint, to be used in an explanation if needed.
* @throws ContradictionException if the set of constraints appears to be trivially inconsistent.
*/
public void setTrue(T thing, C name) throws ContradictionException {
IVecInt clause = new VecInt();
clause.push(getIntValue(thing));
......@@ -131,6 +186,13 @@ public class DependencyHelper<T,C> {
descs.push(name);
}
/**
* Add a constraint to set the value of a domain object to false.
*
* @param thing the domain object
* @param name the name of the constraint, to be used in an explanation if needed.
* @throws ContradictionException if the set of constraints appears to be trivially inconsistent.
*/
public void setFalse(T thing, C name) throws ContradictionException {
IVecInt clause = new VecInt();
clause.push(-getIntValue(thing));
......@@ -138,6 +200,12 @@ public class DependencyHelper<T,C> {
descs.push(name);
}
/**
* Create a logical implication of the form lhs -> rhs
*
* @param lhs some domain objects. They form a conjunction in the left hand side of the implication.
* @return the right hand side of the implication.
*/
public ImplicationRHS<T,C> implication(T... lhs) {
IVecInt clause = new VecInt();
for (T t : lhs) {
......@@ -146,6 +214,14 @@ public class DependencyHelper<T,C> {
return new ImplicationRHS<T,C>(this, clause);
}
/**
* Create a constraint stating that at most i domain object should be set to true.
*
* @param i the maximum number of domain object to set to true.
* @param things the domain objects.
* @return an object used to name the constraint. The constraint MUST BE NAMED.
* @throws ContradictionException
*/
public ImplicationNamer<T,C> atMost(int i, T... things)
throws ContradictionException {
IVec<IConstr> toName = new Vec<IConstr>();
......@@ -157,6 +233,11 @@ public class DependencyHelper<T,C> {
return new ImplicationNamer<T,C>(this, toName);
}
/**
* Add an objective function to ask for a solution that minimize the objective function.
*
* @param wobj a set of weighted objects (pairs of domain object and BigInteger).
*/
public void setObjectiveFunction(WeightedObject<T> ... wobj) {
IVecInt literals = new VecInt(wobj.length);
IVec<BigInteger> coefs = new Vec<BigInteger>(wobj.length);
......
......@@ -28,6 +28,14 @@ import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
/**
* That class is used to represent a conjunction of literals in the RHS of an implication.
*
* @author daniel
*
* @param <T>
* @param <C>
*/
public class ImplicationAnd<T,C> {
private final DependencyHelper<T,C> helper;
private final IVecInt clause;
......@@ -38,6 +46,12 @@ public class ImplicationAnd<T,C> {
this.helper = helper;
}
/**
* Add a new positive literal to the conjunction of literals.
* @param thing a domain object
* @return a RHS conjunction of literals.
* @throws ContradictionException
*/
public ImplicationAnd<T,C> and(T thing) throws ContradictionException {
IVecInt tmpClause = new VecInt();
clause.copyTo(tmpClause);
......@@ -46,6 +60,12 @@ public class ImplicationAnd<T,C> {
return this;
}
/**
* Add a new negative literal to the conjunction of literals.
* @param thing a domain object
* @return a RHS conjunction of literals.
* @throws ContradictionException
*/
public ImplicationAnd<T,C> andNot(T thing) throws ContradictionException {
IVecInt tmpClause = new VecInt();
clause.copyTo(tmpClause);
......@@ -54,6 +74,13 @@ public class ImplicationAnd<T,C> {
return this;
}
/**
* "name" the constraint for the explanation.
*
* IT IS MANDATORY TO NAME ALL THE CONSTRAINTS!
*
* @param name an object to link to the constraint.
*/
public void named(C name) {
for (Iterator<IConstr> it = toName.iterator(); it.hasNext();) {
helper.constrs.push(it.next());
......
......@@ -25,6 +25,15 @@ import org.sat4j.core.Vec;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
/**
* That class is used to associate each constraint with another object that
* must be used to represent it in an explanation.
*
* @author daniel
*
* @param <T>
* @param <C>
*/
public class ImplicationNamer<T,C> {
private final DependencyHelper<T,C> helper;
......@@ -35,6 +44,11 @@ public class ImplicationNamer<T,C> {
this.helper = helper;
}
/**
* Associate the current constraint with a specific object that
* will be used to represent it in an explanation.
* @param name
*/
public void named(C name) {
for (Iterator<IConstr> it = toName.iterator();it.hasNext();) {
helper.constrs.push(it.next());
......
......@@ -25,6 +25,14 @@ import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
/**
* That class represents the RHS of an implication.
*
* @author daniel
*
* @param <T>
* @param <C>
*/
public class ImplicationRHS<T,C> {
private IVecInt clause;
......@@ -37,12 +45,26 @@ public class ImplicationRHS<T,C> {
this.helper = helper;
}
/**
* Build an implication with a conjunction of literals in the RHS.
*
* @param thing a domain object that will appear positively.
* @return a RHS conjunction of literals.
* @throws ContradictionException
*/
public ImplicationAnd<T,C> implies(T thing) throws ContradictionException {
ImplicationAnd<T,C> and = new ImplicationAnd<T,C>(helper, clause);
and.and(thing);
return and;
}
/**
* Build an implication with a disjunction of literals in the RHS.
*
* @param thing a domain object
* @return an object used to name the constraint. The constraint MUST BE NAMED.
* @throws ContradictionException
*/
public ImplicationNamer<T,C> implies(T... things)
throws ContradictionException {
for (T t : things) {
......@@ -52,6 +74,13 @@ public class ImplicationRHS<T,C> {
return new ImplicationNamer<T,C>(helper, toName);
}
/**
* Build an implication with a conjunction of literals in the RHS.
*
* @param thing a domain object that will appear negatively.
* @return a RHS conjunction of literals.
* @throws ContradictionException
*/
public ImplicationAnd<T,C> impliesNot(T thing) throws ContradictionException {
ImplicationAnd<T,C> and = new ImplicationAnd<T,C>(helper, clause);
and.andNot(thing);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment