Mercurial > hg > Applications > JavaLite
view src/lite/OrSolver.java @ 107:30e74062f06c continuation-removal
*** empty log message ***
author | kono |
---|---|
date | Sun, 20 Jan 2008 18:22:55 +0900 |
parents | 0258fcdf488c |
children |
line wrap: on
line source
package lite; import sbdd.SBDDFactoryInterface; public class OrSolver extends ITLSolver { ITLSolver left; ITLSolver right; public OrSolver(ITLSolver left, ITLSolver right) { this.left = left; this.right = right; } public String toString() { return "("+left+" or "+right+")"; } class OrSolver2 implements Next { Next next; ITLSolver residue; public OrSolver2(Next next,ITLSolver value) { residue = value; this.next = next; } public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack { if (value==null) { return next.next(sat,residue); } else if (value==sat.true_) { return next.next(sat,value); } else { return next.next(sat,sat.lf.orNode(residue,value)); } } } public BDDSolver toSBDD(SBDDFactoryInterface sf) { return left.toSBDD(sf).or(sf, right.toSBDD(sf)).toSBDD(sf); } class OrSolver1 implements Next { Next next; public OrSolver1(Next next) { this.next = next; } public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack { if (value==null) { return right.sat(sat, next); } else if (value==sat.true_) { return next.next(sat,value); } else { return right.sat(sat, new OrSolver2(next,value)); } } } @Override public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack { return left.sat(sat, new OrSolver1(next)); } }