mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

working on udoc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-21 20:25:11 -07:00
parent a50cbef877
commit 22808a039d
17 changed files with 171 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/muz/base/dl_context.cpp
View file

@ -233,7 +233,7 @@ namespace datalog {
m_engine_type(LAST_ENGINE),
m_cancel(false) {
re.set_context(this);
m_generate_proof_trace = m_params->generate_proof_trace();
updt_params(pa);
}
context::~context() {
@ -285,7 +285,8 @@ namespace datalog {
unsigned context::dl_profile_milliseconds_threshold() const { return m_params->datalog_profile_timeout_milliseconds(); }
bool context::all_or_nothing_deltas() const { return m_params->datalog_all_or_nothing_deltas(); }
bool context::compile_with_widening() const { return m_params->datalog_compile_with_widening(); }
bool context::unbound_compressor() const { return m_params->datalog_unbound_compressor(); }
bool context::unbound_compressor() const { return m_unbound_compressor; }
void context::set_unbound_compressor(bool f) { m_unbound_compressor = f; }
bool context::similarity_compressor() const { return m_params->datalog_similarity_compressor(); }
unsigned context::similarity_compressor_threshold() const { return m_params->datalog_similarity_compressor_threshold(); }
unsigned context::soft_timeout() const { return m_fparams.m_soft_timeout; }
@ -293,8 +294,7 @@ namespace datalog {
bool context::generate_explanations() const { return m_params->datalog_generate_explanations(); }
bool context::explanations_on_relation_level() const { return m_params->datalog_explanations_on_relation_level(); }
bool context::magic_sets_for_queries() const { return m_params->datalog_magic_sets_for_queries(); }
bool context::eager_emptiness_checking() const { return m_params->datalog_eager_emptiness_checking(); }
bool context::bit_blast() const { return m_params->xform_bit_blast(); }
bool context::karr() const { return m_params->xform_karr(); }
bool context::scale() const { return m_params->xform_scale(); }
@ -839,6 +839,7 @@ namespace datalog {
m_params_ref.copy(p);
if (m_engine.get()) m_engine->updt_params();
m_generate_proof_trace = m_params->generate_proof_trace();
m_unbound_compressor = m_params->datalog_unbound_compressor();
}
expr_ref context::get_background_assertion() {

3
src/muz/base/dl_context.h
View file

@ -172,6 +172,7 @@ namespace datalog {
params_ref m_params_ref;
fixedpoint_params* m_params;
bool m_generate_proof_trace;
bool m_unbound_compressor;
dl_decl_util m_decl_util;
th_rewriter m_rewriter;
var_subst m_var_subst;
@ -256,6 +257,7 @@ namespace datalog {
bool all_or_nothing_deltas() const;
bool compile_with_widening() const;
bool unbound_compressor() const;
void set_unbound_compressor(bool f);
bool similarity_compressor() const;
unsigned similarity_compressor_threshold() const;
unsigned soft_timeout() const;
@ -263,7 +265,6 @@ namespace datalog {
bool generate_explanations() const;
bool explanations_on_relation_level() const;
bool magic_sets_for_queries() const;
bool eager_emptiness_checking() const;
bool bit_blast() const;
bool karr() const;
bool scale() const;

3
src/muz/base/fixedpoint_params.pyg
View file

@ -33,9 +33,6 @@ def_module_params('fixedpoint',
"updated relation was modified or not"),
('datalog.compile_with_widening', BOOL, False,
"widening will be used to compile recursive rules"),
('datalog.eager_emptiness_checking', BOOL, True,
"emptiness of affected relations will be checked after each instruction, " +
"so that we may ommit unnecessary instructions"),
('datalog.default_table_checked', BOOL, False, "if true, the detault " +
'table will be default_table inside a wrapper that checks that its results ' +
'are the same as of default_table_checker table'),

8
src/muz/rel/dl_base.h
View file

@ -465,6 +465,14 @@ namespace datalog {
relation_manager & get_manager() const { return get_plugin().get_manager(); }
virtual bool empty() const = 0;
/**
\brief fast emptiness check. This may be partial.
The requirement is that if fast_empty returns true
then the table or relation is in fact empty.
It is allowed to return false even if the relation is non-empty.
*/
virtual bool fast_empty() const { return empty(); }
virtual void add_fact(const fact & f) = 0;
/**
\brief Like \c add_fact, only here the caller guarantees that the fact is not present in

56
src/muz/rel/dl_instruction.cpp
View file

@ -37,8 +37,7 @@ namespace datalog {
execution_context::execution_context(context & context)
: m_context(context),
m_stopwatch(0),
m_timelimit_ms(0),
m_eager_emptiness_checking(context.eager_emptiness_checking()) {}
m_timelimit_ms(0) {}
execution_context::~execution_context() {
reset();
@ -122,6 +121,22 @@ namespace datalog {
m_timelimit_ms < static_cast<unsigned>(1000*m_stopwatch->get_current_seconds()));
}
void execution_context::collect_statistics(statistics& st) const {
st.update("dl.joins", m_stats.m_join);
st.update("dl.project", m_stats.m_project);
st.update("dl.filter", m_stats.m_filter);
st.update("dl.total", m_stats.m_total);
st.update("dl.unary_singleton", m_stats.m_unary_singleton);
st.update("dl.filter_by_negation", m_stats.m_filter_by_negation);
st.update("dl.select_equal_project", m_stats.m_select_equal_project);
st.update("dl.join_project", m_stats.m_join_project);
st.update("dl.project_rename", m_stats.m_project_rename);
st.update("dl.union", m_stats.m_union);
st.update("dl.filter_interpreted_project", m_stats.m_filter_interp_project);
st.update("dl.filter_id", m_stats.m_filter_id);
st.update("dl.filter_eq", m_stats.m_filter_eq);
}
// -----------------------------------
//
@ -182,7 +197,7 @@ namespace datalog {
}
else {
relation_base& rel = ctx.get_rel_context().get_relation(m_pred);
if ((!ctx.eager_emptiness_checking() || !rel.empty())) {
if (!rel.fast_empty()) {
ctx.set_reg(m_reg, rel.clone());
}
else {
@ -348,6 +363,7 @@ namespace datalog {
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
ctx.make_empty(m_res);
++ctx.m_stats.m_join;
if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) {
return true;
}
@ -375,7 +391,7 @@ namespace datalog {
ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout);
tout<<":"<<ctx.reg(m_res)->get_size_estimate_rows()<<"\n";);
if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) {
if (ctx.reg(m_res)->fast_empty()) {
ctx.make_empty(m_res);
}
return true;
@ -409,6 +425,7 @@ namespace datalog {
: m_reg(reg), m_value(value, m), m_col(col) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
++ctx.m_stats.m_filter_eq;
if (!ctx.reg(m_reg)) {
return true;
}
@ -426,7 +443,7 @@ namespace datalog {
}
(*fn)(r);
if (ctx.eager_emptiness_checking() && r.empty()) {
if (r.fast_empty()) {
ctx.make_empty(m_reg);
}
return true;
@ -457,6 +474,7 @@ namespace datalog {
: m_reg(reg), m_cols(col_cnt, identical_cols) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
++ctx.m_stats.m_filter_id;
if (!ctx.reg(m_reg)) {
return true;
}
@ -474,7 +492,7 @@ namespace datalog {
}
(*fn)(r);
if (ctx.eager_emptiness_checking() && r.empty()) {
if (r.fast_empty()) {
ctx.make_empty(m_reg);
}
return true;
@ -504,6 +522,7 @@ namespace datalog {
return true;
}
log_verbose(ctx);
++ctx.m_stats.m_filter;
relation_mutator_fn * fn;
relation_base & r = *ctx.reg(m_reg);
@ -519,7 +538,7 @@ namespace datalog {
}
(*fn)(r);
if (ctx.eager_emptiness_checking() && r.empty()) {
if (r.fast_empty()) {
ctx.make_empty(m_reg);
}
TRACE("dl_verbose", r.display(tout <<"post-filter-interpreted:\n"););
@ -559,6 +578,7 @@ namespace datalog {
ctx.make_empty(m_res);
return true;
}
++ctx.m_stats.m_filter_interp_project;
relation_transformer_fn * fn;
relation_base & reg = *ctx.reg(m_src);
@ -575,7 +595,7 @@ namespace datalog {
ctx.set_reg(m_res, (*fn)(reg));
if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) {
if (ctx.reg(m_res)->fast_empty()) {
ctx.make_empty(m_res);
}
TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n"););
@ -613,12 +633,13 @@ namespace datalog {
instr_union(reg_idx src, reg_idx tgt, reg_idx delta, bool widen)
: m_src(src), m_tgt(tgt), m_delta(delta), m_widen(widen) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
TRACE("dl", tout << "union " << m_src << " into " << m_tgt
<< " " << ctx.reg(m_src) << " " << ctx.reg(m_tgt) << "\n";);
if (!ctx.reg(m_src)) {
return true;
}
log_verbose(ctx);
++ctx.m_stats.m_union;
relation_base & r_src = *ctx.reg(m_src);
if (!ctx.reg(m_tgt)) {
relation_base * new_tgt = r_src.get_plugin().mk_empty(r_src);
@ -682,7 +703,7 @@ namespace datalog {
r_delta->display(tout <<"delta:");
});
if (ctx.eager_emptiness_checking() && r_delta && r_delta->empty()) {
if (r_delta && r_delta->fast_empty()) {
ctx.make_empty(m_delta);
}
@ -726,11 +747,12 @@ namespace datalog {
reg_idx tgt) : m_projection(projection), m_src(src),
m_cols(col_cnt, cols), m_tgt(tgt) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
ctx.make_empty(m_tgt);
if (!ctx.reg(m_src)) {
return true;
}
log_verbose(ctx);
++ctx.m_stats.m_project_rename;
relation_transformer_fn * fn;
relation_base & r_src = *ctx.reg(m_src);
@ -797,6 +819,7 @@ namespace datalog {
if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) {
return true;
}
++ctx.m_stats.m_join_project;
relation_join_fn * fn;
const relation_base & r1 = *ctx.reg(m_rel1);
const relation_base & r2 = *ctx.reg(m_rel2);
@ -811,7 +834,7 @@ namespace datalog {
TRACE("dl", tout<<r1.get_size_estimate_rows()<<" x "<<r2.get_size_estimate_rows()<<" jp->\n";);
ctx.set_reg(m_res, (*fn)(r1, r2));
TRACE("dl", tout<<ctx.reg(m_res)->get_size_estimate_rows()<<"\n";);
if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) {
if (ctx.reg(m_res)->fast_empty()) {
ctx.make_empty(m_res);
}
return true;
@ -855,6 +878,7 @@ namespace datalog {
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
++ctx.m_stats.m_select_equal_project;
if (!ctx.reg(m_src)) {
ctx.make_empty(m_result);
return true;
@ -873,7 +897,7 @@ namespace datalog {
}
ctx.set_reg(m_result, (*fn)(r));
if (ctx.eager_emptiness_checking() && ctx.reg(m_result)->empty()) {
if (ctx.reg(m_result)->fast_empty()) {
ctx.make_empty(m_result);
}
return true;
@ -913,6 +937,8 @@ namespace datalog {
if (!ctx.reg(m_tgt) || !ctx.reg(m_neg_rel)) {
return true;
}
++ctx.m_stats.m_filter_by_negation;
relation_intersection_filter_fn * fn;
relation_base & r1 = *ctx.reg(m_tgt);
const relation_base & r2 = *ctx.reg(m_neg_rel);
@ -928,7 +954,7 @@ namespace datalog {
}
(*fn)(r1, r2);
if (ctx.eager_emptiness_checking() && r1.empty()) {
if (r1.fast_empty()) {
ctx.make_empty(m_tgt);
}
return true;
@ -966,6 +992,7 @@ namespace datalog {
}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
++ctx.m_stats.m_unary_singleton;
ctx.make_empty(m_tgt);
relation_base * rel = ctx.get_rel_context().get_rmanager().mk_empty_relation(m_sig, m_pred);
rel->add_fact(m_fact);
@ -999,6 +1026,7 @@ namespace datalog {
instr_mk_total(const relation_signature & sig, func_decl* p, reg_idx tgt) : m_sig(sig), m_pred(p), m_tgt(tgt) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
++ctx.m_stats.m_total;
ctx.make_empty(m_tgt);
ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred));
return true;

29
src/muz/rel/dl_instruction.h
View file

@ -66,14 +66,6 @@ namespace datalog {
reg_annotations m_reg_annotation;
stopwatch * m_stopwatch;
unsigned m_timelimit_ms; //zero means no limit
/**
\brief If true, after every operation that may result in an empty relation, a check
for emptiness will be performed, and if a relation is empty, it will be deleted
and replaced by zero. This allows us to avoid performing operations that would have
no effect due to relation emptiness, but if the check for emptiness is expensive, its
cost may overcome the gains.
*/
bool m_eager_emptiness_checking;
public:
execution_context(context & context);
~execution_context();
@ -86,7 +78,26 @@ namespace datalog {
void reset_timelimit();
bool should_terminate();
bool eager_emptiness_checking() const { return m_eager_emptiness_checking; }
struct stats {
unsigned m_join;
unsigned m_project;
unsigned m_filter;
unsigned m_total;
unsigned m_unary_singleton;
unsigned m_filter_by_negation;
unsigned m_select_equal_project;
unsigned m_join_project;
unsigned m_project_rename;
unsigned m_union;
unsigned m_filter_interp_project;
unsigned m_filter_id;
unsigned m_filter_eq;
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
stats m_stats;
void collect_statistics(statistics& st) const;
/**
\brief Return reference to \c i -th register that contains pointer to a relation.

2
src/muz/rel/dl_relation_manager.cpp
View file

@ -538,7 +538,7 @@ namespace datalog {
for(; it!=end; ++it) {
func_decl * pred = *it;
relation_base * rel = try_get_relation(pred);
if(!rel) {
if (!rel) {
out << "Tuples in " << pred->get_name() << ": \n";
continue;
}

28
src/muz/rel/doc.cpp
View file

@ -434,6 +434,34 @@ bool doc_manager::equals(doc const& a, doc const& b) const {
bool doc_manager::is_full(doc const& src) const {
return src.neg().is_empty() && m.equals(src.pos(), *m_full);
}
bool doc_manager::is_empty(doc const& src) {
if (src.neg().size() == 0) return false;
if (src.neg().size() == 1) {
return m.equals(src.pos(), src.neg()[0]);
}
tbv_ref pos(m, m.allocate(src.pos()));
for (unsigned i = 0; i < src.neg().size(); ++i) {
bool found = false;
for (unsigned j = 0; !found && j < num_tbits(); ++j) {
tbit b1 = (*pos)[j];
tbit b2 = src.neg()[i][j];
found = (b1 != BIT_x && b2 != BIT_x && b1 != b2);
}
for (unsigned j = 0; !found && j < num_tbits(); ++j) {
tbit b1 = (*pos)[j];
tbit b2 = src.neg()[i][j];
found = (b1 == BIT_x && b2 != BIT_x);
if (found) {
pos->set(j, neg(b2));
}
}
if (!found) {
return false; // TBD make complete SAT check.
}
}
return true;
}
unsigned doc_manager::hash(doc const& src) const {
unsigned r = 0;
for (unsigned i = 0; i < src.neg().size(); ++i) {

1
src/muz/rel/doc.h
View file

@ -57,6 +57,7 @@ public:
doc& fill1(doc& src);
doc& fillX(doc& src);
bool is_full(doc const& src) const;
bool is_empty(doc const& src);
bool set_and(doc& dst, doc const& src);
bool fold_neg(doc& dst);
bool intersect(doc const& A, doc const& B, doc& result);

12
src/muz/rel/rel_context.cpp
View file

@ -222,6 +222,7 @@ namespace datalog {
}
lbool rel_context::query(unsigned num_rels, func_decl * const* rels) {
setup_default_relation();
get_rmanager().reset_saturated_marks();
scoped_query _scoped_query(m_context);
for (unsigned i = 0; i < num_rels; ++i) {
@ -307,6 +308,7 @@ namespace datalog {
}
lbool rel_context::query(expr* query) {
setup_default_relation();
get_rmanager().reset_saturated_marks();
scoped_query _scoped_query(m_context);
rule_manager& rm = m_context.get_rule_manager();
@ -495,6 +497,12 @@ namespace datalog {
get_rmanager().set_cancel(f);
}
void rel_context::setup_default_relation() {
if (m_context.default_relation() == symbol("doc")) {
m_context.set_unbound_compressor(false);
}
}
relation_plugin & rel_context::get_ordinary_relation_plugin(symbol relation_name) {
relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name);
if (!plugin) {
@ -553,6 +561,10 @@ namespace datalog {
get_rmanager().store_relation(pred, rel);
}
void rel_context::collect_statistics(statistics& st) const {
m_ectx.collect_statistics(st);
}
void rel_context::inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) {
if (orig_pred) {
family_id target_kind = get_rmanager().get_requested_predicate_kind(orig_pred);

3
src/muz/rel/rel_context.h
View file

@ -52,6 +52,8 @@ namespace datalog {
void set_cancel(bool f);
void setup_default_relation();
public:
rel_context(context& ctx);
@ -77,6 +79,7 @@ namespace datalog {
virtual void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred);
virtual void collect_statistics(statistics& st) const;
virtual void cancel() { set_cancel(true); }
virtual void cleanup() { set_cancel(false);}

13
src/muz/rel/tbv.cpp
View file

@ -191,8 +191,17 @@ bool tbv_manager::set_and(tbv& dst, tbv const& src) const {
}
bool tbv_manager::is_well_formed(tbv const& dst) const {
for (unsigned i = 0; i < num_tbits(); ++i) {
if (dst[i] == BIT_z) return false;
unsigned nw = m.num_words();
unsigned w;
for (unsigned i = 0; i + 1 < nw; ++i) {
w = dst.get_word(i);
w = w | (w << 1) | 0x55555555;
if (w != 0xFFFFFFFF) return false;
}
if (nw > 0) {
w = m.last_word(dst);
w = w | (w << 1) | 0x55555555 | ~m.get_mask();
if (w != 0xFFFFFFFF) return false;
}
return true;
}

13
src/muz/rel/udoc_relation.cpp
View file

@ -57,6 +57,16 @@ namespace datalog {
doc* d = fact2doc(f);
m_elems.insert(dm, d);
}
void udoc_relation::add_new_fact(const relation_fact & f) {
m_elems.push_back(fact2doc(f));
}
bool udoc_relation::empty() const {
// TBD: make this a complete check
for (unsigned i = 0; i < m_elems.size(); ++i) {
if (!dm.is_empty(m_elems[i])) return false;
}
return true;
}
bool udoc_relation::contains_fact(const relation_fact & f) const {
doc_ref d(dm, fact2doc(f));
return m_elems.contains(dm, *d);
@ -240,9 +250,8 @@ namespace datalog {
unsigned num_bits = 0;
if (bv.is_bv_sort(s))
return bv.get_bv_size(s);
if (m.is_bool(s)) {
if (m.is_bool(s))
return 1;
}
uint64 sz;
if (dl.try_get_size(s, sz)) {
while (sz > 0) ++num_bits, sz /= 2;

6
src/muz/rel/udoc_relation.h
View file

@ -32,7 +32,7 @@ namespace datalog {
class udoc_relation : public relation_base {
friend class udoc_plugin;
doc_manager& dm;
udoc m_elems;
mutable udoc m_elems;
unsigned_vector m_column_info;
doc* fact2doc(relation_fact const& f) const;
expr_ref to_formula(tbv const& t) const;
@ -42,12 +42,14 @@ namespace datalog {
virtual ~udoc_relation();
virtual void reset();
virtual void add_fact(const relation_fact & f);
virtual void add_new_fact(const relation_fact & f);
virtual bool contains_fact(const relation_fact & f) const;
virtual udoc_relation * clone() const;
virtual udoc_relation * complement(func_decl*) const;
virtual void to_formula(expr_ref& fml) const;
udoc_plugin& get_plugin() const;
virtual bool empty() const { return m_elems.is_empty(); }
virtual bool fast_empty() const { return m_elems.is_empty(); }
virtual bool empty() const;
virtual void display(std::ostream& out) const;
virtual bool is_precise() const { return true; }
virtual unsigned get_size_estimate_rows() const { return m_elems.size(); }

3
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -644,7 +644,8 @@ namespace datalog {
tout << " num unifiers: " << m_unifiers.size();
tout << " num positions: " << m_positions.find(e).size() << "\n";
output_predicate(m_context, to_app(e), tout); tout << "\n";);
return true;
// stop visitor when we have more than 1 unifier, since that's all we want.
return m_unifiers.size() <= 1;
}
void mk_rule_inliner::visitor::reset(unsigned sz) {

20
src/test/tbv.cpp
View file

@ -38,6 +38,7 @@ static void tst1(unsigned num_bits) {
m.deallocate(b1);
m.deallocate(bX);
m.deallocate(bN);
}
static void tst0() {
@ -54,11 +55,30 @@ static void tst0() {
SASSERT(m.equals(*t1, *t3));
}
static void tst2(unsigned num_bits) {
tbv_manager m(num_bits);
tbv_ref t(m), t2(m);
for (unsigned i = 0; i < 55; ++i) {
t = m.allocate(i);
SASSERT(m.is_well_formed(*t));
t2 = m.allocate(i+1);
VERIFY(!m.set_and(*t2, *t));
SASSERT(!m.is_well_formed(*t2));
}
}
void tst_tbv() {
tst0();
tst1(31);
tst1(11);
tst1(15);
tst1(16);
tst1(17);
tst2(31);
tst2(11);
tst2(15);
tst2(16);
tst2(17);
}

1
src/util/fixed_bit_vector.h
View file

@ -108,6 +108,7 @@ public:
fixed_bit_vector& set_or(fixed_bit_vector& dst, fixed_bit_vector const& src) const;
fixed_bit_vector& set_neg(fixed_bit_vector& dst) const;
unsigned last_word(fixed_bit_vector const& bv) const;
unsigned get_mask() const { return m_mask; }
bool equals(fixed_bit_vector const& a, fixed_bit_vector const& b) const;
unsigned hash(fixed_bit_vector const& src) const;
bool contains(fixed_bit_vector const& a, fixed_bit_vector const& b) const;