Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

src/sat/sat_solver/inc_sat_solver.cpp

@@ -24,6 +24,8 @@ Notes:
 #include "ast/ast_util.h"
 #include "solver/solver.h"
 #include "solver/tactic2solver.h"
+#include "solver/parallel_params.hpp"
+#include "solver/parallel_tactic.h"
 #include "tactic/tactical.h"
 #include "tactic/aig/aig_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
@@ -39,6 +41,7 @@ Notes:
 #include "sat/sat_solver.h"
 #include "sat/sat_params.hpp"
 #include "sat/tactic/goal2sat.h"
+#include "sat/tactic/sat_tactic.h"
 #include "sat/sat_simplifier_params.hpp"
 
 // incremental SAT solver.
@@ -865,3 +868,9 @@ void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* sof
     s.display_weighted(out, sz, soft, weights.c_ptr());
 }
 
+
+tactic * mk_psat_tactic(ast_manager& m, params_ref const& p) {
+    parallel_params pp(p);
+    bool use_parallel = pp.enable();
+    return pp.enable() ? mk_parallel_tactic(mk_inc_sat_solver(m, p, false), p) : mk_sat_tactic(m);
+}

src/sat/sat_solver/inc_sat_solver.h

@@ -22,8 +22,12 @@ Notes:
 
 #include "solver/solver.h"
 
+class tactic;
+
 solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode = true);
 
+tactic* mk_psat_tactic(ast_manager& m, params_ref const& p);
+
 
 void  inc_sat_display(std::ostream& out, solver& s, unsigned sz, expr*const* soft, rational const* _weights);
 

src/sat/tactic/sat_tactic.cpp

@@ -20,6 +20,8 @@ Notes:
 #include "tactic/tactical.h"
 #include "sat/tactic/goal2sat.h"
 #include "sat/sat_solver.h"
+#include "solver/parallel_tactic.h"
+#include "solver/parallel_params.hpp"
 #include "model/model_v2_pp.h"
 
 class sat_tactic : public tactic {
@@ -215,3 +217,4 @@ tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p) {
     return t;
 }
 
+

src/smt/tactic/smt_tactic.cpp

@@ -16,19 +16,21 @@ Author:
 Notes:
 
 --*/
-#include "tactic/tactic.h"
-#include "tactic/tactical.h"
+#include "util/lp/lp_params.hpp"
+#include "ast/rewriter/rewriter_types.h"
+#include "ast/ast_util.h"
 #include "smt/smt_kernel.h"
 #include "smt/params/smt_params.h"
 #include "smt/params/smt_params_helper.hpp"
-#include "util/lp/lp_params.hpp"
-#include "ast/rewriter/rewriter_types.h"
-#include "tactic/generic_model_converter.h"
-#include "ast/ast_util.h"
-#include "solver/solver2tactic.h"
 #include "smt/smt_solver.h"
+#include "tactic/tactic.h"
+#include "tactic/tactical.h"
+#include "tactic/generic_model_converter.h"
+#include "solver/solver2tactic.h"
 #include "solver/solver.h"
 #include "solver/mus.h"
+#include "solver/parallel_tactic.h"
+#include "solver/parallel_params.hpp"
 
 typedef obj_map<expr, expr *> expr2expr_map;
 
@@ -301,3 +303,20 @@ tactic * mk_smt_tactic_using(bool auto_config, params_ref const & _p) {
     return using_params(r, p);
 }
 
+tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) {
+    parallel_params pp(p);
+    bool use_parallel = pp.enable();
+    return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p);
+}
+
+tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p, symbol const& logic) {
+    parallel_params pp(_p);
+    bool use_parallel = pp.enable();
+    params_ref p = _p;
+    p.set_bool("auto_config", auto_config);
+    return using_params(pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p), p);
+}
+
+tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) {
+    return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p);
+}

src/smt/tactic/smt_tactic.h

@@ -31,8 +31,13 @@ tactic * mk_smt_tactic(params_ref const & p = params_ref());
 // syntax sugar for using_params(mk_smt_tactic(), p) where p = (:auto_config, auto_config)
 tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref());
 
+tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic = symbol::null);
+tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p, symbol const& logic = symbol::null);
+tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p);
+
 
 /*
   ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)") 
+  ADD_TACTIC("psmt", "builtin strategy for SMT tactic in parallel.", "mk_parallel_smt_tactic(m, p)")
 */
 #endif

src/solver/CMakeLists.txt

@@ -3,6 +3,7 @@ z3_add_component(solver
     check_sat_result.cpp
     combined_solver.cpp
     mus.cpp
+    parallel_tactic.cpp
     smt_logics.cpp
     solver.cpp
     solver_na2as.cpp
@@ -14,4 +15,6 @@ z3_add_component(solver
     tactic
   PYG_FILES
     combined_solver_params.pyg
+    parallel_params.pyg
+
 )

src/solver/parallel_tactic.cpp

@@ -39,7 +39,8 @@ Notes:
 #include "tactic/tactic.h"
 #include "tactic/tactical.h"
 #include "tactic/portfolio/fd_solver.h"
-#include "tactic/smtlogics/parallel_params.hpp"
+#include "solver/parallel_tactic.h"
+#include "solver/parallel_params.hpp"
 #include "smt/tactic/smt_tactic.h"
 #include "smt/smt_solver.h"
 #include "sat/sat_solver/inc_sat_solver.h"
@@ -710,37 +711,7 @@ public:
 };
 
 
