diff --git a/spec/ClemensTableau.pdf b/spec/ClemensTableau.pdf
new file mode 100644
index 000000000..8bc5e4e7b
Binary files /dev/null and b/spec/ClemensTableau.pdf differ
diff --git a/spec/LazyMemberships.pdf b/spec/LazyMemberships.pdf
new file mode 100644
index 000000000..d77f6154e
Binary files /dev/null and b/spec/LazyMemberships.pdf differ
diff --git a/spec/plan.md b/spec/plan.md
new file mode 100644
index 000000000..41ea69e20
--- /dev/null
+++ b/spec/plan.md
@@ -0,0 +1,12 @@
+Your task is to implement the theory solver for strings that is described in the resources under reference.md
+
+The theory solver should be implemented as a theory solver in src/smt. Call it theory\_nseq. 
+
+Add a parameter setting to control whether using the default string solver theory\_seq or theory\_nseq or the empty string solver. 
+
+Utilities that can be made self-contained go in the directory ast/rewriter.
+
+
+
+Start out by creating a plan for this implementation.
+
diff --git a/spec/reference.md b/spec/reference.md
new file mode 100644
index 000000000..6a6238917
--- /dev/null
+++ b/spec/reference.md
@@ -0,0 +1,8 @@
+A C# implementation of the procedure is here: https://github.com/CEisenhofer/ZIPT/tree/parikh/ZIPT
+
+A description of the algorithm is in LazyMemberships.pdf
+
+Other algorithms are descried in ClemensTableau.pdf
+
+
+