From 79ceaa1d1394d7b51e5c1b90c98c64188776509e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Oct 2017 13:17:57 -0700 Subject: [PATCH] fixes Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 4 +- src/sat/tactic/goal2sat.cpp | 29 +++--- src/tactic/portfolio/CMakeLists.txt | 1 + src/tactic/portfolio/parallel_tactic.cpp | 116 +++++++++++++---------- 4 files changed, 89 insertions(+), 61 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 4447b399c..3812eff56 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1468,11 +1468,14 @@ namespace sat { lh.simplify(); lh.collect_statistics(m_aux_stats); } +#if 0 + // Buggy { lookahead lh(*this); lh.scc(); lh.collect_statistics(m_aux_stats); } +#endif } @@ -3049,7 +3052,6 @@ namespace sat { m_probing.updt_params(p); m_scc.updt_params(p); m_rand.set_seed(m_config.m_random_seed); - m_step_size = m_config.m_step_size_init; } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 75561ed86..81302764a 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -94,6 +94,12 @@ struct goal2sat::imp { std::string s0 = "operator " + s + " not supported, apply simplifier before invoking translator"; throw tactic_exception(s0.c_str()); } + + sat::bool_var mk_var(expr* t, bool ext) { + sat::bool_var v = m_solver.mk_var(ext); + m_map.insert(t, v); + return v; + } void mk_clause(sat::literal l) { TRACE("goal2sat", tout << "mk_clause: " << l << "\n";); @@ -120,7 +126,7 @@ struct goal2sat::imp { sat::bool_var mk_true() { if (m_true == sat::null_bool_var) { // create fake variable to represent true; - m_true = m_solver.mk_var(); + m_true = mk_var(m.mk_true(), false); mk_clause(sat::literal(m_true, false)); // v is true } return m_true; @@ -139,8 +145,7 @@ struct goal2sat::imp { } else { bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t); - sat::bool_var v = m_solver.mk_var(ext); - m_map.insert(t, v); + sat::bool_var v = mk_var(t, ext); l = sat::literal(v, sign); TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";); if (ext && !is_uninterp_const(t)) { @@ -247,7 +252,7 @@ struct goal2sat::imp { } else { SASSERT(num <= m_result_stack.size()); - sat::bool_var k = m_solver.mk_var(); + sat::bool_var k = mk_var(t, false); sat::literal l(k, false); m_cache.insert(t, l); sat::literal * lits = m_result_stack.end() - num; @@ -286,7 +291,7 @@ struct goal2sat::imp { } else { SASSERT(num <= m_result_stack.size()); - sat::bool_var k = m_solver.mk_var(); + sat::bool_var k = mk_var(t, false); sat::literal l(k, false); m_cache.insert(t, l); // l => /\ lits @@ -330,7 +335,7 @@ struct goal2sat::imp { m_result_stack.reset(); } else { - sat::bool_var k = m_solver.mk_var(); + sat::bool_var k = mk_var(n, false); sat::literal l(k, false); m_cache.insert(n, l); mk_clause(~l, ~c, t); @@ -367,7 +372,7 @@ struct goal2sat::imp { m_result_stack.reset(); } else { - sat::bool_var k = m_solver.mk_var(); + sat::bool_var k = mk_var(t, false); sat::literal l(k, false); m_cache.insert(t, l); mk_clause(~l, l1, ~l2); @@ -392,7 +397,7 @@ struct goal2sat::imp { } sat::literal_vector lits; convert_pb_args(num, lits); - sat::bool_var v = m_solver.mk_var(true); + sat::bool_var v = mk_var(t, true); ensure_extension(); if (lits.size() % 2 == 0) lits[0].neg(); m_ext->add_xor(v, lits); @@ -451,7 +456,7 @@ struct goal2sat::imp { m_ext->add_pb_ge(sat::null_bool_var, wlits, k.get_unsigned()); } else { - sat::bool_var v = m_solver.mk_var(true); + sat::bool_var v = mk_var(t, true); sat::literal lit(v, sign); m_ext->add_pb_ge(v, wlits, k.get_unsigned()); TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";); @@ -476,7 +481,7 @@ struct goal2sat::imp { m_ext->add_pb_ge(sat::null_bool_var, wlits, k.get_unsigned()); } else { - sat::bool_var v = m_solver.mk_var(true); + sat::bool_var v = mk_var(t, true); sat::literal lit(v, sign); m_ext->add_pb_ge(v, wlits, k.get_unsigned()); TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";); @@ -525,7 +530,7 @@ struct goal2sat::imp { m_ext->add_at_least(sat::null_bool_var, lits, k.get_unsigned()); } else { - sat::bool_var v = m_solver.mk_var(true); + sat::bool_var v = mk_var(t, true); sat::literal lit(v, sign); m_ext->add_at_least(v, lits, k.get_unsigned()); TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";); @@ -547,7 +552,7 @@ struct goal2sat::imp { m_ext->add_at_least(sat::null_bool_var, lits, lits.size() - k.get_unsigned()); } else { - sat::bool_var v = m_solver.mk_var(true); + sat::bool_var v = mk_var(t, true); sat::literal lit(v, sign); m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned()); m_result_stack.shrink(sz - t->get_num_args()); diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index c4ae795c6..055251467 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -21,4 +21,5 @@ z3_add_component(portfolio TACTIC_HEADERS default_tactic.h fd_solver.h + parallel_tactic.h ) diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index 1ee6cbfef..524754613 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -30,12 +30,14 @@ Notes: class parallel_tactic : public tactic { class solver_state { + params_ref m_params; scoped_ptr m_manager; ref m_solver; expr_ref_vector m_cube; unsigned m_units; public: - solver_state(ast_manager* m, solver* s): + solver_state(ast_manager* m, solver* s, params_ref const& p): + m_params(p), m_manager(m), m_solver(s), m_cube(s->get_manager()), @@ -49,6 +51,7 @@ class parallel_tactic : public tactic { for (unsigned i = st.size(); i-- > 0; ) { if (st.get_key(i) == units) { m_units = st.get_uint_value(i); + std::cout << "value for " << i << " is " << m_units << "\n"; break; } } @@ -64,15 +67,17 @@ class parallel_tactic : public tactic { solver const& get_solver() const { return *m_solver; } - solver_state* clone(params_ref& p, expr* cube) { + params_ref const& params() const { return m_params; } + + solver_state* clone(params_ref const& p, expr* cube) { ast_manager& m = m_solver->get_manager(); ast_manager* new_m = alloc(ast_manager, m, !m.proof_mode()); solver* s = m_solver->translate(*new_m, p); - solver_state* st = alloc(solver_state, new_m, s); + solver_state* st = alloc(solver_state, new_m, s, m_params); ast_translation translate(m, *new_m); for (expr* c : m_cube) { st->m_cube.push_back(translate(c)); - } + } expr_ref cube1(translate(cube), *new_m); st->m_cube.push_back(cube1); s->assert_expr(cube1); @@ -109,7 +114,7 @@ private: m_conflicts_decay_rate = 75; m_max_conflicts = m_conflicts_lower_bound; m_progress = 0; - m_num_threads = omp_get_num_threads(); // TBD adjust by possible threads used inside each solver. + m_num_threads = omp_get_num_procs(); // TBD adjust by possible threads used inside each solver. } unsigned get_max_conflicts() { @@ -173,40 +178,60 @@ private: lbool simplify(solver& s) { params_ref p; p.copy(m_params); - p.set_uint("sat.max_conflicts", 10); - p.set_bool("sat.lookahead_simplify", true); + p.set_uint("max_conflicts", 10); + p.set_bool("lookahead_simplify", true); s.updt_params(p); lbool is_sat = s.check_sat(0,0); - p.set_uint("sat.max_conflicts", get_max_conflicts()); - p.set_bool("sat.lookahead_simplify", false); + p.set_uint("max_conflicts", get_max_conflicts()); + p.set_bool("lookahead_simplify", false); s.updt_params(p); return is_sat; } - void cube(solver& s, expr_ref_vector& cubes) { - ast_manager& m = s.get_manager(); - params_ref p; - p.copy(m_params); - p.set_uint("sat.lookahead.cube.cutoff", 1); - s.updt_params(p); + lbool cube(solver_state& s) { + ast_manager& m = s.get_solver().get_manager(); + expr_ref_vector cubes(m); + params_ref p; + p.copy(s.params()); + p.set_uint("lookahead.cube.cutoff", 1); + s.get_solver().updt_params(p); + SASSERT(&m == &cubes.get_manager()); while (true) { - expr_ref c = s.cube(); - if (m.is_false(c)) { + expr_ref c = s.get_solver().cube(); + VERIFY(c); + if (m.is_false(c)) { break; } if (m.is_true(c)) { cubes.reset(); - cubes.push_back(c); - break; + return l_undef; } cubes.push_back(c); } + + IF_VERBOSE(1, verbose_stream() << "cubes: " << cubes << "\n";); + + if (cubes.empty()) { + return l_false; + } + for (unsigned j = 1; j < cubes.size(); ++j) { + solver_state* s1 = s.clone(s.params(), cubes[j].get()); + #pragma omp critical (parallel_tactic) + { + m_solvers.push_back(s1); + } + } + + expr* cube0 = cubes[0].get(); + s.add_cube(cube0); + s.get_solver().assert_expr(cube0); + return l_undef; } lbool solve(solver& s) { params_ref p; p.copy(m_params); - p.set_uint("sat.max_conflicts", get_max_conflicts()); + p.set_uint("max_conflicts", get_max_conflicts()); s.updt_params(p); return s.check_sat(0, 0); } @@ -238,6 +263,7 @@ private: while (true) { int sz = pick_solvers(); + if (sz == 0) { return l_false; } @@ -246,6 +272,8 @@ private: // Simplify phase. IF_VERBOSE(1, verbose_stream() << "(solver.parallel :simplify " << sz << ")\n";); + IF_VERBOSE(1, display(verbose_stream()); verbose_stream() << "Number of solvers: " << sz << "\n";); + #pragma omp parallel for for (int i = 0; i < sz; ++i) { lbool is_sat = simplify(m_solvers[i]->get_solver()); @@ -273,6 +301,8 @@ private: // Solve phase. IF_VERBOSE(1, verbose_stream() << "(solver.parallel :solve " << sz << ")\n";); + IF_VERBOSE(1, display(verbose_stream()); verbose_stream() << "Number of solvers: " << sz << "\n";); + #pragma omp parallel for for (int i = 0; i < sz; ++i) { lbool is_sat = solve(m_solvers[i]->get_solver()); @@ -287,10 +317,6 @@ private: sat_index = i; break; case l_undef: - #pragma omp critical (parallel_tactic) - { - update_progress(false); - } break; } } @@ -304,35 +330,29 @@ private: sz = std::min(max_num_splits(), sz); if (sz == 0) continue; - vector cubes; - for (int i = 0; i < sz; ++i) { - cubes.push_back(expr_ref_vector(m_solvers[i]->get_solver().get_manager())); - } // Split phase. IF_VERBOSE(1, verbose_stream() << "(solver.parallel :split " << sz << ")\n";); + IF_VERBOSE(1, display(verbose_stream()); verbose_stream() << "Number of solvers: " << sz << "\n";); + #pragma omp parallel for for (int i = 0; i < sz; ++i) { - cube(m_solvers[i]->get_solver(), cubes[i]); + switch (cube(*m_solvers[i])) { + case l_false: + #pragma omp critical (parallel_tactic) + { + unsat.push_back(i); + } + break; + default: + #pragma omp critical (parallel_tactic) + { + update_progress(false); + } + break; + } } - for (int i = 0; i < sz; ++i) { - if (cubes[i].empty()) { - unsat.push_back(i); - continue; - } - solver& s = m_solvers[i]->get_solver(); - ast_manager& m = s.get_manager(); - if (cubes[i].size() == 1 && m.is_true(cubes[i][0].get())) { - continue; - } - for (unsigned j = 1; j < cubes[i].size(); ++j) { - m_solvers.push_back(m_solvers[i]->clone(m_params, cubes[i][j].get())); - } - expr* cube0 = cubes[i][0].get(); - m_solvers[i]->add_cube(cube0); - s.assert_expr(cube0); - } remove_unsat(unsat); update_max_conflicts(); } @@ -341,7 +361,7 @@ private: std::ostream& display(std::ostream& out) { for (solver_state* s : m_solvers) { - out << "solver units" << s->num_units() << "\n"; + out << "solver units " << s->num_units() << "\n"; out << "cube " << s->cube() << "\n"; } m_stats.display(out); @@ -359,7 +379,7 @@ public: void operator ()(const goal_ref & g,goal_ref_buffer & result,model_converter_ref & mc,proof_converter_ref & pc,expr_dependency_ref & dep) { ast_manager& m = g->m(); solver* s = mk_fd_solver(m, m_params); - m_solvers.push_back(alloc(solver_state, 0, s)); + m_solvers.push_back(alloc(solver_state, 0, s, m_params)); expr_ref_vector clauses(m); ptr_vector assumptions; obj_map bool2dep;