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

DoC: enable filter_project

Browse source 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2014-10-08 09:58:02 +01:00
parent a3a008bdde
commit 0cf04589ff
1 changed files with 5 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1056,7 +1056,7 @@ namespace datalog {
return check_kind(t)?alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition):0; return check_kind(t)?alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition):0;
} }
class udoc_plugin::join_project_fn : convenient_relation_join_project_fn { class udoc_plugin::join_project_fn : public convenient_relation_join_project_fn {
udoc_plugin::join_fn m_joiner; udoc_plugin::join_fn m_joiner;
union_find_default_ctx union_ctx; union_find_default_ctx union_ctx;
bit_vector m_to_delete; bit_vector m_to_delete;
@ -1172,15 +1172,11 @@ namespace datalog {
relation_base const& t1, relation_base const& t2, relation_base const& t1, relation_base const& t2,
unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2,
unsigned removed_col_cnt, const unsigned * removed_cols) { unsigned removed_col_cnt, const unsigned * removed_cols) {
if (check_kind(t1) && check_kind(t2)) if (!check_kind(t1) || !check_kind(t2))
return 0;
#if 0
return alloc(join_project_fn, get(t1), ge(t2),
joined_col_cnt, cols1, cols2,
removed_col_cnt, removed_cols);
#endif
else
return 0; return 0;
return alloc(join_project_fn, get(t1), get(t2),
joined_col_cnt, cols1, cols2,
removed_col_cnt, removed_cols);
} }