1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
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
|
