Portfolio Solver #284
Portfolio Solver #284
Conversation
|
@mikand: This is not ready to be merged, but I'd like some feedback. An open point that I am not sure how to manage is multiple instances of the same solver with different options. I cannot figure out a syntax that I like. |
|
Done with the exception handling (as discussed). Missing is the handling of options for solvers, including multiple instance of the same solver with different options (btw, we should find a meaningful example for this). |
marcogario
changed the title
| class MSatOptions(SolverOptions): | ||
| """Options from MathSAT Solver. """ | ||
| VALID_OPTIONS = SolverOptions.VALID_OPTIONS +\ | ||
| [("random_seed", None), |
There was a problem hiding this comment.
randomseed is part of the SMT-LIB standard, we should move this option to SolverOptions (and incidentally, consider which other options from the standard we can support at this time).
marcogario
force-pushed
the
portfolio
branch
2 times, most recently
from
1d4d9a3
to
e452931
Compare
- Created Portfolio class that uses multiprocessing to solve the problem
using multiple solvers.
- The solver provides a naive incremental interface by using
IncrementalTrackingSolver Interface
- get_value and get_model work after a SAT query. Other
artifacts (unsat-core, interpolants) are not supported.
- Extend Factory.is_* to include `portfolio` key-word, and exported as
is_* shortcuts. The syntax becomes:
is_sat(f, portfolio=["s1", "s2"])
- Exceptions are handled via the 'exit_on_exception' option
- Logic testing is done only when the solvers are started (i.e., during
solve()). If at least one solver terminates, this might not be a
problem, but it is not nice.
| @@ -76,6 +76,8 @@ class BoolectorSolver(IncrementalTrackingSolver, | |||
| LOGICS = [QF_BV, QF_UFBV, QF_ABV, QF_AUFBV, QF_AX] | |||
| OptionsClass = BoolectorOptions | |||
|
|
|||
| OptionsClass = BoolectorOptions | |||
There was a problem hiding this comment.
Duplicated line (see above)
| @@ -88,6 +90,28 @@ def __init__(self, environment, logic, **options): | |||
| self.declarations = {} | |||
| return | |||
|
|
|||
| def _prepare_config(self, options): | |||
There was a problem hiding this comment.
Where is this function used?
| import logging | ||
| from multiprocessing import Process, Queue, Pipe | ||
|
|
||
| from pysmt.solvers.solver import IncrementalTrackingSolver, SolverOptions |
There was a problem hiding this comment.
Does this work? SolverOptions is now in pysmt.solvers.options ...
There was a problem hiding this comment.
Only if you believe with all your heart! 😉
pysmt.solver imports SolverOptions, therefore it is visible from there. I left it like this, in case we want to split the files in the future.
This addresses the PR comments.
Conflicts: pysmt/solvers/solver.py pysmt/test/test_solving.py
Portfolio Solver
Created Portfolio class that uses multiprocessing to solve the problem
using multiple solvers.
The solver provides a naive incremental interface by using
IncrementalTrackingSolver Interface
get_value and get_model work after a SAT query. Other
artifacts (unsat-core, interpolants) are not supported.
Extend Factory.is_* to include
portfoliokey-word, and exported asis_* shortcuts. The syntax becomes:
Exceptions are currently not handled internally. Similarly, logic testing is done only when the solvers are started (i.e., during solve()). If at least one solver terminates, this might not be a problem, but it is not nice.