From d57bca8f8cd7cd0de8c14b76a28c131085c9a213 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Apr 2018 10:43:55 +0800 Subject: [PATCH] fixes Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 2 +- src/sat/sat_model_converter.cpp | 2 +- src/sat/sat_simplifier.cpp | 9 +-- src/tactic/core/elim_uncnstr_tactic.cpp | 33 +++------ src/tactic/portfolio/CMakeLists.txt | 2 - src/tactic/portfolio/parallel_tactic.cpp | 88 ++++++++++++++++-------- src/tactic/smtlogics/CMakeLists.txt | 1 + src/tactic/smtlogics/qfbv_tactic.cpp | 2 +- 8 files changed, 78 insertions(+), 61 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 5b89b4dfd..0d737500a 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1832,7 +1832,7 @@ namespace sat { unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations; scoped_level _sl(*this, dl_truth); //SASSERT(get_level(m_trail.back()) == dl_truth); - IF_VERBOSE(2, verbose_stream() << "(sat-lookahead :double " << l << " :depth " << m_trail_lim.size() << ")\n";); + IF_VERBOSE(3, verbose_stream() << "(sat-lookahead :double " << l << " :depth " << m_trail_lim.size() << ")\n";); lookahead_backtrack(); assign(l); propagate(); diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index b097b3462..22cab35ea 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -75,7 +75,7 @@ namespace sat { void model_converter::operator()(model & m) const { vector::const_iterator begin = m_entries.begin(); vector::const_iterator it = m_entries.end(); - bool first = false; // true; // false; // // true; + bool first = false; // true; // false; // // true; //SASSERT(!m_solver || m_solver->check_clauses(m)); while (it != begin) { --it; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index c048740ac..9c57c79ed 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1129,7 +1129,8 @@ namespace sat { } } } - if (m_intersection.empty()) { + // remove tautology literals if literal has no resolution intersection + if (m_intersection.empty() && !first) { m_tautology.shrink(tsz); } // if (first) IF_VERBOSE(0, verbose_stream() << "taut: " << m_tautology << "\n";); @@ -1202,7 +1203,7 @@ namespace sat { if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit); if (s.is_marked(lit)) idx = i; } - if (false) { + if (false && _blocked.var() == 8074) { IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n"; verbose_stream() << "tautology: " << m_tautology << "\n"; verbose_stream() << "index: " << idx << "\n"; @@ -1212,8 +1213,8 @@ namespace sat { } for (unsigned i = idx; i > 0; --i) { literal lit = m_covered_clause[i]; - s.mark_visited(lit); - continue; + //s.mark_visited(lit); + //continue; if (!s.is_marked(lit)) continue; clause_ante const& ante = m_covered_antecedent[i]; if (ante.cls()) { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 2f961f9bc..0fd25100e 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -552,7 +552,7 @@ class elim_uncnstr_tactic : public tactic { // The result of bv_le is not just introducing a new fresh name, // we need a side condition. // TODO: the correct proof step - return 0; + return nullptr; } if (uncnstr(arg1)) { // v <= t @@ -804,20 +804,17 @@ class elim_uncnstr_tactic : public tactic { ast_manager & m() { return m_manager; } void init_mc(bool produce_models) { - if (!produce_models) { - m_mc = 0; - return; + m_mc = nullptr; + if (produce_models) { + m_mc = alloc(mc, m(), "elim_uncstr"); } - m_mc = alloc(mc, m(), "elim_uncstr"); } void init_rw(bool produce_proofs) { m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps); } - void operator()(goal_ref const & g, - goal_ref_buffer & result) { - bool produce_models = g->models_enabled(); + void operator()(goal_ref const & g, goal_ref_buffer & result) { bool produce_proofs = g->proofs_enabled(); TRACE("elim_uncnstr_bug", g->display(tout);); @@ -832,14 +829,9 @@ class elim_uncnstr_tactic : public tactic { } bool modified = true; TRACE("elim_uncnstr", tout << "unconstrained variables...\n"; - obj_hashtable::iterator it = m_vars.begin(); - obj_hashtable::iterator end = m_vars.end(); - for (; it != end; ++it) { - expr * v = *it; - tout << mk_ismt2_pp(v, m()) << " "; - } + for (expr * v : m_vars) tout << mk_ismt2_pp(v, m()) << " "; tout << "\n";); - init_mc(produce_models); + init_mc(g->models_enabled()); init_rw(produce_proofs); expr_ref new_f(m()); @@ -866,14 +858,9 @@ class elim_uncnstr_tactic : public tactic { else { app_ref_vector & fresh_vars = m_rw->cfg().m_fresh_vars; m_num_elim_apps = fresh_vars.size(); - if (produce_models && !fresh_vars.empty()) { - generic_model_converter * fmc = alloc(generic_model_converter, m(), "elim_uncnstr"); - for (app * f : fresh_vars) - fmc->hide(f); - g->add(concat(fmc, m_mc.get())); - } - else { - g->set((model_converter*)nullptr); + if (m_mc.get()) { + for (app * f : fresh_vars) m_mc->hide(f); + g->add(m_mc.get()); } } m_mc = 0; diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index ed5ec8cf7..055251467 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -18,8 +18,6 @@ z3_add_component(portfolio smtlogic_tactics subpaving_tactic ufbv_tactic - PYG_FILES - parallel_params.pyg TACTIC_HEADERS default_tactic.h fd_solver.h diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index e01e58051..999dbc2e0 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -42,6 +42,7 @@ Notes: #include "solver/solver2tactic.h" #include "tactic/tactic.h" #include "tactic/portfolio/fd_solver.h" +#include "tactic/smtlogics/parallel_params.hpp" class parallel_tactic : public tactic { @@ -150,10 +151,27 @@ class parallel_tactic : public tactic { }; + class cube_var { + expr_ref_vector m_vars; + expr_ref m_cube; + public: + cube_var(expr* c, expr_ref_vector& vs): + m_vars(vs), m_cube(c, vs.get_manager()) {} + + cube_var operator()(ast_translation& tr) { + expr_ref_vector vars(tr.to()); + for (expr* v : m_vars) vars.push_back(tr(v)); + return cube_var(tr(m_cube.get()), vars); + } + + expr* cube() const { return m_cube; } + expr_ref_vector const& vars() { return m_vars; } + }; + class solver_state { task_type m_type; // current work role of the task scoped_ptr m_manager; // ownership handle to ast_manager - expr_ref_vector m_cubes; // set of cubes to process by task + vector m_cubes; // set of cubes to process by task expr_ref_vector m_asserted_cubes; // set of cubes asserted on the current solver params_ref m_params; // configuration parameters ref m_solver; // solver state @@ -176,14 +194,14 @@ class parallel_tactic : public tactic { solver_state(ast_manager* m, solver* s, params_ref const& p, task_type t): m_type(t), m_manager(m), - m_cubes(s->get_manager()), m_asserted_cubes(s->get_manager()), m_params(p), m_solver(s), m_depth(0), m_width(1.0) { - m_restart_max = p.get_uint("sat.restart.max", 10); + parallel_params pp(p); + m_restart_max = pp.restart_max(); } ast_manager& m() { return m_solver->get_manager(); } @@ -199,7 +217,7 @@ class parallel_tactic : public tactic { ast_translation tr(m, *new_m); solver* s = m_solver->translate(*new_m, m_params); solver_state* st = alloc(solver_state, new_m, s, m_params, m_type); - for (expr* c : m_cubes) st->m_cubes.push_back(tr(c)); + for (auto & c : m_cubes) st->m_cubes.push_back(c(tr)); for (expr* c : m_asserted_cubes) st->m_asserted_cubes.push_back(tr(c)); st->m_depth = m_depth; st->m_width = m_width; @@ -210,11 +228,11 @@ class parallel_tactic : public tactic { void set_type(task_type t) { m_type = t; } - expr_ref_vector const& cubes() const { SASSERT(m_type == conquer_task); return m_cubes; } + vector const& cubes() const { SASSERT(m_type == conquer_task); return m_cubes; } // remove up to n cubes from list of cubes. - expr_ref_vector split_cubes(unsigned n) { - expr_ref_vector result(m()); + vector split_cubes(unsigned n) { + vector result; while (n-- > 0 && !m_cubes.empty()) { result.push_back(m_cubes.back()); m_cubes.pop_back(); @@ -222,7 +240,7 @@ class parallel_tactic : public tactic { return result; } - void set_cubes(expr_ref_vector const& c) { + void set_cubes(vector& c) { m_cubes.reset(); m_cubes.append(c); } @@ -280,16 +298,18 @@ class parallel_tactic : public tactic { } void set_conquer_params() { + m_params.set_bool("gc.initial", true); m_params.set_bool("lookahead_simplify", false); m_params.set_uint("restart.max", m_restart_max); get_solver().updt_params(m_params); } void set_simplify_params(bool pb_simp, bool retain_blocked) { + parallel_params pp(m_params); m_params.set_bool("cardinality.solver", pb_simp); m_params.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit")); if (m_params.get_uint("inprocess.max", UINT_MAX) == UINT_MAX) - m_params.set_uint("inprocess.max", 2); + m_params.set_uint("inprocess.max", pp.inprocess_max()); m_params.set_bool("lookahead_simplify", true); m_params.set_uint("restart.max", UINT_MAX); m_params.set_bool("retain_blocked_clauses", retain_blocked); @@ -350,7 +370,7 @@ private: IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% "; if (status == l_true) verbose_stream() << ":status sat "; if (status == l_undef) verbose_stream() << ":status unknown "; - verbose_stream() << ":unsat " << m_num_unsat << " :branches " << m_branches << ")\n";); + verbose_stream() << ":unsat " << m_num_unsat << " :open-branches " << m_branches << ")\n";); } void report_sat(solver_state& s) { @@ -371,9 +391,11 @@ private: } void report_unsat(solver_state& s) { + { + std::lock_guard lock(m_mutex); + ++m_num_unsat; + } close_branch(s, l_false); - std::lock_guard lock(m_mutex); - ++m_num_unsat; } void report_undef(solver_state& s) { @@ -383,7 +405,11 @@ private: void cube_and_conquer(solver_state& s) { ast_manager& m = s.m(); - expr_ref_vector cubes(m), cube(m), hard_cubes(m); + // expr_ref_vector cube(m), hard_cubes(m); + vector cube, hard_cubes, cubes; + expr_ref_vector vars(m); + + add_branches(1); switch (s.type()) { case cube_task: goto cube; @@ -399,7 +425,11 @@ private: SASSERT(cube.size() <= 1); IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";); if (!s.cubes().empty()) m_queue.add_task(s.clone()); - if (!cube.empty()) s.assert_cube(cube.get(0)); + if (!cube.empty()) { + s.assert_cube(cube.get(0).cube()); + vars.reset(); + vars.append(cube.get(0).vars()); + } s.inc_depth(1); // simplify @@ -414,7 +444,6 @@ private: cubes.reset(); s.set_cube_params(); while (true) { - expr_ref_vector vars(m); expr_ref_vector c = s.get_solver().cube(vars, UINT_MAX); // TBD tune this if (c.empty()) { report_undef(s); @@ -423,11 +452,11 @@ private: if (m.is_false(c.back())) { break; } - cubes.push_back(mk_and(c)); + cubes.push_back(cube_var(mk_and(c), vars)); + IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :cube " << cubes.size() << " :vars " << vars.size() << ")\n"); } IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << ")\n";); - IF_VERBOSE(12, verbose_stream() << "(tactic.parallel :cubes " << cubes << ")\n";); if (cubes.empty()) { report_unsat(s); @@ -435,7 +464,7 @@ private: } else { s.inc_width(cubes.size()); - add_branches(cubes.size()); + add_branches(cubes.size() - 1); s.set_cubes(cubes); s.set_type(conquer_task); goto conquer; @@ -451,9 +480,9 @@ private: s.set_conquer_params(); hard_cubes.reset(); - for (expr * c : cubes) { - switch (s.solve(c)) { - case l_undef: hard_cubes.push_back(c); break; + for (cube_var& cv : cubes) { + switch (s.solve(cv.cube())) { + case l_undef: hard_cubes.push_back(cv); break; case l_true: report_sat(s); break; case l_false: report_unsat(s); break; } @@ -580,6 +609,15 @@ public: result.push_back(g.get()); } + virtual void collect_param_descrs(param_descrs & r) { + r.insert("conquer_batch_size", CPK_UINT, "(default: 1000) batch size of cubes to conquer"); + } + + unsigned conquer_batch_size() const { + parallel_params pp(m_params); + return pp.conquer_batch_size(); + } + void cleanup() { m_queue.reset(); init(); @@ -593,14 +631,6 @@ public: m_params.copy(p); } - virtual void collect_param_descrs(param_descrs & r) { - r.insert("conquer_batch_size", CPK_UINT, "(default: 1000) batch size of cubes to conquer"); - } - - unsigned conquer_batch_size() const { - return m_params.get_uint("conquer_batch_size", 1000); - } - virtual void collect_statistics(statistics & st) const { st.copy(m_stats); st.update("par unsat", m_num_unsat); diff --git a/src/tactic/smtlogics/CMakeLists.txt b/src/tactic/smtlogics/CMakeLists.txt index 2741334b4..09b145316 100644 --- a/src/tactic/smtlogics/CMakeLists.txt +++ b/src/tactic/smtlogics/CMakeLists.txt @@ -26,6 +26,7 @@ z3_add_component(smtlogic_tactics smt_tactic PYG_FILES qfufbv_tactic_params.pyg + parallel_params.pyg TACTIC_HEADERS nra_tactic.h qfaufbv_tactic.h diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 0eb235791..25741c09e 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -29,7 +29,7 @@ Notes: #include "tactic/aig/aig_tactic.h" #include "sat/tactic/sat_tactic.h" #include "tactic/portfolio/parallel_tactic.h" -#include "tactic/portfolio/parallel_params.hpp" +#include "tactic/smtlogics/parallel_params.hpp" #include "ackermannization/ackermannize_bv_tactic.h" #define MEMLIMIT 300