initial code

1 files changed, 49 insertions, 0 deletions

diff --git a/README b/README
new file mode 100644
index 0000000..3463ad6
--- /dev/null
+++ b/README
@@ -0,0 +1,49 @@
+######## satispipy ########
+Satisfiability modulo theory with Portfolio and Incremental solving, in Python
+
+Dependencies:
+    - reasonably modern Python
+    - pexpect
+    - SMT-LIB solver binaries
+
+Features:
+    - automatic incremental solving (no need to push/pop)
+    - persistent caching
+    - automatic portfolio solving (use multiple solvers and take the fastest)
+    - support for heuristic quantifier instantiation
+    - simple, easy to hack
+
+Usage example:
+    see example/ for a simple symbolic execution engine using satispipy
+
+More details on automatic incremental solving:
+    to use:
+        call model([a, b, c])
+        call model([a, b, c, d, e])
+        call model([a, b, c, f, g])
+        call model([a, b, c])
+    satispipy will automatically insert push() and pop() commands as needed
+
+More details on persistent caching:
+    to use:
+        call model([a, b, c])
+        call model([e, f, g])
+        call model([a, b, c])
+    satispipy will return immediately for the third call
+    if you run the program again, it will also return immediately for all calls
+
+More details on portfolio solving:
+    portfolio is hard to make work with incremental solving.
+    suppose you're portfolio solving with solvers SMTA and SMTB,
+    and make incremental queries X, Y, Z
+    what if SMTA is fast for X and Y, but slow for Z? and SMTB is the opposite
+    we might have to wait for SMTA to solve X and Y before it gets to Z
+
+    instead, after each solve, we kill all but the single solver that solved it
+    so SMTB starts fresh on the calls for Y and Z
+    no need to wait
+
+Quantifier instantiation:
+    top-level assertions can be universally quantified
+    the quantifier can define its own instantiation heuristics
+    still works with incremental, persistent, and cached solving