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