From: bdemsky <bdemsky@uci.edu>
Date: Tue, 20 Jun 2017 21:09:50 +0000 (-0700)
Subject: add notes
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=5486d5ef9ea1ddedae0fb273efe9521d28af2e49;hp=487b405f45bfc928a981a2b3613c08f26cf4a9e5

add notes
---

diff --git a/design/notes.dot b/design/notes.dot
new file mode 100644
index 0000000..713fa6e
--- /dev/null
+++ b/design/notes.dot
@@ -0,0 +1,7 @@
+digraph "Passes" {
+TreeConstruction->TreeRewriting;
+TreeRewriting->EncodingSelection;
+EncodingSelection->Encoding;
+Encoding->SATOptimization;
+SATOptimization->CNFSATConversion;
+}
\ No newline at end of file
diff --git a/design/notes.pdf b/design/notes.pdf
new file mode 100644
index 0000000..c9e46f7
Binary files /dev/null and b/design/notes.pdf differ
diff --git a/design/notes.txt b/design/notes.txt
index ce399c3..4219c89 100644
--- a/design/notes.txt
+++ b/design/notes.txt
@@ -9,3 +9,52 @@ 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...
+
+(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...
+
+(7) Profile system....