diff options
Diffstat (limited to 'README')
-rw-r--r-- | README | 7 |
1 files changed, 4 insertions, 3 deletions
@@ -32,16 +32,17 @@ More details on persistent caching: 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 + incremental: 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 + like pysmt + (https://github.com/pysmt/pysmt/blob/8c79de2635936f980595f4a43ee20a7da7554844/pysmt/solvers/portfolio.py#L87), + 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 |