######## 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