mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 00:41:56 +00:00
Code Activity

work on inprocessing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-11 09:29:00 -07:00
parent e653f167df
commit dcd947f5ef
6 changed files with 104 additions and 97 deletions
Download patch file Download diff file Expand all files Collapse all files

74
src/ast/simplifiers/dependent_expr_state.h
View file

@ -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<dependent_expr> 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);
}

3
src/params/smt_parallel_params.pyg
View file

@ -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')
))

5
src/smt/smt_context.cpp
View file

@ -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<expr> const& vars, unsigned_vector& depth) {

1
src/smt/smt_context.h
View file

@ -137,6 +137,7 @@ namespace smt {
lbool m_internal_completed = l_undef;
scoped_ptr<dependent_expr_simplifier> m_simplifier;
scoped_ptr<base_dependent_expr_state> m_fmls;
// -----------------------------------

117
src/smt/smt_parallel2.cpp
View file

@ -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<dependent_expr> 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 {

1
src/smt/smt_parallel2.h
View file

@ -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<cube_config>;