-
-tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p) {
-    solver* s = mk_fd_solver(m, p);
-    return alloc(parallel_tactic, s, p);
-}
-
 tactic * mk_parallel_tactic(solver* s, params_ref const& p) {
     return alloc(parallel_tactic, s, p);
 }
 
-
-tactic * mk_psat_tactic(ast_manager& m, params_ref const& p) {
-    parallel_params pp(p);
-    bool use_parallel = pp.enable();
-    return pp.enable() ? mk_parallel_tactic(mk_inc_sat_solver(m, p), p) : mk_sat_tactic(m);
-}
-
-tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) {
-    parallel_params pp(p);
-    bool use_parallel = pp.enable();
-    return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p);
-}
-
-tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p, symbol const& logic) {
-    parallel_params pp(_p);
-    bool use_parallel = pp.enable();
-    params_ref p = _p;
-    p.set_bool("auto_config", auto_config);
-    return using_params(pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p), p);
-}
-
-tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) {
-    return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p);
-}

src/solver/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 tactic;
+class solver;
+
+tactic * mk_parallel_tactic(solver* s, params_ref const& p);
+
+#endif

src/tactic/portfolio/CMakeLists.txt

@@ -4,11 +4,9 @@ z3_add_component(portfolio
     default_tactic.cpp
     enum2bv_solver.cpp
     fd_solver.cpp
-    parallel_tactic.cpp
     pb2bv_solver.cpp
     smt_strategic_solver.cpp
     solver2lookahead.cpp
-    solver_sat_extension.cpp
   COMPONENT_DEPENDENCIES
     aig_tactic
     fp
@@ -22,5 +20,4 @@ z3_add_component(portfolio
   TACTIC_HEADERS
     default_tactic.h
     fd_solver.h
-    parallel_tactic.h
 )

src/tactic/portfolio/fd_solver.cpp

@@ -24,6 +24,8 @@ Notes:
 #include "tactic/portfolio/pb2bv_solver.h"
 #include "tactic/portfolio/bounded_int2bv_solver.h"
 #include "solver/solver2tactic.h"
+#include "solver/parallel_tactic.h"
+#include "solver/parallel_params.hpp"
 
 solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mode) {
     solver* s = mk_inc_sat_solver(m, p, incremental_mode);
@@ -36,3 +38,8 @@ solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mo
 tactic * mk_fd_tactic(ast_manager & m, params_ref const& p) {
     return mk_solver2tactic(mk_fd_solver(m, p, false));
 }
+
+tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p) {
+    solver* s = mk_fd_solver(m, p);
+    return mk_parallel_tactic(s, p);
+}

src/tactic/portfolio/fd_solver.h

@@ -27,9 +27,11 @@ class tactic;
 
 solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mode = true);
 tactic * mk_fd_tactic(ast_manager & m, params_ref const & p);
+tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p);
 
 /*
     ADD_TACTIC("qffd", "builtin strategy for solving QF_FD problems.", "mk_fd_tactic(m, p)")
+    ADD_TACTIC("pqffd", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_qffd_tactic(m, p)")
 */
 
 #endif

src/tactic/portfolio/parallel_tactic.h

@@ -1,40 +0,0 @@
-/*++
-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;
-class solver;
-
-tactic * mk_parallel_tactic(solver* s, params_ref const& p);
-tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p);
-tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p);
-
-// create parallel sat/smt tactics if parallel.enable=true, otherwise return sequential versions.
-tactic * mk_psat_tactic(ast_manager& m, params_ref const& p);
-tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic = symbol::null);
-tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p, symbol const& logic = symbol::null);
-
-/*
-    ADD_TACTIC("pqffd", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_qffd_tactic(m, p)")
-    ADD_TACTIC("psmt", "builtin strategy for SMT tactic in parallel.", "mk_parallel_smt_tactic(m, p)")
-*/
-
-#endif

src/tactic/smtlogics/CMakeLists.txt

@@ -26,7 +26,6 @@ z3_add_component(smtlogic_tactics
     smt_tactic
   PYG_FILES
     qfufbv_tactic_params.pyg
-    parallel_params.pyg
   TACTIC_HEADERS
     nra_tactic.h
     qfaufbv_tactic.h

src/tactic/smtlogics/qfbv_tactic.cpp

@@ -29,8 +29,6 @@ Notes:
 #include "tactic/aig/aig_tactic.h"
 #include "sat/tactic/sat_tactic.h"
 #include "sat/sat_solver/inc_sat_solver.h"
-#include "tactic/portfolio/parallel_tactic.h"
-#include "tactic/smtlogics/parallel_params.hpp"
 #include "ackermannization/ackermannize_bv_tactic.h"
 
 #define MEMLIMIT 300

src/tactic/smtlogics/qflia_tactic.cpp

@@ -34,7 +34,6 @@ Notes:
 #include "sat/tactic/sat_tactic.h"
 #include "tactic/arith/bound_manager.h"
 #include "tactic/arith/probe_arith.h"
-#include "tactic/portfolio/parallel_tactic.h"
 
 struct quasi_pb_probe : public probe {
     virtual result operator()(goal const & g) {