X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=design%2Fnotes.txt;h=f7282be8883bf8bad2ba8e2c1809646ef6ad41df;hp=1159c96aa11a37202a54f6cb49c2bdbfa280bf65;hb=9a515eb218f2788ee13b88dc84f3c14bfcf731ef;hpb=5249fbe7415e60c2e0411c64031d8a60aa7cd09f

diff --git a/design/notes.txt b/design/notes.txt
index 1159c96..f7282be 100644
--- a/design/notes.txt
+++ b/design/notes.txt
@@ -1,8 +1,94 @@
 (1) Elements/BooleanVars should link back to expressions that use them
+--> Done
 
 (2) Need to introduce variables in encoding of functions....
+--> Done
 
 (3) Some cases can do variable elimination of introduced variables...
 
 (4) Might need to indicate what variables we can query about in
 future?
+
+(5) Could simplify output of functions...  Maybe several outputs have
+same effect...
+
+
+Work/Passes:
+
+(1) TreeConstruction --- need backwards links...
+BooleanVar/ElementVar should be able to query all of its uses.  Should
+go all the way up...
+
+(2) Naive Encoding Pass --- add an encoding to every Element/Function...
+
+(3) Encoder Pass --- implement encodings into constraint objects...
+
+(4) Test...  Make sure the thing works...
+
+Next basic implementation phase:
+(1) Extend Naive Encoder Pass to test other encodings
+(2) Build more clever function encodings strategies (e.g., equals, add, etc)...
+(3) Test
+
+Actual research:
+
+(1) TreeRewriting --- probably should do Equivalent Subexpression
+Elimination (Don't have the same expression appear twice, instead
+simply link to it again).  Possibly good to do in TreeConstruction...
+This could be lower priority as it isn't really essential to make
+things work.  Should also probably be switchable on/off...
+
+--> Done
+
+(2) Advanced TreeRewriting --- can rewrite functions/predicates to
+eliminate unused entries or to eliminate effectively identical
+outputs...  e.g., consider a function f() that can output the values
+1,3, 5, 7, and its output is only ever compared to 3...  We could
+rewrite the values 1, 5, and 7 to be the same value.
+
+(3) Advanced Encoding Strategies
+  a) encoding alignment --- making binary index encodings over
+different sets work together
+
+  b) Implement K-Map for function encoding
+
+(4) Implement search framework --- probably simulated annealing over a
+population of strategies...  search framework should probably be able
+to turn on/off nearly any optimization we have...
+
+(5) Implement backend translation strategies....do optimizations and
+implement other simplifcation strategies
+
+(6) Convert SATCheck to use Constraint Compiler...not sure about order...
+Started...
+
+(7) Profile system....
+
+---------------------------------------------------------------------
+
+To do:
+
+(0) Support for saving/loading problem instances...
+
+(1) Complete satcheck support
+
+(2) Advance tree rewriting...  Variable value elimination...
+
+(3) Think about undefined semantics...
+
+(4) Smart encoding...
+    Variable Graphs....
+
+    Split graph into connected components
+
+Encoding ideas:
+*    Monotonic increasing index
+*    Matched index (equality)
+*    Bit exposes
+*    Single var
+*    Support arithmetic
+*    Sparse encoding
+
+--------------------------------------------------------------------
+
+