Merging with branch master

[satune.git] / design / notes.txt

diff --git a/design/notes.txt b/design/notes.txt
index 1159c96aa11a37202a54f6cb49c2bdbfa280bf65..f7282be8883bf8bad2ba8e2c1809646ef6ad41df 100644 (file)
--- a/design/notes.txt
+++ b/design/notes.txt
@@ -1,8 +1,94 @@
 (1) Elements/BooleanVars should link back to expressions that use them
 (1) Elements/BooleanVars should link back to expressions that use them

+--> Done

 
 (2) Need to introduce variables in encoding of functions....
 
 (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?
 
 (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
+
+--------------------------------------------------------------------
+
+