adding outline for parallel tactic

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/sat_elim_eqs.cpp

@@ -96,9 +96,9 @@ namespace sat {
             if (!c.frozen())
                 m_solver.detach_clause(c);
             // apply substitution
-            for (i = 0; i < sz; i++) {
-                SASSERT(!m_solver.was_eliminated(c[i].var()));
+            for (i = 0; i < sz; i++) {                
                 c[i] = norm(roots, c[i]);
+				SASSERT(!m_solver.was_eliminated(c[i].var()));
             }
             std::sort(c.begin(), c.end());
             for (literal l : c) VERIFY(l == norm(roots, l));

src/sat/sat_lookahead.cpp

@@ -1623,6 +1623,8 @@ namespace sat {
     }
 
     void lookahead::reset_lookahead_reward() {
+        SASSERT(m_search_mode == lookahead_mode::lookahead1 ||
+                m_search_mode == lookahead_mode::lookahead2);
         m_qhead = m_qhead_lim.back();
         TRACE("sat", tout << "reset_lookahead_reward: " << m_qhead << "\n";);
         unsigned old_sz = m_trail_lim.back();

src/tactic/portfolio/CMakeLists.txt

@@ -1,11 +1,13 @@
 z3_add_component(portfolio
   SOURCES
+    bounded_int2bv_solver.cpp
     default_tactic.cpp
     enum2bv_solver.cpp
-    pb2bv_solver.cpp
-    bounded_int2bv_solver.cpp
     fd_solver.cpp
+    parallel_tactic.cpp
+    pb2bv_solver.cpp
     smt_strategic_solver.cpp
+    solver2lookahead.cpp
   COMPONENT_DEPENDENCIES
     aig_tactic
     fp

src/tactic/portfolio/parallel_tactic.cpp

@@ -0,0 +1,48 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    parallel_solver.cpp
+
+Abstract:
+
+    Parallel solver in the style of Treengeling.
+
+    It assumes a solver that supports good lookaheads.
+    
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-10-9
+
+Notes:
+   
+--*/
+
+#include "solver/solver.h"
+#include "tactic/tactic.h"
+
+class parallel_tactic : public tactic {
+    ref<solver> m_solver;
+public:
+    parallel_tactic(solver* s) : m_solver(s) {}
+
+    void operator ()(const goal_ref & g,goal_ref_buffer & result,model_converter_ref & mc,proof_converter_ref & pc,expr_dependency_ref & dep) {
+        NOT_IMPLEMENTED_YET();
+    }
+
+    void cleanup() {
+        NOT_IMPLEMENTED_YET();
+    }
+
+    tactic* translate(ast_manager& m) {
+        NOT_IMPLEMENTED_YET();
+        return 0;
+    }
+};
+
+tactic * mk_parallel_tactic(solver* s) {
+    return alloc(parallel_tactic, s);
+}
+

src/tactic/portfolio/parallel_tactic.h

@@ -0,0 +1,27 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    parallel_tactic.h
+
+Abstract:
+
+    Parallel tactic in the style of Treengeling.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-10-9
+
+Notes:
+   
+--*/
+#ifndef PARALLEL_TACTIC_H_
+#define PARALLEL_TACTIC_H_
+
+class solver;
+class tactic;
+
+tactic * mk_parallel_tactic(solver* s);
+
+#endif

src/tactic/portfolio/solver2lookahead.cpp

@@ -0,0 +1,24 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    solver2lookahead.cpp
+
+Abstract:
+
+    Lookahead wrapper for arbitrary solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-10-9
+
+Notes:
+   
+--*/
+#include "sat/sat_solver/inc_sat_solver.h"
+#include "solver/solver.h"
+
+solver * mk_solver2lookahead(solver* s) {
+    return 0;
+}

src/tactic/portfolio/solver2lookahead.h

@@ -0,0 +1,26 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    solver2lookahead.h
+
+Abstract:
+
+    Lookahead wrapper for arbitrary solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-10-9
+
+Notes:
+   
+--*/
+#ifndef SOLVER2LOOKAHEAD_H_
+#define SOLVER2LOOKAHEAD_H_
+
+class solver;
+
+solver * mk_solver2lookahead(solver* s);
+
+#endif