ClassCastException when a class implements Propagatable but not Constr watches a conflicting literal
While experimenting with some new constraint types I've run into the situation where a constraint looks at several gruop of literals. For that, each group has it's own class that watches for propagation and undo of their literals.
Since watches require that a class implements interface Propagatable, everything looks fine, but I'm havng problems when one of the watched literals is identidfied as part of a conflict.
The offending lines are located in Solver.java around line 1025: {noformat} public Constr propagate() { ... qhead = ltrail.size(); // propQ.clear(); // FIXME enlever le transtypage return (Constr) lwatched.get(i); ... } {noformat} There, a Propagatable from the watch list is cast to Constr to return the conflicting clause.
As a workaround, I've added a new method to Propagatable: {noformat} /** * Returns the associated constraint with this object. Used for conflict analisys */ Constr associatedConstraint(); {noformat} then I modified all the existing clauses to define this method as returning this: {noformat} public Constr associatedConstraint() { return this; } {noformat} and finally modified Solver to use the new method. {noformat} public Constr propagate() { ... qhead = ltrail.size(); // propQ.clear(); return lwatched.get(i).associatedConstraint(); ... } {noformat}
This works fine for the ocnstraints I'm defining, but it will be great if SAT4J can support this case by default, as the API implies.