mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

udoc: micro optimization for compiler_guard

Browse source 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-06-24 15:00:47 +01:00 • committed by Christoph M. Wintersteiger
parent 6bf87083ef
commit 5cc8c8bde6
2 changed files with 8 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -723,12 +723,9 @@ namespace datalog {
conds.push_back(m.mk_eq(e1, e2)); conds.push_back(m.mk_eq(e1, e2));
} }
void udoc_relation::compile_guard(expr* g, udoc& d, bit_vector const& discard_cols) const { void udoc_relation::compile_guard(expr* g, udoc& result, bit_vector const& discard_cols) const {
d.reset(dm); result.push_back(dm.allocateX());
d.push_back(dm.allocateX());
apply_guard(g, d, 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 // datastructure to store equalities with columns that will be projected out
union_find_default_ctx union_ctx; union_find_default_ctx union_ctx;
subset_ints equalities(union_ctx); subset_ints equalities(union_ctx);
@ -737,6 +734,7 @@ namespace datalog {
} }
apply_guard(g, result, equalities, discard_cols); apply_guard(g, result, equalities, discard_cols);
} }
bool udoc_relation::apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const { bool udoc_relation::apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const {
udoc_plugin& p = get_plugin(); udoc_plugin& p = get_plugin();
unsigned num_bits; unsigned num_bits;
@ -753,9 +751,6 @@ namespace datalog {
return false; return false;
} }
bool udoc_relation::apply_bv_eq( bool udoc_relation::apply_bv_eq(
expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const { expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const {
udoc_plugin& p = get_plugin(); udoc_plugin& p = get_plugin();
@ -928,7 +923,8 @@ namespace datalog {
m_equalities.mk_var(); m_equalities.mk_var();
} }
t.extract_guard(condition, guard, m_reduced_condition); t.extract_guard(condition, guard, m_reduced_condition);
t.compile_guard(guard, m_udoc, m_empty_bv); m_udoc.push_back(dm.allocateX());
t.apply_guard(guard, m_udoc, m_equalities, m_empty_bv);
TRACE("doc", TRACE("doc",
tout << "original condition: " << mk_pp(condition, m) << "\n"; tout << "original condition: " << mk_pp(condition, m) << "\n";

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

@ -72,7 +72,6 @@ namespace datalog {
void extract_equalities( void extract_equalities(
expr* e1, expr* e2, expr_ref_vector& conds, expr* e1, expr* e2, expr_ref_vector& conds,
subset_ints& equalities, unsigned_vector& roots) const; subset_ints& equalities, unsigned_vector& roots) const;
void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const;
void apply_guard(expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const; void apply_guard(expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const;
bool apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const; bool apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const;
bool apply_bv_eq(expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const; bool apply_bv_eq(expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const;