diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index e187f19c6..047dc4652 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -33,6 +33,7 @@ Author: #include "util/statistics.h" #include "util/params.h" #include "util/z3_exception.h" +#include "ast/ast_util.h" #include "ast/converters/model_converter.h" #include "ast/simplifiers/dependent_expr.h" #include "ast/simplifiers/model_reconstruction_trail.h" @@ -113,9 +114,80 @@ public: model_reconstruction_trail& model_trail() override { throw default_exception("unexpected access to model reconstruction"); } bool updated() override { return false; } void reset_updated() override {} - }; + +struct base_dependent_expr_state : public dependent_expr_state { + ast_manager& m; + model_reconstruction_trail m_reconstruction_trail; + bool m_updated = false; + bool m_inconsistent = false; + vector m_fmls; + base_dependent_expr_state(ast_manager& m) :dependent_expr_state(m), m(m), m_reconstruction_trail(m, m_trail) {} + unsigned qtail() const override { return m_fmls.size(); } + dependent_expr const& operator[](unsigned i) override { return m_fmls[i]; } + void update(unsigned i, dependent_expr const& j) override { + SASSERT(j.fml()); + check_false(j.fml()); + m_fmls[i] = j; + m_updated = true; + } + void add(dependent_expr const& j) override { m_updated = true; check_false(j.fml()); m_fmls.push_back(j); } + bool inconsistent() override { return m_inconsistent; } + bool updated() override { return m_updated; } + void reset_updated() override { m_updated = false; } + model_reconstruction_trail& model_trail() override { return m_reconstruction_trail; } + std::ostream& display(std::ostream& out) const override { + unsigned i = 0; + for (auto const& d : m_fmls) { + if (i > 0 && i == qhead()) + out << "---- head ---\n"; + out << d << "\n"; + ++i; + } + m_reconstruction_trail.display(out); + return out; + } + void check_false(expr* f) { + if (m.is_false(f)) + m_inconsistent = true; + } + void replay(unsigned qhead, expr_ref_vector& assumptions) { + m_reconstruction_trail.replay(qhead, assumptions, *this); + } + void flatten_suffix() override { + expr_mark seen; + unsigned j = qhead(); + expr_ref_vector pinned(m); + for (unsigned i = qhead(); i < qtail(); ++i) { + expr* f = m_fmls[i].fml(), * g = nullptr; + pinned.push_back(f); + if (seen.is_marked(f)) + continue; + seen.mark(f, true); + if (m.is_true(f)) + continue; + if (m.is_and(f)) { + auto* d = m_fmls[i].dep(); + for (expr* arg : *to_app(f)) + add(dependent_expr(m, arg, nullptr, d)); + continue; + } + if (m.is_not(f, g) && m.is_or(g)) { + auto* d = m_fmls[i].dep(); + for (expr* arg : *to_app(g)) + add(dependent_expr(m, mk_not(m, arg), nullptr, d)); + continue; + } + if (i != j) + m_fmls[j] = m_fmls[i]; + ++j; + } + m_fmls.shrink(j); + } +}; + + inline std::ostream& operator<<(std::ostream& out, dependent_expr_state& st) { return st.display(out); } diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index 2dd2d95de..0726d91b0 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -20,5 +20,6 @@ def_module_params('smt_parallel', ('explicit_hardness', BOOL, False, 'use explicit hardness metric for cube'), ('cubetree', BOOL, False, 'use cube tree data structure for storing cubes'), ('searchtree', BOOL, False, 'use search tree implementation (parallel2)'), - ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification') + ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'), + ('inprocessing_delay', UINT, 0, 'number of undef before invoking simplification') )) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index ab7197808..818021a60 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4769,6 +4769,11 @@ namespace smt { } mdl = m_model.get(); } + if (m_fmls && mdl) { + auto convert = m_fmls->model_trail().get_model_converter(); + if (convert) + (*convert)(mdl); + } } void context::get_levels(ptr_vector const& vars, unsigned_vector& depth) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 7f3663e49..b6046d33c 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -137,6 +137,7 @@ namespace smt { lbool m_internal_completed = l_undef; scoped_ptr m_simplifier; + scoped_ptr m_fmls; // ----------------------------------- diff --git a/src/smt/smt_parallel2.cpp b/src/smt/smt_parallel2.cpp index 80ebcce4a..7a9253bed 100644 --- a/src/smt/smt_parallel2.cpp +++ b/src/smt/smt_parallel2.cpp @@ -218,6 +218,7 @@ namespace smt { m_config.m_cubetree = pp.cubetree(); m_config.m_max_cube_depth = pp.max_cube_depth(); m_config.m_inprocessing = pp.inprocessing(); + m_config.m_inprocessing_delay = pp.inprocessing_delay(); // don't share initial units ctx->pop_to_base_lvl(); @@ -251,107 +252,38 @@ namespace smt { m_num_shared_units = sz; } - // move to ast/simplifiers as a general class - struct dep_expr_state : public dependent_expr_state { - ast_manager& m; - model_reconstruction_trail m_reconstruction_trail; - bool m_updated = false; - vector m_fmls; - bool m_inconsistent = false; - dep_expr_state(ast_manager& m) :dependent_expr_state(m), m(m), m_reconstruction_trail(m, m_trail) {} - unsigned qtail() const override { return m_fmls.size(); } - dependent_expr const& operator[](unsigned i) override { return m_fmls[i]; } - void update(unsigned i, dependent_expr const& j) override { - SASSERT(j.fml()); - check_false(j.fml()); - m_fmls[i] = j; - m_updated = true; - } - void add(dependent_expr const& j) override { m_updated = true; check_false(j.fml()); m_fmls.push_back(j); } - bool inconsistent() override { return m_inconsistent; } - bool updated() override { return m_updated; } - void reset_updated() override { m_updated = false; } - model_reconstruction_trail& model_trail() override { return m_reconstruction_trail; } - std::ostream& display(std::ostream& out) const override { - unsigned i = 0; - for (auto const& d : m_fmls) { - if (i > 0 && i == qhead()) - out << "---- head ---\n"; - out << d << "\n"; - ++i; - } - m_reconstruction_trail.display(out); - return out; - } - void check_false(expr* f) { - if (m.is_false(f)) - m_inconsistent = true; - } - void replay(unsigned qhead, expr_ref_vector& assumptions) { - m_reconstruction_trail.replay(qhead, assumptions, *this); - th_rewriter rw(m); - expr_ref tmp(m); - for (unsigned i = 0; i < assumptions.size(); ++i) { - tmp = assumptions.get(i); - rw(tmp); - assumptions[i] = tmp; - } - } - void flatten_suffix() override { - expr_mark seen; - unsigned j = qhead(); - expr_ref_vector pinned(m); - for (unsigned i = qhead(); i < qtail(); ++i) { - expr* f = m_fmls[i].fml(), * g = nullptr; - pinned.push_back(f); - if (seen.is_marked(f)) - continue; - seen.mark(f, true); - if (m.is_true(f)) - continue; - if (m.is_and(f)) { - auto* d = m_fmls[i].dep(); - for (expr* arg : *to_app(f)) - add(dependent_expr(m, arg, nullptr, d)); - continue; - } - if (m.is_not(f, g) && m.is_or(g)) { - auto* d = m_fmls[i].dep(); - for (expr* arg : *to_app(g)) - add(dependent_expr(m, mk_not(m, arg), nullptr, d)); - continue; - } - if (i != j) - m_fmls[j] = m_fmls[i]; - ++j; - } - m_fmls.shrink(j); - } - }; + void parallel2::worker::simplify() { // first attempt: one-shot simplification of the context. - // a precise schedule of repeated simplificaiton is TBD. + // a precise schedule of repeated simplification is TBD. // also, the in-processing simplifier should be applied to // a current set of irredundant clauses that may be reduced by // unit propagation. By including the units we are effectively - // repeating unit propagaiton, but potentially not subsumption or - // Boolean simplifications that a solver could perform. + // repeating unit propagation, but potentially not subsumption or + // Boolean simplifications that a solver could perform (smt_context doesnt really) // Integration of inprocssing simplifcation here or in sat/smt solver could // be based on taking the current clause set instead of the asserted formulas. if (!m_config.m_inprocessing) return; + if (m_config.m_inprocessing_delay > 0) { + --m_config.m_inprocessing_delay; + return; + } m_config.m_inprocessing = false; // initial strategy is to immediately disable inprocessing for future calls. - dep_expr_state fmls(m); // TBD, OH, this also has to be heap allocated for m_simplifier to be valid! - if (!ctx->m_simplifier) { + dependent_expr_simplifier* s = ctx->m_simplifier.get(); + if (!s) { // create a simplifier if none exists // initialize it to a default pre-processing simplifier. - auto* s = alloc(then_simplifier, m, ctx->get_params(), fmls); + ctx->m_fmls = alloc(base_dependent_expr_state, m); + auto then_s = alloc(then_simplifier, m, ctx->get_params(), *ctx->m_fmls); + s = then_s; ctx->m_simplifier = s; - init_preprocess(m, ctx->get_params(), *s, fmls); + init_preprocess(m, ctx->get_params(), *then_s, *ctx->m_fmls); } - dependent_expr_simplifier* s = ctx->m_simplifier.get(); + + dependent_expr_state& fmls = *ctx->m_fmls.get(); // extract assertions from ctx. // it is possible to track proof objects here if wanted. // feed them to the simplifier @@ -360,9 +292,9 @@ namespace smt { ctx->get_assertions(assertions); ctx->get_units(units); for (expr* e : assertions) - s->get_fmls().add(dependent_expr(m, e, nullptr, nullptr)); + fmls.add(dependent_expr(m, e, nullptr, nullptr)); for (expr* e : units) - s->get_fmls().add(dependent_expr(m, e, nullptr, nullptr)); + fmls.add(dependent_expr(m, e, nullptr, nullptr)); // run in-processing on the assertions s->reduce(); @@ -371,18 +303,13 @@ namespace smt { // extract simplified assertions from the simplifier // create a new context with the simplified assertions // update ctx with the new context. - for (unsigned i = 0; i < s->get_fmls().qtail(); ++i) { - auto const& de = s->get_fmls()[i]; + for (unsigned i = 0; i < fmls.qtail(); ++i) { + auto const& de = fmls[i]; new_ctx->assert_expr(de.fml()); } ctx = new_ctx.detach(); - // TODO: outside of this function is to make sure model construction uses - // model converter from simplifier. - // The model produced by ctx is not correct when there are model converting - // simplifications. The model returned in the "SAT" case has to be post-processed - // by m_simplifier->model_trail(). - // not too complicated, just has to be done properly. + // TODO: copy user-propagators similar to context::copy. } void parallel2::worker::collect_statistics(::statistics& st) const { diff --git a/src/smt/smt_parallel2.h b/src/smt/smt_parallel2.h index b65e99787..08c0f9fe7 100644 --- a/src/smt/smt_parallel2.h +++ b/src/smt/smt_parallel2.h @@ -137,6 +137,7 @@ namespace smt { bool m_explicit_hardness = false; bool m_cubetree = false; bool m_inprocessing = false; + unsigned m_inprocessing_delay = 0; }; using node = search_tree::node;