From 0b12ba0ca00f7cdfb50b614fb24b673fb7e4e322 Mon Sep 17 00:00:00 2001 From: Matthew Sotoudeh Date: Fri, 14 Jul 2023 07:25:31 -0700 Subject: initial code --- README | 49 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 README (limited to 'README') 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 -- cgit v1.2.3