mirror of
https://github.com/Z3Prover/z3
synced 2025-06-27 00:18:45 +00:00
minor optimization to previous patch
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
parent
4ee83c1774
commit
dddb31fc37
1 changed files with 3 additions and 9 deletions
|
@ -1157,13 +1157,9 @@ namespace datalog {
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
||||||
class udoc_plugin::join_project_and_fn : public convenient_relation_join_project_fn {
|
class udoc_plugin::join_project_and_fn : public relation_join_fn {
|
||||||
public:
|
public:
|
||||||
join_project_and_fn(udoc_relation const& t1, udoc_relation const& t2,
|
join_project_and_fn() {}
|
||||||
unsigned col_cnt, const unsigned *cols1, const unsigned *cols2,
|
|
||||||
unsigned removed_col_cnt, unsigned const *rm_cols)
|
|
||||||
: convenient_relation_join_project_fn(t1.get_signature(), t2.get_signature(),
|
|
||||||
col_cnt, cols1, cols2, removed_col_cnt, rm_cols) {}
|
|
||||||
|
|
||||||
virtual relation_base* operator()(relation_base const& t1, relation_base const& t2) {
|
virtual relation_base* operator()(relation_base const& t1, relation_base const& t2) {
|
||||||
udoc_relation *result = get(t1.clone());
|
udoc_relation *result = get(t1.clone());
|
||||||
|
@ -1186,9 +1182,7 @@ namespace datalog {
|
||||||
if (removed_cols[i] != i)
|
if (removed_cols[i] != i)
|
||||||
goto general_fn;
|
goto general_fn;
|
||||||
}
|
}
|
||||||
return alloc(join_project_and_fn, get(t1), get(t2),
|
return alloc(join_project_and_fn);
|
||||||
joined_col_cnt, cols1, cols2,
|
|
||||||
removed_col_cnt, removed_cols);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
general_fn:
|
general_fn:
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue