Adding support for ElementFunction
[satune.git] / design / notes.txt
1 (1) Elements/BooleanVars should link back to expressions that use them
2 --> Done
3
4 (2) Need to introduce variables in encoding of functions....
5 --> Done
6
7 (3) Some cases can do variable elimination of introduced variables...
8
9 (4) Might need to indicate what variables we can query about in
10 future?
11
12 (5) Could simplify output of functions...  Maybe several outputs have
13 same effect...
14
15
16 Work/Passes:
17
18 (1) TreeConstruction --- need backwards links...
19 BooleanVar/ElementVar should be able to query all of its uses.  Should
20 go all the way up...
21
22 (2) Naive Encoding Pass --- add an encoding to every Element/Function...
23
24 (3) Encoder Pass --- implement encodings into constraint objects...
25
26 (4) Test...  Make sure the thing works...
27
28 Next basic implementation phase:
29 (1) Extend Naive Encoder Pass to test other encodings
30 (2) Build more clever function encodings strategies (e.g., equals, add, etc)...
31 (3) Test
32
33 Actual research:
34
35 (1) TreeRewriting --- probably should do Equivalent Subexpression
36 Elimination (Don't have the same expression appear twice, instead
37 simply link to it again).  Possibly good to do in TreeConstruction...
38 This could be lower priority as it isn't really essential to make
39 things work.  Should also probably be switchable on/off...
40
41 --> Done
42
43 (2) Advanced TreeRewriting --- can rewrite functions/predicates to
44 eliminate unused entries or to eliminate effectively identical
45 outputs...  e.g., consider a function f() that can output the values
46 1,3, 5, 7, and its output is only ever compared to 3...  We could
47 rewrite the values 1, 5, and 7 to be the same value.
48
49 (3) Advanced Encoding Strategies
50   a) encoding alignment --- making binary index encodings over
51 different sets work together
52
53   b) Implement K-Map for function encoding
54
55 (4) Implement search framework --- probably simulated annealing over a
56 population of strategies...  search framework should probably be able
57 to turn on/off nearly any optimization we have...
58
59 (5) Implement backend translation strategies....do optimizations and
60 implement other simplifcation strategies
61
62 (6) Convert SATCheck to use Constraint Compiler...not sure about order...
63 Started...
64
65 (7) Profile system....
66
67 ---------------------------------------------------------------------
68
69 To do:
70
71 (0) Support for saving/loading problem instances...
72
73 (1) Complete satcheck support
74
75 (2) Advance tree rewriting...  Variable value elimination...
76
77 (3) Think about undefined semantics...
78
79 (4) Smart encoding...
80     Variable Graphs....
81
82     Split graph into connected components
83
84 Encoding ideas:
85 *    Monotonic increasing index
86 *    Matched index (equality)
87 *    Bit exposes
88 *    Single var
89 *    Support arithmetic
90 *    Sparse encoding
91
92 --------------------------------------------------------------------
93
94