Mercurial > hg > Applications > JavaLite
view src/sbdd/BDDSatisfier.java @ 67:4ced2af1ff09 bdd-order
BDD Order fix
author | kono |
---|---|
date | Sun, 13 Jan 2008 19:48:42 +0900 |
parents | 96b1c8c2f9b9 |
children | 416e4d272e79 |
line wrap: on
line source
package sbdd; import java.util.LinkedList; import verifier.Backtrack; import lite.BDDSolver; import lite.Continuation; import lite.ITLNodeFactory; import lite.ITLNodeFactoryInterface; import lite.ITLNodeParser; import lite.ITLSatisfier; import lite.ITLSolver; import lite.Next; public class BDDSatisfier extends ITLSatisfier { public ITLNodeParser<ITLSolver> p; public SBDDFactory sf; public LinkedList<SBDDEntry> queue; public SBDDSet state; /** * */ private static final long serialVersionUID = 1L; public void init() { lf = new ITLNodeFactory(); p = new ITLNodeParser<ITLSolver>((ITLNodeFactoryInterface<ITLSolver>) lf); sf = new SBDDFactory(); // empty = ITLNodeFactory.emptySolver; // empty = SBDDFactory.emptySolver; empty = lf.emptyNode(); } public BDDSatisfier() { init(); lf = new SBDDFactory(); true_ = SBDDFactory.trueSolver; false_ = SBDDFactory.falseSolver; state = sf.set(); state.getEntry(SBDDFactory.trueSolver).expanded = true; state.getEntry(SBDDFactory.falseSolver).expanded = true; state.getEntry(SBDDFactory.emptySolver).expanded = true; } public void showAllNext(String s) { ITLSolver n = p.parse(s); BDDSolver b = n.toSBDD(sf); System.out.println(b); develop(b, new Print()); // System.out.println(sf.hash); System.out.println(); } class Print implements Next { public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { System.out.println(" "+sat.choicePoint()+" -> "+value); throw sat.backtrack; } } public void showVerify(String s) { ITLSolver n = p.parse(s); BDDSolver b = n.toSBDD(sf); System.out.println(s); verify(b); // System.out.println(sf.hash); System.out.println(); } class AllNext implements Next { public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { if (value!=null) { SBDDEntry e = state.getEntry(value); if (e.expanded) { System.out.print((e.key==sat.true_)?"t":"."); } else { queue.add(e); e.expanded = true; System.out.print(e.id+" "); } } else { System.out.print("f"); } throw sat.backtrack; } } class AllNextVerbose implements Next { public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { String s = "null"; System.out.print(" "+sat.choicePoint()+" -> "); if (value!=null) { SBDDEntry e = state.getEntry(value); s = value.toString(); s = Integer.toString(e.id)+":"+s; if (e.expanded) { // skip } else { queue.add(e); e.expanded = true; s = "!"+s; } } System.out.println(s); throw sat.backtrack; } } public void verify(ITLSolver n) { queue = new LinkedList<SBDDEntry>(); Next allNext = verbose? new AllNextVerbose() : new AllNext(); SBDDEntry b = state.getEntry(n); if (b.expanded) { // already checked System.out.println(" already checked."); return; } queue.add(b); b.expanded = true; for(SBDDEntry e;(e = queue.poll())!=null; ) { System.out.println(e.id+":"+(verbose?e.key+"->":"")); develop(e.key, allNext); if (!verbose) System.out.println(); } } }