mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
opt + udoc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7e91fb5c15
commit
99ff13b651
|
@ -333,12 +333,10 @@ namespace datalog {
|
|||
doc_manager& dm = r.get_dm();
|
||||
unsigned num_bits = dm.num_tbits();
|
||||
m_size = r.column_num_bits(identical_cols[0]);
|
||||
m_empty_bv.resize(r.get_num_bits(), false);
|
||||
|
||||
m_empty_bv.resize(r.get_num_bits(), false);
|
||||
for (unsigned i = 0; i < col_cnt; ++i) {
|
||||
m_cols[i] = r.column_idx(identical_cols[i]);
|
||||
}
|
||||
|
||||
}
|
||||
for (unsigned i = 0, e = m_empty_bv.size(); i < e; ++i) {
|
||||
m_equalities.mk_var();
|
||||
}
|
||||
|
@ -354,11 +352,8 @@ namespace datalog {
|
|||
}
|
||||
};
|
||||
relation_mutator_fn * udoc_plugin::mk_filter_identical_fn(
|
||||
const relation_base & t, unsigned col_cnt,
|
||||
const unsigned * identical_cols) {
|
||||
if (!check_kind(t))
|
||||
return 0;
|
||||
return alloc(filter_identical_fn, t, col_cnt, identical_cols);
|
||||
const relation_base & t, unsigned col_cnt, const unsigned * identical_cols) {
|
||||
return check_kind(t)?alloc(filter_identical_fn, t, col_cnt, identical_cols):0;
|
||||
}
|
||||
class udoc_plugin::filter_equal_fn : public relation_mutator_fn {
|
||||
doc_manager& dm;
|
||||
|
@ -434,7 +429,7 @@ namespace datalog {
|
|||
void udoc_relation::compile_guard(expr* g, udoc& d) const {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
void udoc_relation::apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) {
|
||||
void udoc_relation::apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const {
|
||||
// datastructure to store equalities with columns that will be projected out
|
||||
union_find_default_ctx union_ctx;
|
||||
subset_ints equalities(union_ctx);
|
||||
|
@ -443,9 +438,13 @@ namespace datalog {
|
|||
}
|
||||
apply_guard(g, result, equalities, discard_cols);
|
||||
}
|
||||
void udoc_relation::apply_eq(expr* g, udoc& result, var* v, unsigned hi, unsigned lo, expr* c) const {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
||||
void udoc_relation::apply_guard(
|
||||
expr* g, udoc& result,
|
||||
subset_ints& equalities, bit_vector const& discard_cols) {
|
||||
subset_ints& equalities, bit_vector const& discard_cols) const {
|
||||
ast_manager& m = get_plugin().get_ast_manager();
|
||||
bv_util& bv = get_plugin().bv;
|
||||
expr* e1, *e2;
|
||||
|
@ -489,6 +488,7 @@ namespace datalog {
|
|||
else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) {
|
||||
unsigned hi, lo;
|
||||
expr* e3;
|
||||
NOT_IMPLEMENTED_YET();
|
||||
// TBD: equalities and discard_cols?
|
||||
if (is_var(e1) && is_ground(e2)) {
|
||||
apply_eq(g, result, to_var(e1), bv.get_bv_size(e1)-1, 0, e2);
|
||||
|
@ -506,6 +506,7 @@ namespace datalog {
|
|||
var* v1 = to_var(e1);
|
||||
var* v2 = to_var(e2);
|
||||
// TBD
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
else {
|
||||
goto failure_case;
|
||||
|
@ -551,14 +552,8 @@ namespace datalog {
|
|||
TRACE("dl", tout << "final size: " << t.get_size_estimate_rows() << '\n';);
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
|
||||
relation_mutator_fn * udoc_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) {
|
||||
if (!check_kind(t))
|
||||
return 0;
|
||||
TRACE("dl", tout << mk_pp(condition, get_ast_manager()) << '\n';);
|
||||
return alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition);
|
||||
return check_kind(t)?alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition):0;
|
||||
}
|
||||
|
||||
class udoc_plugin::negation_filter_fn : public relation_intersection_filter_fn {
|
||||
|
@ -588,4 +583,55 @@ namespace datalog {
|
|||
return alloc(negation_filter_fn, get(t), get(neg), joined_col_cnt, t_cols, negated_cols);
|
||||
}
|
||||
|
||||
class udoc_plugin::filter_proj_fn : public convenient_relation_project_fn {
|
||||
doc_manager& dm;
|
||||
expr_ref m_condition;
|
||||
udoc m_udoc;
|
||||
bit_vector m_col_list; // map: col idx -> bool (whether the column is to be removed)
|
||||
public:
|
||||
filter_proj_fn(const udoc_relation & t, ast_manager& m, app *condition,
|
||||
unsigned col_cnt, const unsigned * removed_cols) :
|
||||
convenient_relation_project_fn(t.get_signature(), col_cnt, removed_cols),
|
||||
dm(t.get_dm()),
|
||||
m_condition(m) {
|
||||
t.expand_column_vector(m_removed_cols);
|
||||
m_col_list.resize(t.get_num_bits(), false);
|
||||
for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
|
||||
m_col_list.set(m_removed_cols[i]);
|
||||
}
|
||||
m_removed_cols.push_back(UINT_MAX);
|
||||
expr_ref guard(m), rest(m);
|
||||
t.extract_guard(condition, guard, m_condition);
|
||||
t.compile_guard(guard, m_udoc);
|
||||
if (m.is_true(m_condition)) {
|
||||
m_condition = 0;
|
||||
}
|
||||
}
|
||||
|
||||
virtual ~filter_proj_fn() {
|
||||
m_udoc.reset(dm);
|
||||
}
|
||||
virtual relation_base* operator()(const relation_base & tb) {
|
||||
udoc_relation const & t = get(tb);
|
||||
udoc const& u1 = t.get_udoc();
|
||||
udoc u2;
|
||||
// copy u1 -> u2;
|
||||
NOT_IMPLEMENTED_YET();
|
||||
u2.intersect(dm, m_udoc);
|
||||
if (m_condition && !u2.empty()) {
|
||||
t.apply_guard(m_condition, u2, m_col_list);
|
||||
}
|
||||
udoc_relation* res = get(t.get_plugin().mk_empty(get_result_signature()));
|
||||
NOT_IMPLEMENTED_YET();
|
||||
// u2.project(m_removed_cols, res->get_dm(), res->get_udoc());
|
||||
return res;
|
||||
}
|
||||
};
|
||||
relation_transformer_fn * udoc_plugin::mk_filter_interpreted_and_project_fn(
|
||||
const relation_base & t, app * condition,
|
||||
unsigned removed_col_cnt, const unsigned * removed_cols) {
|
||||
return check_kind(t)?alloc(filter_proj_fn, get(t), get_ast_manager(), condition, removed_col_cnt, removed_cols):0;
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
|
@ -64,9 +64,9 @@ namespace datalog {
|
|||
bool is_guard(expr* g) const;
|
||||
bool is_guard(unsigned n, expr* const *g) const;
|
||||
void compile_guard(expr* g, udoc& d) const;
|
||||
void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols);
|
||||
void apply_guard(expr* g, udoc& result, subset_ints& equalities, bit_vector const& discard_cols);
|
||||
void apply_eq(expr* g, udoc& result, var* v, unsigned hi, unsigned lo, expr* c);
|
||||
void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const;
|
||||
void apply_guard(expr* g, udoc& result, subset_ints& equalities, bit_vector const& discard_cols) const;
|
||||
void apply_eq(expr* g, udoc& result, var* v, unsigned hi, unsigned lo, expr* c) const;
|
||||
};
|
||||
|
||||
class udoc_plugin : public relation_plugin {
|
||||
|
@ -120,8 +120,6 @@ namespace datalog {
|
|||
virtual relation_transformer_fn * mk_filter_interpreted_and_project_fn(
|
||||
const relation_base & t, app * condition,
|
||||
unsigned removed_col_cnt, const unsigned * removed_cols);
|
||||
|
||||
// project join select
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
@ -163,7 +163,7 @@ public:
|
|||
tout << "\n";
|
||||
display(tout);
|
||||
);
|
||||
lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
|
||||
lbool is_sat = check_sat_hill_climb(m_asms);
|
||||
if (m_cancel) {
|
||||
return l_undef;
|
||||
}
|
||||
|
@ -276,7 +276,7 @@ public:
|
|||
tout << "\n";
|
||||
display(tout);
|
||||
);
|
||||
lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
|
||||
lbool is_sat = check_sat_hill_climb(m_asms);
|
||||
if (m_cancel) {
|
||||
return l_undef;
|
||||
}
|
||||
|
@ -339,6 +339,32 @@ public:
|
|||
return l_true;
|
||||
}
|
||||
|
||||
lbool check_sat_hill_climb(expr_ref_vector& asms1) {
|
||||
expr_ref_vector asms(asms1);
|
||||
lbool is_sat = l_true;
|
||||
if (m_hill_climb) {
|
||||
/**
|
||||
Give preference to cores that have large minmal values.
|
||||
*/
|
||||
sort_assumptions(asms);
|
||||
unsigned index = 0;
|
||||
unsigned last_index = 0;
|
||||
while (index < asms.size() && is_sat == l_true) {
|
||||
while (asms.size() > 20*(index - last_index) && index < asms.size()) {
|
||||
index = next_index(asms, index);
|
||||
//std::cout << "weight: " << get_weight(asms[index-1].get()) << "\n";
|
||||
//break;
|
||||
}
|
||||
last_index = index;
|
||||
is_sat = s().check_sat(index, asms.c_ptr());
|
||||
}
|
||||
}
|
||||
else {
|
||||
is_sat = s().check_sat(asms.size(), asms.c_ptr());
|
||||
}
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
void found_optimum() {
|
||||
s().get_model(m_model);
|
||||
DEBUG_CODE(
|
||||
|
@ -392,25 +418,7 @@ public:
|
|||
TRACE("opt",
|
||||
display_vec(tout << "core: ", core.size(), core.c_ptr());
|
||||
display_vec(tout << "assumptions: ", asms.size(), asms.c_ptr()););
|
||||
|
||||
if (m_hill_climb) {
|
||||
/**
|
||||
Give preference to cores that have large minmal values.
|
||||
*/
|
||||
sort_assumptions(asms);
|
||||
unsigned index = 0;
|
||||
unsigned last_index = 0;
|
||||
while (index < asms.size() && is_sat != l_false) {
|
||||
while (asms.size() > 10*(index - last_index) && index < asms.size()) {
|
||||
index = next_index(asms, index);
|
||||
}
|
||||
last_index = index;
|
||||
is_sat = s().check_sat(index, asms.c_ptr());
|
||||
}
|
||||
}
|
||||
else {
|
||||
is_sat = s().check_sat(asms.size(), asms.c_ptr());
|
||||
}
|
||||
is_sat = check_sat_hill_climb(asms);
|
||||
}
|
||||
TRACE("opt",
|
||||
tout << "num cores: " << cores.size() << "\n";
|
||||
|
|
Loading…
Reference in a new issue