From be65a844adc8d58e3a879cfc988bdc9882b5773e Mon Sep 17 00:00:00 2001 From: Matthew Sotoudeh Date: Wed, 2 Aug 2023 07:50:53 -0700 Subject: note that pysmt also supports portfolio + incremental --- README | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'README') diff --git a/README b/README index 3463ad6..705abed 100644 --- a/README +++ b/README @@ -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 -- cgit v1.2.3