notes.txt

   1 (1) Elements/BooleanVars should link back to expressions that use them
   2
   3 (2) Need to introduce variables in encoding of functions....
   4
   5 (3) Some cases can do variable elimination of introduced variables...
   6
   7 (4) Might need to indicate what variables we can query about in
   8 future?
   9
  10 (5) Could simplify output of functions...  Maybe several outputs have
  11 same effect...
  12
  13
  14 Work/Passes:
  15
  16 (1) TreeConstruction --- need backwards links...
  17 BooleanVar/ElementVar should be able to query all of its uses.  Should
  18 go all the way up...
  19
  20 (2) Naive Encoding Pass --- add an encoding to every Element/Function...
  21
  22 (3) Encoder Pass --- implement encodings into constraint objects...
  23
  24 (4) Test...  Make sure the thing works...
  25
  26 Next basic implementation phase:
  27 (1) Extend Naive Encoder Pass to test other encodings
  28 (2) Build more clever function encodings strategies (e.g., equals, add, etc)...
  29 (3) Test
  30
  31 Actual research:
  32
  33 (1) TreeRewriting --- probably should do Equivalent Subexpression
  34 Elimination (Don't have the same expression appear twice, instead
  35 simply link to it again).  Possibly good to do in TreeConstruction...
  36 This could be lower priority as it isn't really essential to make
  37 things work.  Should also probably be switchable on/off...
  38
  39 (2) Advanced TreeRewriting --- can rewrite functions/predicates to
  40 eliminate unused entries or to eliminate effectively identical
  41 outputs...  e.g., consider a function f() that can output the values
  42 1,3, 5, 7, and its output is only ever compared to 3...  We could
  43 rewrite the values 1, 5, and 7 to be the same value.
  44
  45 (3) Advanced Encoding Strategies
  46   a) encoding alignment --- making binary index encodings over
  47 different sets work together
  48
  49   b) Implement K-Map for function encoding
  50
  51 (4) Implement search framework --- probably simulated annealing over a
  52 population of strategies...  search framework should probably be able
  53 to turn on/off nearly any optimization we have...
  54
  55 (5) Implement backend translation strategies....do optimizations and
  56 implement other simplifcation strategies
  57
  58 (6) Convert SATCheck to use Constraint Compiler...not sure about order...
  59
  60 (7) Profile system....