|
49
|
1 package sbdd;
|
|
|
2
|
|
55
|
3 import java.util.LinkedList;
|
|
49
|
4
|
|
|
5
|
|
55
|
6 import verifier.Backtrack;
|
|
|
7 import lite.BDDSolver;
|
|
|
8 import lite.Continuation;
|
|
|
9 import lite.ITLNodeFactory;
|
|
|
10 import lite.ITLNodeFactoryInterface;
|
|
|
11 import lite.ITLNodeParser;
|
|
49
|
12 import lite.ITLSatisfier;
|
|
|
13 import lite.ITLSolver;
|
|
55
|
14 import lite.Next;
|
|
49
|
15
|
|
|
16 public class BDDSatisfier extends ITLSatisfier {
|
|
|
17
|
|
|
18
|
|
55
|
19 public ITLNodeParser<ITLSolver> p;
|
|
|
20 public SBDDFactory sf;
|
|
|
21
|
|
|
22 public LinkedList<SBDDEntry> queue;
|
|
|
23 public SBDDSet state;
|
|
|
24
|
|
49
|
25 /**
|
|
|
26 *
|
|
|
27 */
|
|
|
28 private static final long serialVersionUID = 1L;
|
|
|
29
|
|
55
|
30
|
|
|
31 public void init() {
|
|
|
32 lf = new ITLNodeFactory();
|
|
|
33 p = new ITLNodeParser<ITLSolver>((ITLNodeFactoryInterface<ITLSolver>) lf);
|
|
|
34 sf = new SBDDFactory();
|
|
|
35 // empty = ITLNodeFactory.emptySolver;
|
|
|
36 // empty = SBDDFactory.emptySolver;
|
|
|
37 empty = lf.emptyNode();
|
|
|
38 }
|
|
|
39
|
|
|
40 public BDDSatisfier() {
|
|
|
41 init();
|
|
49
|
42 lf = new SBDDFactory();
|
|
55
|
43 true_ = SBDDFactory.trueSolver;
|
|
58
|
44 state = sf.set();
|
|
|
45 state.getEntry(SBDDFactory.trueSolver).expanded = true;
|
|
|
46 state.getEntry(SBDDFactory.falseSolver).expanded = true;
|
|
|
47 state.getEntry(SBDDFactory.emptySolver).expanded = true;
|
|
49
|
48 }
|
|
|
49
|
|
55
|
50 public void showAllNext(String s) {
|
|
|
51 ITLSolver n = p.parse(s);
|
|
|
52 BDDSolver b = n.toSBDD(sf);
|
|
|
53 System.out.println(b);
|
|
|
54 develop(b, new Print());
|
|
|
55 // System.out.println(sf.hash);
|
|
|
56 System.out.println();
|
|
|
57 }
|
|
|
58
|
|
|
59 class Print implements Next {
|
|
|
60 public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
|
|
|
61 System.out.println(" "+sat.choicePoint()+" -> "+value);
|
|
|
62 throw sat.backtrack;
|
|
|
63 }
|
|
|
64 }
|
|
|
65
|
|
|
66
|
|
|
67 public void showVerify(String s) {
|
|
|
68 ITLSolver n = p.parse(s);
|
|
|
69 BDDSolver b = n.toSBDD(sf);
|
|
56
|
70 System.out.println(s);
|
|
55
|
71 verify(b);
|
|
|
72 // System.out.println(sf.hash);
|
|
|
73 System.out.println();
|
|
|
74 }
|
|
|
75
|
|
|
76
|
|
|
77 class AllNext implements Next {
|
|
|
78 public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
|
|
|
79 System.out.print(" "+sat.choicePoint()+" -> "+value);
|
|
|
80 if (value!=null) {
|
|
|
81 SBDDEntry e = state.getEntry(value);
|
|
58
|
82 if (e.expanded) {
|
|
55
|
83 // skip
|
|
|
84 } else {
|
|
|
85 queue.add(e);
|
|
|
86 System.out.print("!");
|
|
|
87 }
|
|
|
88 }
|
|
|
89 System.out.println();
|
|
|
90 throw sat.backtrack;
|
|
|
91 }
|
|
|
92 }
|
|
|
93
|
|
|
94 public void verify(ITLSolver n) {
|
|
|
95 queue = new LinkedList<SBDDEntry>();
|
|
|
96 AllNext allNext = new AllNext();
|
|
56
|
97 SBDDEntry b = state.getEntry(n);
|
|
62
|
98 this.clear(); // if not empty something wrong
|
|
58
|
99 if (b.expanded) {
|
|
|
100 // already checked
|
|
|
101 System.out.println(" already checked.");
|
|
|
102 return;
|
|
|
103 }
|
|
56
|
104 queue.add(b);
|
|
55
|
105 for(SBDDEntry e;(e = queue.poll())!=null; ) {
|
|
|
106 if (e.expanded) continue;
|
|
|
107 e.expanded = true;
|
|
|
108 System.out.println(e.key+"->");
|
|
|
109 develop(e.key, allNext);
|
|
|
110 }
|
|
|
111 }
|
|
|
112
|
|
49
|
113
|
|
|
114 }
|
