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 `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.

pysmt/factory.py

@@ -35,6 +35,8 @@
 from pysmt.logics import convert_logic_from_string
 from pysmt.oracles import get_logic
 from pysmt.solvers.qelim import ShannonQuantifierEliminator
+from pysmt.solvers.solver import SolverOptions
+from pysmt.solvers.portfolio import Portfolio
 
 DEFAULT_SOLVER_PREFERENCE_LIST = ['msat', 'z3', 'cvc4', 'yices', 'btor',
                                   'picosat', 'bdd']
@@ -463,19 +465,24 @@ def UnsatCoreSolver(self, quantified=False, name=None, logic=None,
                                           logic=logic,
                                           unsat_cores_mode=unsat_cores_mode)
 
-
     def QuantifierEliminator(self, name=None, logic=None):
         return self.get_quantifier_eliminator(name=name, logic=logic)
 
     def Interpolator(self, name=None, logic=None):
         return self.get_interpolator(name=name, logic=logic)
 
-    def is_sat(self, formula, solver_name=None, logic=None):
+    def is_sat(self, formula, solver_name=None, logic=None, portfolio=None):
         if logic is None or logic == AUTO_LOGIC:
             logic = get_logic(formula, self.environment)
-        with self.Solver(name=solver_name, logic=logic,
-                         generate_models=False, incremental=False) \
-             as solver:
+        if portfolio is not None:
+            solver = Portfolio(solvers_set=portfolio,
+                               environment=self.environment,
+                               logic=logic,
+                               generate_models=False, incremental=False)
+        else:
+            solver = self.Solver(name=solver_name, logic=logic,
+                                 generate_models=False, incremental=False)
+        with solver:
             return solver.is_sat(formula)
 
     def get_model(self, formula, solver_name=None, logic=None):
@@ -530,20 +537,30 @@ def get_unsat_core(self, clauses, solver_name=None, logic=None):
 
             return solver.get_unsat_core()
 
-    def is_valid(self, formula, solver_name=None, logic=None):
+    def is_valid(self, formula, solver_name=None, logic=None, portfolio=None):
         if logic is None or logic == AUTO_LOGIC:
             logic = get_logic(formula, self.environment)
-        with self.Solver(name=solver_name, logic=logic,
-                         generate_models=False,
-                         incremental=False) as solver:
+        if portfolio is not None:
+            solver = Portfolio(solvers_set=portfolio,
+                               environment=self.environment,
+                               logic=logic,
+                               generate_models=False, incremental=False)
+        else:
+            solver = self.Solver(name=solver_name, logic=logic,
+                                 generate_models=False, incremental=False)
+        with solver:
             return solver.is_valid(formula)
 
-    def is_unsat(self, formula, solver_name=None, logic=None):
-        if logic is None or logic == AUTO_LOGIC:
-            logic = get_logic(formula, self.environment)
-        with self.Solver(name=solver_name, logic=logic,
-                         generate_models=False,
-                         incremental=False) as solver:
+    def is_unsat(self, formula, solver_name=None, logic=None, portfolio=None):
+        if portfolio is not None:
+            solver = Portfolio(solvers_set=portfolio,
+                               environment=self.environment,
+                               logic=logic,
+                               generate_models=False, incremental=False)
+        else:
+            solver = self.Solver(name=solver_name, logic=logic,
+                                 generate_models=False, incremental=False)
+        with solver:
             return solver.is_unsat(formula)
 
     def qelim(self, formula, solver_name=None, logic=None):